Commit 3105ad7e authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Move memory model to stdlib

parent b8420ce8
......@@ -1307,7 +1307,6 @@
<proof prover="9" memlimit="2000"><result status="valid" time="0.16" steps="104"/></proof>
</goal>
<goal name="VC add_in_place.18" expl="assertion" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="9.92"/></proof>
<transf name="split_goal_wp" proved="true" >
<goal name="VC add_in_place.18.0" expl="VC for add_in_place" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.37" steps="127"/></proof>
......@@ -1612,14 +1611,12 @@
<proof prover="0" memlimit="1000"><result status="valid" time="3.69"/></proof>
</goal>
<goal name="VC sub_limb.13.1" expl="VC for sub_limb" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.09" steps="112"/></proof>
</goal>
<goal name="VC sub_limb.13.2" expl="VC for sub_limb" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sub_limb.13.3" expl="VC for sub_limb" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="99"/></proof>
</goal>
<goal name="VC sub_limb.13.4" expl="VC for sub_limb" proved="true">
......@@ -1629,13 +1626,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sub_limb.13.6" expl="VC for sub_limb" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.21" steps="123"/></proof>
</goal>
<goal name="VC sub_limb.13.7" expl="VC for sub_limb" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.06"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
......@@ -1750,9 +1744,6 @@
</goal>
<goal name="VC sub_limbs.9" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="4.02"/></proof>
<proof prover="2" timelimit="10" memlimit="4000" obsolete="true"><result status="unknown" time="10.05"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="9.99"/></proof>
</goal>
<goal name="VC sub_limbs.10" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
......@@ -1773,19 +1764,14 @@
<transf name="split_goal_wp" proved="true" >
<goal name="VC sub_limbs.15.0" expl="VC for sub_limbs" proved="true">
<proof prover="0"><result status="valid" time="4.17"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="1.08"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="0.99"/></proof>
</goal>
<goal name="VC sub_limbs.15.1" expl="VC for sub_limbs" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.14" steps="118"/></proof>
</goal>
<goal name="VC sub_limbs.15.2" expl="VC for sub_limbs" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sub_limbs.15.3" expl="VC for sub_limbs" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.11" steps="103"/></proof>
</goal>
<goal name="VC sub_limbs.15.4" expl="VC for sub_limbs" proved="true">
......@@ -1801,17 +1787,13 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sub_limbs.15.8" expl="VC for sub_limbs" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.35" steps="125"/></proof>
</goal>
<goal name="VC sub_limbs.15.9" expl="VC for sub_limbs" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.30" steps="124"/></proof>
</goal>
<goal name="VC sub_limbs.15.10" expl="VC for sub_limbs" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.12"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
......@@ -1876,9 +1858,6 @@
</goal>
<goal name="VC sub.10.0.1" proved="true">
<proof prover="0"><result status="valid" time="4.62"/></proof>
<proof prover="2" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="9.98"/></proof>
</goal>
</transf>
</goal>
......@@ -2013,8 +1992,6 @@
<proof prover="9" memlimit="2000"><result status="valid" time="0.07" steps="118"/></proof>
</goal>
<goal name="VC sub.37" expl="loop invariant preservation" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="118"/></proof>
</goal>
<goal name="VC sub.38" expl="loop invariant preservation" proved="true">
......@@ -2042,8 +2019,6 @@
<goal name="VC sub.45" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC sub.45.0" expl="assertion" proved="true">
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="1.05"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.28" steps="210"/></proof>
</goal>
</transf>
......@@ -2063,14 +2038,12 @@
<proof prover="0"><result status="valid" time="2.32"/></proof>
</goal>
<goal name="VC sub.49.1" expl="VC for sub" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.08" steps="130"/></proof>
</goal>
<goal name="VC sub.49.2" expl="VC for sub" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sub.49.3" expl="VC for sub" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.07" steps="114"/></proof>
</goal>
<goal name="VC sub.49.4" expl="VC for sub" proved="true">
......@@ -2080,13 +2053,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sub.49.6" expl="VC for sub" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.16" steps="138"/></proof>
</goal>
<goal name="VC sub.49.7" expl="VC for sub" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.07"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
</transf>
</goal>
......@@ -2753,22 +2723,14 @@
</goal>
<goal name="VC addmul_limb.22.1" expl="VC for addmul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.08"/></proof>
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.06"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="9.99"/></proof>
</goal>
<goal name="VC addmul_limb.22.2" expl="VC for addmul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.05"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="4" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
</goal>
<goal name="VC addmul_limb.22.3" expl="VC for addmul_limb" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC addmul_limb.22.4" expl="VC for addmul_limb" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.96"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC addmul_limb.22.5" expl="VC for addmul_limb" proved="true">
......@@ -2788,12 +2750,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC addmul_limb.22.9" expl="VC for addmul_limb" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.93"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="1.91"/></proof>
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.07"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="4" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
</goal>
<goal name="VC addmul_limb.22.10" expl="VC for addmul_limb" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.02"/></proof>
......@@ -2811,8 +2768,6 @@
<transf name="inline_all" proved="true" >
<goal name="VC addmul_limb.22.14.0" expl="VC for addmul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.75"/></proof>
<proof prover="2" timelimit="10" memlimit="4000" obsolete="true"><result status="unknown" time="10.05"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="9.99"/></proof>
</goal>
</transf>
</goal>
......@@ -3362,7 +3317,6 @@
<proof prover="9" timelimit="20"><result status="valid" time="0.58" steps="140"/></proof>
</goal>
<goal name="VC addmul_limbs.36" expl="assertion" proved="true">
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.06"/></proof>
<transf name="split_goal_wp" proved="true" >
<goal name="VC addmul_limbs.36.0" expl="VC for addmul_limbs" proved="true">
<proof prover="9" memlimit="2000"><result status="valid" time="0.58" steps="137"/></proof>
......@@ -3661,26 +3615,17 @@
<proof prover="1" memlimit="2000"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="VC mul.33.4" expl="VC for mul" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.96"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="2.82"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.08"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="VC mul.33.5" expl="VC for mul" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="3.25"/></proof>
</goal>
<goal name="VC mul.33.6" expl="VC for mul" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.07"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="4" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC mul.33.7" expl="VC for mul" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC mul.33.7.0" expl="VC for mul" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.96"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......@@ -3929,7 +3874,6 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC lsld_ext.10.4" expl="VC for lsld_ext" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.05" steps="97"/></proof>
</goal>
<goal name="VC lsld_ext.10.5" expl="VC for lsld_ext" proved="true">
......@@ -3948,8 +3892,6 @@
</goal>
<goal name="VC lsld_ext.12" expl="postcondition" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.06"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="VC lsld_ext.13" expl="postcondition" proved="true">
<proof prover="9"><result status="valid" time="0.28" steps="131"/></proof>
......@@ -4004,9 +3946,6 @@
</goal>
<goal name="VC clz_ext.1.11" expl="VC for clz_ext" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.08"/></proof>
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.03"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC clz_ext.1.12" expl="VC for clz_ext" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.10"/></proof>
......@@ -4132,7 +4071,6 @@
</goal>
<goal name="VC lshift.28" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="9" obsolete="true"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="VC lshift.29" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
......@@ -4186,7 +4124,6 @@
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC lshift.31.14" expl="VC for lshift" proved="true">
<proof prover="0" memlimit="1000" obsolete="true"><result status="timeout" time="4.93"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC lshift.31.15" expl="VC for lshift" proved="true">
......@@ -5599,7 +5536,6 @@
</goal>
<goal name="VC divmod_1.26" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="VC divmod_1.27" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
......@@ -5620,8 +5556,6 @@
</goal>
<goal name="VC divmod_1.31.1" expl="VC for divmod_1" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.12"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC divmod_1.31.2" expl="VC for divmod_1" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -5643,8 +5577,6 @@
</goal>
<goal name="VC divmod_1.31.8" expl="VC for divmod_1" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.08"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="VC divmod_1.31.9" expl="VC for divmod_1" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -5653,11 +5585,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC divmod_1.31.11" expl="VC for divmod_1" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.98"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="0.12"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.05"/></proof>
<proof prover="3" timelimit="5" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="VC divmod_1.31.12" expl="VC for divmod_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -5703,11 +5631,9 @@
</goal>
<goal name="VC divmod_1.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="VC divmod_1.35" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="VC divmod_1.36" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -5872,9 +5798,6 @@
</goal>
<goal name="VC divmod_1.52" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.11"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC divmod_1.53" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
......@@ -5948,22 +5871,12 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC divmod_1.70" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.94"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="0.94"/></proof>
<proof prover="2" timelimit="10" memlimit="4000" obsolete="true"><result status="unknown" time="10.78"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="9.98"/></proof>
</goal>
<goal name="VC divmod_1.71" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.94"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="0.09"/></proof>
<proof prover="2" timelimit="10" memlimit="4000" obsolete="true"><result status="unknown" time="10.07"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="9.99"/></proof>
</goal>
<goal name="VC divmod_1.72" expl="precondition" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="106"/></proof>
</goal>
<goal name="VC divmod_1.73" expl="loop invariant init" proved="true">
......@@ -6001,8 +5914,6 @@
<proof prover="9" memlimit="2000"><result status="valid" time="0.06" steps="116"/></proof>
</goal>
<goal name="VC divmod_1.84" expl="precondition" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.05" steps="123"/></proof>
</goal>
<goal name="VC divmod_1.85" expl="precondition" proved="true">
......@@ -6032,9 +5943,6 @@
</goal>
<goal name="VC divmod_1.92" expl="integer overflow" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.10"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="VC divmod_1.93" expl="precondition" proved="true">
<proof prover="2" memlimit="2000"><result status="valid" time="0.08"/></proof>
......@@ -6052,18 +5960,12 @@
</goal>
<goal name="VC divmod_1.95.2" expl="VC for divmod_1" proved="true">
<proof prover="0"><result status="valid" time="5.26"/></proof>
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.07"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="VC divmod_1.95.3" expl="VC for divmod_1" proved="true">
<proof prover="2" memlimit="2000"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC divmod_1.95.4" expl="VC for divmod_1" proved="true">
<proof prover="0"><result status="valid" time="0.33"/></proof>
<proof prover="2" memlimit="2000" obsolete="true"><result status="unknown" time="5.71"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC divmod_1.95.5" expl="VC for divmod_1" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -6239,8 +6141,6 @@
<transf name="split_goal_wp" proved="true" >
<goal name="VC div3by2_inv.15.0" expl="VC for div3by2_inv" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="1.12"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="VC div3by2_inv.15.1" expl="VC for div3by2_inv" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -6253,8 +6153,6 @@
</goal>
<goal name="VC div3by2_inv.15.4" expl="VC for div3by2_inv" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.08"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
</transf>
</goal>
......@@ -6559,10 +6457,6 @@
</goal>
<goal name="VC div3by2_inv.17.57" expl="VC for div3by2_inv" proved="true">
<proof prover="0"><result status="valid" time="2.98"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.11"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="VC div3by2_inv.17.58" expl="VC for div3by2_inv" proved="true">
<proof prover="2"><result status="valid" time="0.10"/></proof>
......@@ -6713,8 +6607,6 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC div3by2_inv.17.94.1" proved="true">
<proof prover="2" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<transf name="apply" proved="true" arg1="prod_compat_r">
<goal name="VC div3by2_inv.17.94.1.0" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -7116,9 +7008,6 @@
</goal>
<goal name="VC div3by2_inv.24.1" expl="VC for div3by2_inv" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.09"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="failure" time="0.00"/></proof>
</goal>
<goal name="VC div3by2_inv.24.2" expl="VC for div3by2_inv" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -7146,19 +7035,14 @@
</goal>
<goal name="VC div3by2_inv.24.10" expl="VC for div3by2_inv" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.42"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC div3by2_inv.24.11" expl="VC for div3by2_inv" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.10"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
</transf>
</goal>
<goal name="VC div3by2_inv.25" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="9" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC div3by2_inv.26" expl="precondition" proved="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
......@@ -7170,8 +7054,6 @@
<transf name="split_goal_wp" proved="true" >
<goal name="VC div3by2_inv.27.0" expl="VC for div3by2_inv" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.11"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC div3by2_inv.27.1" expl="VC for div3by2_inv" proved="true">
<proof prover="1"><result status="valid" time="0.14"/></proof>
......@@ -7354,8 +7236,6 @@
<transf name="split_goal_wp" proved="true" >
<goal name="VC div3by2_inv.36.0" expl="assertion" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="1.33"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC div3by2_inv.36.1" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="3.66"/></proof>
......@@ -7434,7 +7314,6 @@
</goal>
<goal name="VC div3by2_inv.47" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="9" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC div3by2_inv.48" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.29"/></proof>
......@@ -7443,15 +7322,9 @@
<transf name="split_goal_wp" proved="true" >
<goal name="VC div3by2_inv.49.0" expl="assertion" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.11"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC div3by2_inv.49.1" expl="assertion" proved="true">
<proof prover="0" memlimit="1000" obsolete="true"><result status="timeout" time="4.94"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.11"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
......@@ -7531,9 +7404,6 @@
</goal>
<goal name="VC div3by2_inv.56.1" expl="VC for div3by2_inv" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.18"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.01"/></proof>
</goal>
</transf>
</goal>
......@@ -7637,16 +7507,9 @@
<proof prover="1"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.10" expl="assertion" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.95"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="0.06"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.11" expl="integer overflow" proved="true">
<proof prover="2" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.07" steps="98"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.12" expl="assertion" proved="true">
......@@ -7672,21 +7535,18 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.17.1" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.24" steps="110"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.17.2" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.17.3" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.28" steps="112"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.17.4" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.17.5" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.27" steps="114"/></proof>
</goal>
</transf>
......@@ -7930,7 +7790,6 @@
</goal>
<goal name="VC reciprocal_word_3by2.42.7" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="9" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
......@@ -8098,10 +7957,6 @@
</goal>
<goal name="VC reciprocal_word_3by2.62" expl="integer overflow" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="1.00"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.63" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......@@ -8162,8 +8017,6 @@
<proof prover="1"><result status="valid" time="1.00"/></proof>
</goal>
<goal name="VC reciprocal_word_3by2.69.1" expl="VC for reciprocal_word_3by2" proved="true">
<proof prover="1" obsolete="true"><result status="highfailure" time="0.81"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.11" steps="130"/></proof>
</goal>
</transf>
......@@ -8369,16 +8222,11 @@
</goal>
<goal name="VC submul_limb.22.2" expl="VC for submul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.42"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="failure" time="0.00"/></proof>
</goal>
<goal name="VC submul_limb.22.3" expl="VC for submul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC submul_limb.22.4" expl="VC for submul_limb" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.95"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC submul_limb.22.5" expl="VC for submul_limb" proved="true">
......@@ -8402,11 +8250,7 @@
</transf>
</goal>
<goal name="VC submul_limb.22.9" expl="VC for submul_limb" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.94"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="1.96"/></proof>
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.35"/></proof>
<proof prover="3" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
<proof prover="9" timelimit="10" memlimit="4000" obsolete="true"><result status="failure" time="0.00"/></proof>
</goal>
<goal name="VC submul_limb.22.10" expl="VC for submul_limb" proved="true">
<proof prover="2" memlimit="2000"><result status="valid" time="0.05"/></proof>
......@@ -8651,7 +8495,6 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC div_sb_qr.32.2" expl="VC for div_sb_qr" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.09" steps="145"/></proof>
</goal>
<goal name="VC div_sb_qr.32.3" expl="VC for div_sb_qr" proved="true">
......@@ -8666,22 +8509,15 @@
</transf>
</goal>
<goal name="VC div_sb_qr.32.4" expl="VC for div_sb_qr" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" memlimit="2000" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.05" steps="123"/></proof>
</goal>
<goal name="VC div_sb_qr.32.5" expl="VC for div_sb_qr" proved="true">
<proof prover="9" memlimit="2000"><result status="valid" time="0.04" steps="123"/></proof>
</goal>
<goal name="VC div_sb_qr.32.6" expl="VC for div_sb_qr" proved="true">
<proof prover="2" timelimit="1" obsolete="true"><result status="timeout" time="2.00"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<transf name="split_goal_wp" proved="true" >
<goal name="VC div_sb_qr.32.6.0" expl="VC for div_sb_qr" proved="true">
<proof prover="0"><result status="valid" time="0.43"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="failure" time="0.00"/></proof>
</goal>
<goal name="VC div_sb_qr.32.6.1" expl="VC for div_sb_qr" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -8692,7 +8528,6 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC div_sb_qr.32.8" expl="VC for div_sb_qr" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.12" steps="138"/></proof>
</goal>
<goal name="VC div_sb_qr.32.9" expl="VC for div_sb_qr" proved="true">
......@@ -8866,8 +8701,6 @@
<goal name="VC div_sb_qr.46" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC div_sb_qr.46.0" expl="VC for div_sb_qr" proved="true">
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.10" steps="135"/></proof>
</goal>
<goal name="VC div_sb_qr.46.1" expl="VC for div_sb_qr" proved="true">
......@@ -8889,67 +8722,34 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.46.7" expl="VC for div_sb_qr" proved="true">
<proof prover="2" timelimit="1" obsolete="true"><result status="unknown" time="2.09"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<transf name="split_goal_wp" proved="true" >
<goal name="VC div_sb_qr.46.7.0" expl="VC for div_sb_qr" proved="true">
<proof prover="0"><result status="valid" time="0.44"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1" obsolete="true"><result status="failure" time="0.00"/></proof>
</goal>