Commit c60e4dcc authored by MARCHE Claude's avatar MARCHE Claude

upgrade proofs with Alt-Ergo versions < 2.0.0

parent 77be6371
......@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../isqrt_von_neumann.mlw" proved="true">
<theory name="VonNeumann16" proved="true">
<goal name="sqr_add2" proved="true">
......@@ -515,14 +515,14 @@
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0" expl="VC for isqrt64" proved="true">
<transf name="assert" proved="true" arg1="(forall a b c. t&#39;int b + t&#39;int c &lt; two_power_size -&gt; ule a b -&gt; ule (add a c) (add b c))">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="128"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="590"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1" expl="VC for isqrt64" proved="true">
<transf name="case" proved="true" arg1="(add (sqr res_g) (mul bits_g1 (add (mul (2:t) res_g) bits_g1)) = (0:t))">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0" expl="true case" proved="true">
<transf name="unfold" proved="true" arg1="sqr" arg2="in" arg3="h">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0.0" expl="true case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.98"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.30"/></proof>
</goal>
</transf>
</goal>
......@@ -556,7 +556,7 @@
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.0.0.1.0.1.0" proved="true">
<transf name="assert" proved="true" arg1="(0 &lt;= t&#39;int b - t&#39;int (1:t))">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.0.0.1.0.1.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="137"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="213"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.0.0.1.0.1.0.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......@@ -564,7 +564,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.0.0.1.0.1.1" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.02" steps="118"/></proof>
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="213"/></proof>
</goal>
</transf>
</goal>
......@@ -601,7 +601,7 @@
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.80" steps="571"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.88"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.26"/></proof>
</goal>
</transf>
</goal>
......@@ -620,7 +620,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.1" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.02" steps="107"/></proof>
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="213"/></proof>
</goal>
</transf>
</goal>
......@@ -636,7 +636,7 @@
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0" proved="true">
<transf name="assert" proved="true" arg1="(forall a b. a * ((2 * b) + a) = (a + b) * (a + b) - b * b)">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="106"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="209"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1" proved="true">
<transf name="replace" proved="true" arg1="(t&#39;int (2:t))" arg2="2">
......@@ -674,7 +674,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="208"/></proof>
<proof prover="5"><result status="valid" time="0.18" steps="215"/></proof>
</goal>
</transf>
</goal>
......@@ -700,21 +700,21 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.1" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="119"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="213"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.28" steps="239"/></proof>
<proof prover="5"><result status="valid" time="0.77" steps="981"/></proof>
</goal>
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.1" proved="true">
<transf name="split_all_right" proved="true" >
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="124"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="544"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.1.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.47"/></proof>
......
This diff is collapsed.
......@@ -2,8 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw" proved="true">
<theory name="TreeOfList" proved="true">
......@@ -25,7 +24,7 @@
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tree_of_list_aux.5" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="36"/></proof>
<proof prover="3" timelimit="1"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="VC tree_of_list_aux.6" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="l&#39;1">
......@@ -40,7 +39,7 @@
</transf>
</goal>
<goal name="VC tree_of_list" expl="VC for tree_of_list" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="145"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
......
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