Commit 5fea7e14 authored by Benedikt Becker's avatar Benedikt Becker

Add bench test for replaying session without shapes

parent 0f57a419
......@@ -162,6 +162,29 @@ replay () {
done
}
replay_without_shape () {
pgm="bin/why3replay$suffix"; test=$1
test -d "$test" || exit 1
echo -n "Replay $test with shapes... "
if "$pgm" "$test" > /dev/null 2>&1; then
echo "OK."
else
echo "Failure!"
exit 1
fi
echo -n "Replay $test without shapes... "
noshapes=$(mktemp -d -p $(dirname "$test") "$(basename "$test")-without-shapes.XXXXXXXX")
cp "$test/why3session.xml" "$noshapes"
if "$pgm" "$noshapes" > /dev/null 2>&1 ; then
echo "OK."
rm -rf "$noshapes"
else
echo "Failure!"
rm -rf "$noshapes"
exit 1
fi
}
execute () {
pgm="bin/why3execute$suffix"
printf " $1 $2... "
......@@ -440,6 +463,9 @@ echo "=== Checking extraction to C ==="
extract_and_test_wmp examples/multiprecision
echo ""
echo "=== Checking replay without shapes ==="
replay_without_shape examples/replay
echo "=== Checking replay (no prover) ==="
replay bench/replay
replay examples/stdlib --merging-only
......
use int.Int
lemma l : (forall x. x + x = 2 * x) /\ (forall x. x = 0)
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="whyml">
<path name=".."/><path name="replay.mlw"/>
<theory name="Top">
<goal name="l">
<transf name="split_vc" >
<goal name="l.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="192"/></proof>
</goal>
<goal name="l.1">
<proof prover="1"><result status="unknown" time="0.03" steps="4706"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment