Commit 2a375d95 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

update sessions

parent 323642e8
This diff is collapsed.
......@@ -4,11 +4,11 @@
<why3session shape_version="4">
<prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../lemmas.mlw">
<theory name="Lemmas">
<file name="../lemmas.mlw" proved="true">
<theory name="Lemmas" proved="true">
<goal name="VC map_eq_shift" expl="VC for map_eq_shift" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC map_eq_shift.0" expl="postcondition" proved="true">
......@@ -57,7 +57,7 @@
<proof prover="5" memlimit="2000"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC prod_compat_strict_lr" expl="VC for prod_compat_strict_lr" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_sub" expl="VC for value_sub" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -219,7 +219,7 @@
<proof prover="5"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="VC value_sub_lower_bound.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
......@@ -268,7 +268,8 @@
<goal name="VC value_concat" expl="VC for value_concat" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="26"/></proof>
</goal>
<goal name="VC value_sub_eq" expl="VC for value_sub_eq">
<goal name="VC value_sub_eq" expl="VC for value_sub_eq" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
</file>
......
......@@ -1153,7 +1153,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.29" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.30" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1165,7 +1165,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.33" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.34" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -2121,10 +2121,10 @@
</transf>
</goal>
<goal name="VC wmpn_toom22_mul.335.3.1" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.335.3.2" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
......@@ -5651,13 +5651,13 @@
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.237" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.238" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.239" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.240" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
......@@ -6739,10 +6739,10 @@
<proof prover="1"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.1" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.2" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.3" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
......@@ -7476,10 +7476,10 @@
<proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.473.0.0.0.1" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.28"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.473.0.0.0.2" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.28"/></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