Commit 8c1a6b32 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Update sessions

parent 360d029a
......@@ -150,10 +150,10 @@
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sprod.2" expl="exceptional postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
......@@ -1131,7 +1131,7 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.11" expl="precondition" proved="true">
......@@ -1141,24 +1141,24 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="VC linear_decision.15" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.19" expl="assertion" proved="true">
......@@ -1196,10 +1196,10 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.30" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.31" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.32" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -1223,17 +1223,17 @@
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="VC linear_decision.39" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.40" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.41" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
......@@ -1263,18 +1263,18 @@
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.52" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.53" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.54" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.55" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.56" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -1316,19 +1316,19 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.70" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.71" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.72" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......
......@@ -5283,7 +5283,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
assert { value (xd at SmallDiv) sy =
vlx + power radix (sy - 2) * xp0
+ power radix (sy - 1) * xp1 }; (*nonlinear*)
assert { value (x at SubProd) (sy + (!i at StartLoop) - 1) = value (x at SubProd) !i + power radix !i * value (xd at SubProd) sy };
assert { value (x at SubProd) (sy + (!i at StartLoop) - 1)
= value (x at SubProd) !i + power radix !i * value (xd at SubProd) sy };
assert { value (old x) sx =
(value !qp (sx - sy - !i)
+ qh * power radix (sx - sy - !i))
......
......@@ -3085,7 +3085,7 @@
<proof prover="3"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="VC addmul_limbs.36.0.0.0.0.0.2" proved="true">
<proof prover="3"><result status="valid" time="0.57"/></proof>
<proof prover="3"><result status="valid" time="0.80"/></proof>
</goal>
</transf>
</goal>
......@@ -9307,7 +9307,7 @@
<goal name="VC div_sb_qr.149.0.0.0.0.0" expl="assertion" proved="true">
<transf name="rewrite" proved="true" arg1="y_val112">
<goal name="VC div_sb_qr.149.0.0.0.0.0.0" expl="assertion" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.20"/></proof>
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="1.67"/></proof>
</goal>
</transf>
</goal>
......@@ -9321,7 +9321,7 @@
<proof prover="2" timelimit="1"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC div_sb_qr.149.0.2" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.49"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.24"/></proof>
</goal>
</transf>
</goal>
......@@ -9436,7 +9436,7 @@
<goal name="VC div_sb_qr.155.0.0.0.0.0" expl="postcondition" proved="true">
<transf name="rewrite" proved="true" arg1="y_val120">
<goal name="VC div_sb_qr.155.0.0.0.0.0.0" expl="postcondition" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="1.75"/></proof>
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="1.40"/></proof>
</goal>
</transf>
</goal>
......@@ -10572,16 +10572,16 @@
</goal>
<goal name="VC div_sb_qr.227.0.2" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.25"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="timeout" time="1.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>
</goal>
<goal name="VC div_sb_qr.227.0.3" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.21"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
<proof prover="9" timelimit="1"><result status="timeout" time="0.98"/></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.98"/></proof>
</goal>
<goal name="VC div_sb_qr.226.0.4">
<proof prover="3"><undone/></proof>
<proof prover="3"><result status="failure" time="0.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