Commit d31c4a1e authored by MARCHE Claude's avatar MARCHE Claude

update sessions: should be complete now

parent cb08988a
......@@ -3,7 +3,6 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="2" memlimit="0"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="2" memlimit="0"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
......@@ -11,7 +10,6 @@
<theory name="Stmt" sum="468c7dbd45c8c0959e1b169a3ca1bbe3" expanded="true">
<goal name="toto" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></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"/></proof>
......
......@@ -5,7 +5,6 @@
<prover id="0" name="Coq" version="8.4pl4" timelimit="10" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../kmp.mlw" expanded="true">
<theory name="KnuthMorrisPratt" sum="f670f1d351029b654064361a2c56b798" expanded="true">
......@@ -231,7 +230,6 @@
<proof prover="3"><result status="valid" time="0.04" steps="97"/></proof>
</goal>
<goal name="WP_parameter kmp.18" expl="18. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.12"/></proof>
<proof prover="5"><result status="valid" time="3.66" steps="537"/></proof>
</goal>
<goal name="WP_parameter kmp.19" expl="19. loop variant decrease">
......
This diff is collapsed.
......@@ -115,7 +115,7 @@
<proof prover="14"><result status="timeout" time="2.05"/></proof>
<proof prover="15"><result status="unknown" time="0.00"/></proof>
<proof prover="16"><result status="timeout" time="1.99"/></proof>
<proof prover="19"><result status="unknown" time="0.31"/></proof>
<proof prover="19"><result status="unknown" time="0.17"/></proof>
<proof prover="20"><result status="unknown" time="0.01"/></proof>
<proof prover="21"><result status="timeout" time="2.11"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
......@@ -283,7 +283,7 @@
<proof prover="26"><result status="timeout" time="1.99"/></proof>
</goal>
<goal name="smoke2">
<proof prover="2"><result status="unknown" time="0.24"/></proof>
<proof prover="2"><result status="unknown" time="0.09"/></proof>
<proof prover="7"><result status="unknown" time="0.02"/></proof>
<proof prover="8"><result status="timeout" time="1.99"/></proof>
<proof prover="9"><result status="timeout" time="2.01"/></proof>
......@@ -310,7 +310,7 @@
<proof prover="14"><result status="timeout" time="2.09"/></proof>
<proof prover="15"><result status="unknown" time="0.00"/></proof>
<proof prover="16"><result status="timeout" time="1.99"/></proof>
<proof prover="17" obsolete="true"><result status="unknown" time="0.00"/></proof>
<proof prover="17"><result status="unknown" time="0.00"/></proof>
<proof prover="18"><result status="timeout" time="5.14"/></proof>
<proof prover="19"><result status="unknown" time="0.02"/></proof>
<proof prover="20"><result status="unknown" time="0.05"/></proof>
......@@ -357,7 +357,7 @@
<proof prover="26"><result status="timeout" time="1.99"/></proof>
</goal>
<goal name="smoke6">
<proof prover="2"><result status="unknown" time="0.25"/></proof>
<proof prover="2"><result status="unknown" time="0.10"/></proof>
<proof prover="7"><result status="unknown" time="0.01"/></proof>
<proof prover="8"><result status="timeout" time="1.98"/></proof>
<proof prover="9"><result status="timeout" time="2.00"/></proof>
......
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