Skip to content

GitLab

Commit 3c08305d authored by François Bobot's avatar François Bobot
Browse files
Options

regtest check-builtin from previous last part of make bench

parent 3aae4bbd
Hide whitespace changes
Inline Side-by-side
Showing with 607 additions and 52 deletions
bench/bench
View file @ 3c08305d
......@@ -98,27 +98,6 @@ valid_goals () {
done
}
test_provers () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgml -L modules -P alt-ergo $f | grep -q -v Valid; then
echo "valid test $f failed!"
exit 1
else
echo "ok"
fi
done
}
test_prover () {
if $pgm -t 1 -P $1 $2 | grep -q -v Valid; then
echo " $1 fails!"
else
true
fi
}
echo "=== Checking drivers ==="
drivers drivers
echo ""
......@@ -173,34 +152,3 @@ echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking provers ==="
echo -n "Test provers on true..."
provers=$($pgm --list-provers | cut -d " " -f 3 |grep -v "^$")
good_provers=""
bad_provers=""
for prover in $(echo $provers); do
if $pgm -P $prover bench/true_goal.why | grep -q -v Valid; then
#echo "$i : Fail"
bad_provers="$bad_provers $prover"
else
#echo "$i : Ok"
good_provers="$good_provers $prover"
fi
done
echo "done"
echo ""
echo "On your installation the following provers can't prove \"true\":"
echo " $bad_provers"
echo ""
echo "So I will only test the following provers:"
echo $good_provers
echo ""
echo "nb : If a prover can't prove a goal it's perhaps normal (ex: TPTP int)"
for file in bench/valid/*.why; do
echo I test $file
for prover in $good_provers; do
test_prover $prover $file
done
done
examples/check-builtin/ac/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/ac/why3session.xml">
<file name="../ac.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="bb6db914adb3909c925fcf44bf71f57d" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="G2" sum="0ea5f5c71116d14a913f0b8472566d9d" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
bench/valid/array.why → examples/check-builtin/array.why
View file @ 3c08305d
theory Test_simplify_array
use import int.Int
use import array.Array
goal G1 : forall x y:int. forall m: t int int.
use import map.Map
goal G1 : forall x y:int. forall m: map int int.
get (set m y x) y = x
goal G2 : forall x y y' z t:int. forall m: t int int.
goal G2 : forall x y y' z t:int. forall m: map int int.
z <> x ->
get m z = y ->
get (set m x t) z = y
goal G3 : forall y t:int. forall m: t int int.
goal G3 : forall y t:int. forall m: map int int.
get m 0 = y ->
get (set m 1 t) 0 = y
goal G4 : forall x y:int. forall m: t int int.
goal G4 : forall x y:int. forall m: map int int.
get (set (set m 1 y) 0 x) 1 = y
end
examples/check-builtin/array/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/array/why3session.xml">
<file name="../array.why" verified="true" expanded="true">
<theory name="Test_simplify_array" verified="true" expanded="true">
<goal name="G1" sum="6ba9acd1575b0f736753d499a8efa246" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="G2" sum="ba915c2a50e7cb9f66307625030ee440" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="G3" sum="b23fa0a82a81a38100f4990bc5abb06e" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.26"/>
</proof>
</goal>
<goal name="G4" sum="d3736da01102cfb2b3afd57824a993b6" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.33"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/check-builtin/bool/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/bool/why3session.xml">
<file name="../bool.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="7a4b1e7f9f3ee4396d85e1a8843f6c12" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="G2" sum="20e7efb7a2beea23a901d014d3170906" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="G3" sum="2b68363a02d3c401d7a5e6cdbe821586" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/check-builtin/euclideandivision/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/euclideandivision/why3session.xml">
<file name="../euclideandivision.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="ea3bac3defe8dd6c6d07e6bb9584018e" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.01"/>
</proof>
</goal>
<goal name="G2" sum="dcd09929b230a018d26799f2df130ea7" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/check-builtin/int/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/int/why3session.xml">
<file name="../int.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="98b174d6537c40a661dc0b7d6f3e520b" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
</proof>
</goal>
<goal name="G2" sum="175866f81a3b591fe7df5ff8ff1ef55b" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.86"/>
</proof>
</goal>
<goal name="CompatOrderAdd" sum="02c33f1f120f2b572184ff1c06167612" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="CompatOrderMult" sum="2e444ab191874072ca95793d2879fedc" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="InvMult" sum="4907a61fa41e315f3b1560b2b81da1c7" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal name="InvSquare" sum="6d651319668b874df6ffff5949ff351a" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.00"/>
</proof>
</goal>
<goal name="ZeroMult" sum="03cb0ff22ce434d243461722498d91be" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
</proof>
</goal>
<goal name="SquareNonNeg1" sum="49c00266b63c5dd81016599a42c3c974" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.02"/>
</proof>
</goal>
<goal name="SquareNonNeg" sum="a764585ab6e7bc8dfc325378da917597" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.02"/>
</proof>
</goal>
<goal name="ZeroLessOne" sum="56f411cdab6239e1fe4ea11ea3fee8f6" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.22"/>
</proof>
</goal>
</theory>
<theory name="MinMax" verified="true" expanded="true">
<goal name="G" sum="c78ae26be8a59b8e491e9ac728bbc370" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.18"/>
</proof>
</goal>
</theory>
</file>
</why3session>
bench/valid/intreal.why → examples/check-builtin/intreal.why
View file @ 3c08305d
......@@ -9,4 +9,6 @@ theory IntReal
goal G3 : ceil 1.5 = 2
goal G4 : floor (-. 1.5) = -2
goal G5 : ceil (-. 1.5) = -1
goal G6 : forall x : real. floor x <= ceil x
goal G7 : forall x : real. floor x < ceil x -> from_int (floor x) <> x
end
\ No newline at end of file
examples/check-builtin/intreal/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/intreal/why3session.xml">
<file name="../intreal.why" verified="false" expanded="true">
<theory name="IntReal" verified="false" expanded="true">
<goal name="G1" sum="41cbb072f0422d7fc2669af8ba21266b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.29"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.71"/>
</proof>
</goal>
<goal name="G2" sum="fc8aef6289612cfc6453aa02b65cb4d7" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.13"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.80"/>
</proof>
</goal>
<goal name="G3" sum="2b144ec692c704a919d42bcaaa43cccc" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.70"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
</goal>
<goal name="G4" sum="b72371e68b7e34dd72abf019ccb87857" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="6.56"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.07"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.89"/>
</proof>
</goal>
<goal name="G5" sum="ebaa33d09abd898b1e9a54523d586c6d" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="7.67"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.08"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.22"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.92"/>
</proof>
</goal>
<goal name="G6" sum="a6faa76e2ab2363d3142000b50f8e230" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.22"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.48"/>
</proof>
</goal>
<goal name="G7" sum="6c4f130bd29b7d8dad7df3d02454e299" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.27"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/check-builtin/minmax.why 0 → 100644
View file @ 3c08305d
theory MinMax
use import comparison.MinMax
goal G : forall x y z : t. ge z y -> ge z x -> ge y x ->
min x (max (min z x) y) = x
goal G2 : forall x y z : t. max x y = x -> ge x y
end
\ No newline at end of file
examples/check-builtin/minmax/why3session.xml 0 → 100644
View file @ 3c08305d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/minmax/why3session.xml">
<file name="../minmax.why" verified="true" expanded="true">
<theory name="MinMax" verified="true" expanded="true">
<goal name="G" sum="351de8b4cf3d0c7d450f7d1d2f9cc553" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="spass" timelimit="10" edited=