Commit a22b3f29 authored by MARCHE Claude's avatar MARCHE Claude

update oboslete sessions

parent 8045490e
......@@ -587,7 +587,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="1.08" steps="614"/></proof>
</goal>
<goal name="VC pop_min.3.2" expl="VC for pop_min" proved="true">
<proof prover="0" timelimit="20"><result status="valid" time="6.54" steps="2313"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="6.54" steps="2303"/></proof>
</goal>
</transf>
</goal>
......@@ -599,7 +599,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
<goal name="VC add.1" expl="postcondition" proved="true">
<proof prover="0" timelimit="20"><result status="valid" time="8.04" steps="3503"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="8.04" steps="3504"/></proof>
</goal>
<goal name="VC add.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
......
......@@ -8,8 +8,6 @@
<prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double.why" proved="true">
<theory name="BV_double" proved="true">
</theory>
<theory name="TestDouble" proved="true">
<goal name="nth_one1" proved="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
......
......@@ -13,7 +13,7 @@
</goal>
<goal name="sign_of_j" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="3"><result status="valid" time="4.87"/></proof>
<proof prover="3"><result status="valid" time="4.23"/></proof>
</goal>
<goal name="mantissa_of_j" proved="true">
<proof prover="1"><result status="valid" time="0.16" steps="121"/></proof>
......@@ -51,7 +51,7 @@
<proof prover="1"><result status="valid" time="1.72" steps="492"/></proof>
<proof prover="3"><result status="valid" time="1.64"/></proof>
<proof prover="5"><result status="valid" time="2.98"/></proof>
<proof prover="9"><result status="valid" time="0.88"/></proof>
<proof prover="9"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="Mantissa_of_xor_j" proved="true">
<proof prover="3"><result status="valid" time="1.72"/></proof>
......
......@@ -116,7 +116,7 @@
</goal>
<goal name="VC insert.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="182"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC insert.4" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -129,7 +129,7 @@
</goal>
<goal name="VC insert.7" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="104"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
......
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