Commit a8c384af authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

reran proofs on sandor; removed a bit of fluff

parent 6b1b91ba
......@@ -800,7 +800,7 @@
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter asr.2" expl="postcondition">
<proof prover="8"><result status="valid" time="0.41"/></proof>
<proof prover="8"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="WP_parameter asr.3" expl="postcondition">
<proof prover="6"><result status="valid" time="0.03"/></proof>
......@@ -989,10 +989,10 @@
<proof prover="7"><result status="valid" time="1.70"/></proof>
</goal>
<goal name="uint_26" expl="">
<proof prover="7"><result status="valid" time="1.92"/></proof>
<proof prover="7"><result status="valid" time="1.62"/></proof>
</goal>
<goal name="uint_27" expl="">
<proof prover="7"><result status="valid" time="2.08"/></proof>
<proof prover="7"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="uint_28" expl="">
<proof prover="7"><result status="valid" time="2.25"/></proof>
......@@ -1007,7 +1007,7 @@
<proof prover="7"><result status="valid" time="2.77"/></proof>
</goal>
<goal name="uint_32" expl="">
<proof prover="6"><result status="valid" time="9.28"/></proof>
<proof prover="6"><result status="valid" time="8.09"/></proof>
</goal>
<goal name="WP_parameter uint_recursion" expl="VC for uint_recursion">
<transf name="split_goal_wp">
......@@ -1057,7 +1057,7 @@
<goal name="WP_parameter uint_bound.5" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter uint_bound.5.1" expl="assertion">
<proof prover="2"><result status="valid" time="7.22"/></proof>
<proof prover="2"><result status="valid" time="3.67"/></proof>
</goal>
</transf>
</goal>
......@@ -1125,7 +1125,7 @@
<proof prover="8"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter uint_eq.10" expl="postcondition">
<proof prover="6"><result status="valid" time="2.11"/></proof>
<proof prover="6"><result status="valid" time="1.79"/></proof>
</goal>
<goal name="WP_parameter uint_eq.11" expl="postcondition">
<proof prover="8"><result status="valid" time="0.16"/></proof>
......
......@@ -315,7 +315,7 @@
<goal name="WP_parameter bigint_mul256.45" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.45.1" expl="precondition">
<proof prover="0" timelimit="130" memlimit="8000"><result status="valid" time="0.58"/></proof>
<proof prover="0" timelimit="130" memlimit="8000"><result status="valid" time="0.41"/></proof>
</goal>
</transf>
</goal>
......@@ -329,7 +329,7 @@
<goal name="WP_parameter bigint_mul256.47" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.47.1" expl="precondition">
<proof prover="0" timelimit="130"><result status="valid" time="0.61"/></proof>
<proof prover="0" timelimit="130"><result status="valid" time="0.42"/></proof>
</goal>
</transf>
</goal>
......@@ -1152,7 +1152,7 @@
<goal name="WP_parameter bigint_mul256.168" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.168.1" expl="precondition">
<proof prover="0" timelimit="130" memlimit="8000"><result status="valid" time="0.91"/></proof>
<proof prover="0" timelimit="130" memlimit="8000"><result status="valid" time="0.70"/></proof>
</goal>
</transf>
</goal>
......@@ -1188,7 +1188,7 @@
<goal name="WP_parameter bigint_mul256.174" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.174.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.94"/></proof>
<proof prover="0"><result status="valid" time="0.71"/></proof>
</goal>
</transf>
</goal>
......@@ -1878,7 +1878,7 @@
<goal name="WP_parameter bigint_mul256.279" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.279.1" expl="assertion">
<proof prover="1" timelimit="130" memlimit="2000"><result status="valid" time="17.39"/></proof>
<proof prover="1" timelimit="130" memlimit="2000"><result status="valid" time="15.44"/></proof>
</goal>
</transf>
</goal>
......@@ -2164,7 +2164,7 @@
<goal name="WP_parameter bigint_mul256.324" expl="VC for bigint_mul256">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.324.1" expl="VC for bigint_mul256">
<proof prover="1" timelimit="300"><result status="valid" time="144.28"/></proof>
<proof prover="1" timelimit="300"><result status="valid" time="126.68"/></proof>
</goal>
</transf>
</goal>
......@@ -2190,14 +2190,14 @@
<goal name="WP_parameter bigint_mul256.326.1" expl="VC for bigint_mul256">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.326.1.1" expl="VC for bigint_mul256">
<proof prover="1"><result status="valid" time="3.57"/></proof>
<proof prover="1"><result status="valid" time="2.90"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_mul256.326.2" expl="VC for bigint_mul256">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.326.2.1" expl="VC for bigint_mul256">
<proof prover="1" timelimit="130"><result status="valid" time="3.80"/></proof>
<proof prover="1" timelimit="130"><result status="valid" time="3.31"/></proof>
</goal>
</transf>
</goal>
......@@ -2866,7 +2866,7 @@
<goal name="WP_parameter bigint_mul256.416" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.416.1" expl="precondition">
<proof prover="1"><result status="valid" time="2.75"/></proof>
<proof prover="1"><result status="valid" time="2.35"/></proof>
</goal>
</transf>
</goal>
......@@ -3021,14 +3021,14 @@
<goal name="WP_parameter bigint_mul256.436" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.436.1" expl="precondition">
<proof prover="1"><result status="valid" time="2.87"/></proof>
<proof prover="1"><result status="valid" time="2.39"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_mul256.437" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.437.1" expl="precondition">
<proof prover="1"><result status="valid" time="2.99"/></proof>
<proof prover="1"><result status="valid" time="2.45"/></proof>
</goal>
</transf>
</goal>
......@@ -3091,7 +3091,7 @@
<goal name="WP_parameter bigint_mul256.446" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.446.1" expl="precondition">
<proof prover="1"><result status="valid" time="4.04"/></proof>
<proof prover="1"><result status="valid" time="3.47"/></proof>
</goal>
</transf>
</goal>
......@@ -3204,7 +3204,7 @@
<goal name="WP_parameter bigint_mul256.460" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.460.1" expl="precondition">
<proof prover="1"><result status="valid" time="3.13"/></proof>
<proof prover="1"><result status="valid" time="2.70"/></proof>
</goal>
</transf>
</goal>
......@@ -3386,7 +3386,7 @@
<goal name="WP_parameter bigint_mul256.486" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_mul256.486.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.69"/></proof>
<proof prover="0"><result status="valid" time="1.41"/></proof>
</goal>
</transf>
</goal>
......
......@@ -241,7 +241,7 @@
<goal name="WP_parameter mul128.31.1" expl="VC for mul128">
<transf name="eliminate_if_term">
<goal name="WP_parameter mul128.31.1.1" expl="VC for mul128">
<proof prover="4" timelimit="60"><result status="valid" time="18.21"/></proof>
<proof prover="4" timelimit="60"><result status="valid" time="15.81"/></proof>
</goal>
</transf>
</goal>
......@@ -250,7 +250,7 @@
<goal name="WP_parameter mul128.32" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.32.1" expl="VC for mul128">
<proof prover="4" steplimit="-1"><result status="valid" time="8.10"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="7.02"/></proof>
</goal>
</transf>
</goal>
......@@ -264,21 +264,21 @@
<goal name="WP_parameter mul128.34" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.34.1" expl="VC for mul128">
<proof prover="4" steplimit="-1"><result status="valid" time="5.00"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="4.38"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.35" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.35.1" expl="assertion">
<proof prover="4" timelimit="30"><result status="valid" time="9.44"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="8.30"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.36" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.36.1" expl="assertion">
<proof prover="4" timelimit="50"><result status="valid" time="9.82"/></proof>
<proof prover="4" timelimit="50"><result status="valid" time="8.48"/></proof>
</goal>
</transf>
</goal>
......@@ -295,14 +295,14 @@
<goal name="WP_parameter mul128.38" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.38.1" expl="assertion">
<proof prover="4" timelimit="60" steplimit="1"><result status="valid" time="7.42"/></proof>
<proof prover="4" timelimit="60" steplimit="1"><result status="valid" time="6.45"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.39" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.39.1" expl="assertion">
<proof prover="4" timelimit="60"><result status="valid" time="7.75"/></proof>
<proof prover="4" timelimit="60"><result status="valid" time="6.85"/></proof>
</goal>
</transf>
</goal>
......@@ -311,7 +311,7 @@
<goal name="WP_parameter mul128.40.1" expl="VC for mul128">
<transf name="split_goal_wp">
<goal name="WP_parameter mul128.40.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="10.32"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="9.01"/></proof>
</goal>
<goal name="WP_parameter mul128.40.1.2" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="7.08"/></proof>
......@@ -653,7 +653,7 @@
<goal name="WP_parameter mul128.88" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.88.1" expl="VC for mul128">
<proof prover="4" steplimit="1"><result status="valid" time="32.45"/></proof>
<proof prover="4" steplimit="1"><result status="valid" time="28.16"/></proof>
</goal>
</transf>
</goal>
......@@ -782,7 +782,7 @@
<goal name="WP_parameter mul128.106.1" expl="VC for mul128">
<transf name="eliminate_if_term">
<goal name="WP_parameter mul128.106.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="58.90"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="52.04"/></proof>
</goal>
</transf>
</goal>
......@@ -812,35 +812,35 @@
<goal name="WP_parameter mul128.110" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.110.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="9.18"/></proof>
<proof prover="4"><result status="valid" time="8.12"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.111" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.111.1" expl="assertion">
<proof prover="4"><result status="valid" time="18.39"/></proof>
<proof prover="4"><result status="valid" time="16.13"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.112" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.112.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="14.12"/></proof>
<proof prover="4"><result status="valid" time="12.31"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.113" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.113.1" expl="assertion">
<proof prover="4" timelimit="300"><result status="valid" time="14.59"/></proof>
<proof prover="4" timelimit="300"><result status="valid" time="12.78"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.114" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.114.1" expl="assertion">
<proof prover="4"><result status="valid" time="14.55"/></proof>
<proof prover="4"><result status="valid" time="12.59"/></proof>
</goal>
</transf>
</goal>
......@@ -857,14 +857,14 @@
<goal name="WP_parameter mul128.116" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.116.1" expl="assertion">
<proof prover="4" memlimit="2000"><result status="valid" time="14.45"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="12.56"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.117" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.117.1" expl="assertion">
<proof prover="4" memlimit="2000"><result status="valid" time="14.44"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="12.57"/></proof>
</goal>
</transf>
</goal>
......@@ -1317,7 +1317,7 @@
<goal name="WP_parameter mul128.182.1" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.182.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="23.49"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="20.55"/></proof>
</goal>
</transf>
</goal>
......@@ -1328,7 +1328,7 @@
<goal name="WP_parameter mul128.183.1" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.183.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="30.57"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="26.70"/></proof>
</goal>
</transf>
</goal>
......@@ -1350,7 +1350,7 @@
<goal name="WP_parameter mul128.185.1" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.185.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="11.23"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="9.86"/></proof>
</goal>
</transf>
</goal>
......@@ -1366,14 +1366,14 @@
<goal name="WP_parameter mul128.187" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.187.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="21.72"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="19.08"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.188" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.188.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="21.97"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="19.12"/></proof>
</goal>
</transf>
</goal>
......@@ -1442,7 +1442,7 @@
<goal name="WP_parameter mul128.197" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.197.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="10.89"/></proof>
<proof prover="4"><result status="valid" time="9.61"/></proof>
</goal>
</transf>
</goal>
......@@ -1460,21 +1460,21 @@
<goal name="WP_parameter mul128.200" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.200.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="33.38"/></proof>
<proof prover="4"><result status="valid" time="28.98"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.201" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.201.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="36.68"/></proof>
<proof prover="4"><result status="valid" time="31.64"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mul128.202" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.202.1" expl="VC for mul128">
<proof prover="2"><result status="valid" time="8.38"/></proof>
<proof prover="2"><result status="valid" time="6.80"/></proof>
</goal>
</transf>
</goal>
......@@ -1488,7 +1488,7 @@
<goal name="WP_parameter mul128.204" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.204.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="16.56"/></proof>
<proof prover="4"><result status="valid" time="14.67"/></proof>
</goal>
</transf>
</goal>
......@@ -1505,7 +1505,7 @@
<goal name="WP_parameter mul128.207" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.207.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="18.60"/></proof>
<proof prover="4"><result status="valid" time="16.55"/></proof>
</goal>
</transf>
</goal>
......@@ -1522,7 +1522,7 @@
<goal name="WP_parameter mul128.210" expl="VC for mul128">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.210.1" expl="VC for mul128">
<proof prover="4"><result status="valid" time="6.23"/></proof>
<proof prover="4"><result status="valid" time="5.44"/></proof>
</goal>
</transf>
</goal>
......@@ -1549,7 +1549,7 @@
<goal name="WP_parameter mul128.214.1" expl="VC for mul128">
<transf name="eliminate_if">
<goal name="WP_parameter mul128.214.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="55.91"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="49.69"/></proof>
</goal>
</transf>
</goal>
......@@ -1586,7 +1586,7 @@
<goal name="WP_parameter mul128.219" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.219.1" expl="assertion">
<proof prover="4" timelimit="200" memlimit="2000"><result status="valid" time="42.39"/></proof>
<proof prover="4" timelimit="200" memlimit="2000"><result status="valid" time="37.57"/></proof>
</goal>
</transf>
</goal>
......@@ -1706,7 +1706,7 @@
<goal name="WP_parameter mul128.236.1" expl="VC for mul128">
<transf name="eliminate_if">
<goal name="WP_parameter mul128.236.1.1" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="15.92"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="13.50"/></proof>
</goal>
</transf>
</goal>
......@@ -1720,7 +1720,7 @@
<proof prover="4" memlimit="2000"><result status="valid" time="8.07"/></proof>
</goal>
<goal name="WP_parameter mul128.237.1.2" expl="VC for mul128">
<proof prover="4" memlimit="2000"><result status="valid" time="8.15"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="7.20"/></proof>
</goal>
</transf>
</goal>
......@@ -2055,7 +2055,7 @@
<goal name="WP_parameter mul128.285" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter mul128.285.1" expl="assertion">
<proof prover="4"><result status="valid" time="11.66"/></proof>
<proof prover="4"><result status="valid" time="10.30"/></proof>
</goal>
</transf>
</goal>
......
......@@ -599,7 +599,7 @@
<goal name="WP_parameter bigint_square256.82" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.82.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.69"/></proof>
<proof prover="2"><result status="valid" time="0.50"/></proof>
</goal>
</transf>
</goal>
......@@ -613,7 +613,7 @@
<goal name="WP_parameter bigint_square256.84" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.84.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.73"/></proof>
<proof prover="2"><result status="valid" time="0.55"/></proof>
</goal>
</transf>
</goal>
......@@ -669,7 +669,7 @@
<goal name="WP_parameter bigint_square256.92" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.92.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.91"/></proof>
<proof prover="2"><result status="valid" time="0.70"/></proof>
</goal>
</transf>
</goal>
......@@ -1680,7 +1680,7 @@
<goal name="WP_parameter bigint_square256.233" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.233.1" expl="precondition">
<proof prover="2"><result status="valid" time="4.41"/></proof>
<proof prover="2"><result status="valid" time="3.69"/></proof>
</goal>
</transf>
</goal>
......@@ -1773,7 +1773,7 @@
<goal name="WP_parameter bigint_square256.240.1" expl="precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter bigint_square256.240.1.1" expl="VC for bigint_square256">
<proof prover="2"><result status="valid" time="3.98"/></proof>
<proof prover="2"><result status="valid" time="3.41"/></proof>
</goal>
<goal name="WP_parameter bigint_square256.240.1.2" expl="VC for bigint_square256">
<proof prover="2"><result status="valid" time="3.15"/></proof>
......@@ -1787,7 +1787,7 @@
<goal name="WP_parameter bigint_square256.241.1" expl="precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter bigint_square256.241.1.1" expl="VC for bigint_square256">
<proof prover="2"><result status="valid" time="4.06"/></proof>
<proof prover="2"><result status="valid" time="3.51"/></proof>
</goal>
<goal name="WP_parameter bigint_square256.241.1.2" expl="VC for bigint_square256">
<proof prover="2"><result status="valid" time="3.29"/></proof>
......@@ -1801,7 +1801,7 @@
<goal name="WP_parameter bigint_square256.242.1" expl="precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter bigint_square256.242.1.1" expl="VC for bigint_square256">
<proof prover="2"><result status="valid" time="4.15"/></proof>
<proof prover="2"><result status="valid" time="3.60"/></proof>
</goal>
<goal name="WP_parameter bigint_square256.242.1.2" expl="VC for bigint_square256">
<proof prover="2"><result status="valid" time="3.42"/></proof>
......@@ -1988,7 +1988,7 @@
<goal name="WP_parameter bigint_square256.256" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.256.1" expl="precondition">
<proof prover="2"><result status="valid" time="4.61"/></proof>
<proof prover="2"><result status="valid" time="3.99"/></proof>
</goal>
</transf>
</goal>
......@@ -2002,7 +2002,7 @@
<goal name="WP_parameter bigint_square256.258" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.258.1" expl="precondition">
<proof prover="2"><result status="valid" time="4.79"/></proof>
<proof prover="2"><result status="valid" time="4.07"/></proof>
</goal>
</transf>
</goal>
......@@ -2486,7 +2486,7 @@
<goal name="WP_parameter bigint_square256.326" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_square256.326.1" expl="postcondition">
<proof prover="4" timelimit="30"><result status="valid" time="7.42"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="6.51"/></proof>
</goal>
</transf>
</goal>
......
......@@ -100,7 +100,7 @@
<goal name="WP_parameter sqr128.11" expl="VC for sqr128">
<transf name="compute_in_goal">
<goal name="WP_parameter sqr128.11.1" expl="VC for sqr128">
<proof prover="2" timelimit="300"><result status="valid" time="47.78"/></proof>
<proof prover="2" timelimit="300"><result status="valid" time="40.51"/></proof>
</goal>
</transf>
</goal>
......@@ -456,7 +456,7 @@
<goal name="WP_parameter sqr128.64" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter sqr128.64.1" expl="assertion">
<proof prover="2" timelimit="30"><result status="valid" time="18.23"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="16.28"/></proof>
</goal>
</transf>
</goal>
......
(*
general TODO:
- memory stack invariance
labels to investigate
'AD
'Q1
*)
module AVRcode
use import avrmodel.AVRint
......
......@@ -48,7 +48,7 @@
<proof prover="0"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.13" expl="precondition">
<proof prover="0"><result status="valid" time="0.37"/></proof>
<proof prover="0"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.14" expl="precondition">
<proof prover="0"><result status="valid" time="0.27"/></proof>
......@@ -111,7 +111,7 @@
<proof prover="0"><result status="valid" time="57.56"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.34" expl="VC for bigint_subp">
<proof prover="0"><result status="valid" time="0.89"/></proof>
<proof prover="0"><result status="valid" time="0.68"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.35" expl="VC for bigint_subp">
<proof prover="0"><result status="valid" time="0.33"/></proof>
......@@ -147,10 +147,10 @@
<proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.46" expl="precondition">
<proof prover="0"><result status="valid" time="0.44"/></proof>
<proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.47" expl="precondition">
<proof prover="0"><result status="valid" time="0.44"/></proof>
<proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.1.48" expl="precondition">
<proof prover="0"><result status="valid" time="0.41"/></proof>
......
......@@ -483,7 +483,7 @@
<goal name="WP_parameter add31_cf_to_z.1.64" expl="postcondition">
<transf name="introduce_premises">
<goal name="WP_parameter add31_cf_to_z.1.64.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.82"/></proof>
<proof prover="0"><result status="valid" time="0.63"/></proof>
</goal>
</transf>
</goal>
......