Commit f62c3a64 authored by MARCHE Claude's avatar MARCHE Claude

more sessions updated

parent 39507b0d
......@@ -3,22 +3,22 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" memlimit="0"/>
<file name="../ac.why">
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../ac.why" expanded="true">
<theory name="Test" sum="83d8b556674b949a66206b6d5ca52ded" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,44 +3,39 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="3" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" memlimit="0"/>
<prover id="4" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" memlimit="0"/>
<file name="../array.why">
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../array.why" expanded="true">
<theory name="Test_simplify_array" sum="6cb2fd4ede8c2e597266ad5a6f4953c4" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G4" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,28 +3,28 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../bool.why" expanded="true">
<theory name="Test" sum="1df769008ab78b260468adc25cb91f79" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,32 +2,29 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.94" timelimit="3" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="3" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="3" memlimit="1000"/>
<prover id="8" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../euclideandivision.why" expanded="true">
<theory name="Test" sum="34acc475394bbedc4a443071938d84bc" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="0"/>
<prover id="3" name="Gappa" version="1.1.1" timelimit="5" memlimit="0"/>
<file name="../floats.why">
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" memlimit="0"/>
<file name="../floats.why" expanded="true">
<theory name="TestGappa" sum="ed330ba56218830382ea9b26d56f5cd1" expanded="true">
<goal name="Round_single_01" expanded="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -16,9 +16,9 @@
</goal>
<goal name="Test00" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Test01" expanded="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
......
......@@ -2,115 +2,115 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" memlimit="0"/>
<prover id="2" name="Eprover" version="1.6" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="4" name="Spass" version="3.7" timelimit="10" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" memlimit="0"/>
<prover id="6" name="Vampire" version="0.6" timelimit="5" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="8" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../int.why" expanded="true">
<theory name="Test" sum="fc4f5a5b6868cb7535da7ff9ae921fff" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="4.99"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.06"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="timeout" time="10.09"/></proof>
<proof prover="6"><result status="timeout" time="5.10"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="4.99"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="4.98"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.04"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="timeout" time="10.09"/></proof>
<proof prover="6"><result status="timeout" time="5.01"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="4.98"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="CompatOrderAdd" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="CompatOrderMult" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="1.28"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="InvMult" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.86"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="InvSquare" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.78"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ZeroMult" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="SquareNonNeg1" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.04"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="timeout" time="10.10"/></proof>
<proof prover="6"><result status="timeout" time="5.05"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="8"><result status="valid" time="0.04"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="SquareNonNeg" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.74"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="timeout" time="10.03"/></proof>
<proof prover="6"><result status="timeout" time="5.09"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.09"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ZeroLessOne" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="MinMax" sum="5a65a1cfb37258d4746169718f12d1d3" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="4.96"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.06"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="timeout" time="10.03"/></proof>
<proof prover="6"><result status="timeout" time="5.10"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="8"><result status="timeout" time="4.96"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,69 +3,58 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" memlimit="0"/>
<prover id="4" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
<prover id="5" name="Yices" version="1.0.38" timelimit="10" memlimit="0"/>
<prover id="6" name="Z3" version="3.2" timelimit="10" memlimit="0"/>
<prover id="7" name="Gappa" version="1.1.1" timelimit="2" memlimit="0"/>
<file name="../intreal.why">
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../intreal.why" expanded="true">
<theory name="IntReal" sum="3622340391eb2916078d6fa44290f09a" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="10.74"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.06" steps="34"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="1"><result status="valid" time="0.86"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="timeout" time="9.98"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.14" steps="97"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="1"><result status="valid" time="1.57"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="10.10"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.17" steps="100"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G4" expanded="true">
<proof prover="1"><result status="timeout" time="9.99"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.48" steps="142"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5" expanded="true">
<proof prover="1"><result status="timeout" time="9.99"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="9.44"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.46" steps="142"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G6" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.06" steps="63"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G7" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="10.24"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,22 +3,22 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" memlimit="0"/>
<file name="../minmax.why">
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../minmax.why" expanded="true">
<theory name="MinMax" sum="f36cdaa208948cc789cc9e1e3ab076fd" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,10 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.94" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="Simplify" version="1.5.4" timelimit="5" memlimit="1000"/>
......@@ -14,31 +11,33 @@
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="10" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="11" name="Vampire" version="0.6" timelimit="5" memlimit="1000"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="13" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<file name="../First.why" expanded="true">
<theory name="First" sum="dd3c827a781536c6a3834f92a8f38d9a" expanded="true">
<goal name="P1" expanded="true">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="unknown" time="0.02"/></proof>
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="P5" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="10"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,21 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.94" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC3" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../simple.why" expanded="true">
<theory name="T" sum="1679103123ca3a04d928eceb3513f011" expanded="true">
<goal name="g" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="9"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="5" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="4" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Yices" version="1.0.38" timelimit="5" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="8" name="Coq" version="8.4pl6" timelimit="5" memlimit="0"/>
<file name="../sorted_list.why" expanded="true">
<theory name="Order" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
......@@ -18,16 +18,16 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sorted_mem" expanded="true">
<proof prover="1" edited="sorted_list_SortedList_sorted_mem_1.v"><result status="valid" time="0.98"/></proof>
<proof prover="8" edited="sorted_list_SortedList_sorted_mem_1.v"><result status="valid" time="0.98"/></proof>
</goal>
</theory>
<theory name="SortedIntList" sum="b630995dca805d46336501a60025b5e3" expanded="true">
<goal name="sorted123" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,29 +2,31 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="0"/>
<prover id="3" name="CVC3" version="2.2" timelimit="5" memlimit="0"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" memlimit="0"/>
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../cvc3.why">
<theory name="Test" sum="1c79e9f8067af1c17a7189620aa61164" expanded="true">
<goal name="test1" expanded="true">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.03"/></proof>
<proof prover="4"><result status="unknown" time="0.01"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="0.01"/></proof>
<proof prover="7"><result status="unknown" time="0.03"/></proof>
</goal>
<goal name="test2" expanded="true">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="5.02"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>