Commit 20b50a4b authored by MARCHE Claude's avatar MARCHE Claude

update session after former commit: some 'unknown' results are now considered as 'timeout'

parent fa40a1be
......@@ -2,9 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Eprover" version="1.6" timelimit="5" memlimit="1000"/>
<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="Alt-Ergo" version="0.95.1" timelimit="10" 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"/>
......@@ -12,25 +12,25 @@
<file name="../int.why" expanded="true">
<theory name="Test" sum="fc4f5a5b6868cb7535da7ff9ae921fff" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<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="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="unknown" time="10.09"/></proof>
<proof prover="6"><result status="timeout" time="10.09"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<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="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="unknown" time="10.09"/></proof>
<proof prover="6"><result status="timeout" time="10.09"/></proof>
</goal>
<goal name="CompatOrderAdd" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<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>
......@@ -39,25 +39,25 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="CompatOrderMult" expanded="true">
<proof prover="0"><result status="valid" time="1.28"/></proof>
<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="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>
</goal>
<goal name="InvMult" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<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="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>
</goal>
<goal name="InvSquare" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<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>
......@@ -66,7 +66,7 @@
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="ZeroMult" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<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>
......@@ -75,25 +75,25 @@
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="SquareNonNeg1" expanded="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<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="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="unknown" time="10.10"/></proof>
<proof prover="6"><result status="timeout" time="10.10"/></proof>
</goal>
<goal name="SquareNonNeg" expanded="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
<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="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="unknown" time="10.03"/></proof>
<proof prover="6"><result status="timeout" time="10.03"/></proof>
</goal>
<goal name="ZeroLessOne" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<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>
......@@ -104,13 +104,13 @@
</theory>
<theory name="MinMax" sum="5a65a1cfb37258d4746169718f12d1d3" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<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="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="unknown" time="10.03"/></proof>
<proof prover="6"><result status="timeout" time="10.03"/></proof>
</goal>
</theory>
</file>
......
......@@ -29,7 +29,7 @@
<proof prover="5" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. postcondition">
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="0.92"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="10" memlimit="1000"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
......@@ -75,7 +75,7 @@
<proof prover="5" memlimit="1000"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="gcd_even_odd">
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="1.78"/></proof>
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="gcd_even_odd2">
<proof prover="5" memlimit="1000"><result status="valid" time="0.17" steps="28"/></proof>
......@@ -160,7 +160,7 @@
<proof prover="6"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.20" expl="20. precondition">
<proof prover="4"><result status="valid" time="6.49"/></proof>
<proof prover="4"><result status="valid" time="3.49"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.03" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -171,29 +171,29 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm31" sum="d566d8cda9a9bac5bbc9bd41ecf5cfb3" expanded="true">
<theory name="EuclideanAlgorithm31" sum="7e6c4a6c940f11f7bb2278b052b9d3e7" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. division by zero">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="46"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="51"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. variant decrease">
<proof prover="5" timelimit="5"><result status="valid" time="0.80" steps="114"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.80" steps="169"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. precondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="21"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="WP_parameter euclid.7" expl="7. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.97" steps="42"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="45"/></proof>
</goal>
</transf>
</goal>
......
......@@ -53,19 +53,19 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g7b" expanded="true">
<proof prover="1"><result status="timeout" time="2.96"/></proof>
<proof prover="1"><result status="timeout" time="4.00"/></proof>
</goal>
<goal name="g8a" expanded="true">
<proof prover="1"><result status="timeout" time="2.93"/></proof>
<proof prover="1"><result status="timeout" time="4.00"/></proof>
</goal>
<goal name="g8b" expanded="true">
<proof prover="1"><result status="timeout" time="3.01"/></proof>
<proof prover="1"><result status="timeout" time="4.00"/></proof>
</goal>
<goal name="Nth_bw_and">
<proof prover="1"><result status="valid" time="0.16"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_bw_or">
<proof prover="1"><result status="valid" time="0.16"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_bw_xor">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -82,7 +82,7 @@
<goal name="Lsr_nth_low" expanded="true">
</goal>
<goal name="Lsr_nth_high" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Asr_nth_low" expanded="true">
</goal>
......
......@@ -4,18 +4,18 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="30" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.6" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="14" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="7" name="Spass" version="3.7" timelimit="30" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="14" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="5" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="6" name="Spass" version="3.7" timelimit="30" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="8" name="Yices" version="1.0.38" timelimit="7" memlimit="0"/>
<prover id="9" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="10" name="Metis" version="2.3" timelimit="5" memlimit="4000"/>
<prover id="9" name="Metis" version="2.3" timelimit="5" memlimit="4000"/>
<prover id="10" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="12" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="13" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="12" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="13" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="14" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="15" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
<file name="../einstein.why" expanded="true">
......@@ -26,56 +26,56 @@
<theory name="Goals" sum="9fe1211e777a560b454f17977bc1a636" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="13.44" steps="1560"/></proof>
<proof prover="2"><result status="unknown" time="0.17"/></proof>
<proof prover="3" timelimit="17"><result status="valid" time="21.79"/></proof>
<proof prover="4"><result status="valid" time="1.20"/></proof>
<proof prover="5" timelimit="5"><result status="unknown" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="4.51"/></proof>
<proof prover="7"><result status="valid" time="5.72"/></proof>
<proof prover="2" timelimit="17"><result status="valid" time="13.76" steps="969"/></proof>
<proof prover="3"><result status="unknown" time="0.17"/></proof>
<proof prover="4" timelimit="5"><result status="unknown" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.88"/></proof>
<proof prover="6"><result status="valid" time="4.35"/></proof>
<proof prover="7"><result status="valid" time="3.56"/></proof>
<proof prover="8"><result status="unknown" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.26"/></proof>
<proof prover="10" memlimit="1000"><result status="unknown" time="9.99"/></proof>
<proof prover="11"><result status="valid" time="4.13"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="13"><result status="valid" time="12.38" steps="969"/></proof>
<proof prover="9" memlimit="1000"><result status="timeout" time="9.99"/></proof>
<proof prover="10"><result status="valid" time="0.26"/></proof>
<proof prover="11"><result status="valid" time="2.88"/></proof>
<proof prover="12"><result status="valid" time="12.38" steps="969"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="unknown" time="0.06"/></proof>
<proof prover="15"><result status="valid" time="2.72"/></proof>
<proof prover="15"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="Wrong" expanded="true">
<proof prover="0"><result status="unknown" time="15.98"/></proof>
<proof prover="1" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3" timelimit="5"><result status="timeout" time="5.00"/></proof>
<proof prover="4" timelimit="5"><result status="timeout" time="4.95"/></proof>
<proof prover="5"><result status="unknown" time="0.04"/></proof>
<proof prover="6" timelimit="5"><result status="timeout" time="4.97"/></proof>
<proof prover="7" timelimit="5"><result status="timeout" time="4.99"/></proof>
<proof prover="2" timelimit="5"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="0.06"/></proof>
<proof prover="4"><result status="unknown" time="0.04"/></proof>
<proof prover="5" timelimit="5"><result status="timeout" time="4.95"/></proof>
<proof prover="6" timelimit="5"><result status="timeout" time="4.99"/></proof>
<proof prover="7" timelimit="5"><result status="timeout" time="4.97"/></proof>
<proof prover="8" timelimit="5"><result status="unknown" time="0.00"/></proof>
<proof prover="9" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="10"><result status="unknown" time="10.02"/></proof>
<proof prover="9"><result status="timeout" time="10.02"/></proof>
<proof prover="10" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="11"><result status="timeout" time="5.00"/></proof>
<proof prover="12"><result status="timeout" time="4.97"/></proof>
<proof prover="13"><result status="unknown" time="9.98"/></proof>
<proof prover="12"><result status="unknown" time="9.98"/></proof>
<proof prover="13"><result status="timeout" time="4.97"/></proof>
<proof prover="14"><result status="unknown" time="0.06"/></proof>
<proof prover="15" timelimit="5"><result status="unknown" time="10.08"/></proof>
<proof prover="15" timelimit="5"><result status="timeout" time="10.08"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="12.12" steps="1747"/></proof>
<proof prover="1"><result status="valid" time="33.44"/></proof>
<proof prover="2" timelimit="30"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="13.26"/></proof>
<proof prover="4"><result status="valid" time="2.70"/></proof>
<proof prover="5"><result status="unknown" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="4.45"/></proof>
<proof prover="7"><result status="valid" time="5.40"/></proof>
<proof prover="1"><result status="valid" time="17.81"/></proof>
<proof prover="2"><result status="valid" time="8.54" steps="1007"/></proof>
<proof prover="3" timelimit="30"><result status="unknown" time="0.06"/></proof>
<proof prover="4"><result status="unknown" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="1.99"/></proof>
<proof prover="6"><result status="valid" time="4.18"/></proof>
<proof prover="7"><result status="valid" time="3.46"/></proof>
<proof prover="8"><result status="unknown" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.83"/></proof>
<proof prover="10"><result status="valid" time="7.04"/></proof>
<proof prover="11"><result status="valid" time="1.71"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="13"><result status="valid" time="7.55" steps="1007"/></proof>
<proof prover="9"><result status="valid" time="3.74"/></proof>
<proof prover="10"><result status="valid" time="0.62"/></proof>
<proof prover="11"><result status="valid" time="0.79"/></proof>
<proof prover="12"><result status="valid" time="7.55" steps="1007"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
<proof prover="14" timelimit="3"><result status="unknown" time="0.06"/></proof>
<proof prover="15"><result status="valid" time="2.66"/></proof>
<proof prover="15"><result status="valid" time="1.27"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
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