Commit 14bfd09c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update obsolete sessions

parent b6ee1be5
......@@ -14,7 +14,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="a953b8e11e9f21bbfb9646867928ce58" expanded="true">
<theory name="BinarySearchInt32" sum="1ae28c49a2dbfd082c313f20f784c903" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="3"><result status="valid" time="2.52" steps="3682"/></proof>
</goal>
......
......@@ -97,7 +97,7 @@
</transf>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="f8439b7727009b247777048bf19a45ff" expanded="true">
<theory name="BinarySearchInt32" sum="0ffe15153f7e23ef8f6eea186bc06455" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="1. integer overflow">
......
......@@ -25,7 +25,7 @@
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="Utils_Spec" sum="6345ccfa2883bdeaaf4ded7d4c84b2c3">
<theory name="Utils_Spec" sum="5c30c8b3fe01ee8eecd7195fb9ef1238">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -66,7 +66,7 @@
<proof prover="7" timelimit="1"><result status="valid" time="0.56" steps="490"/></proof>
</goal>
<goal name="VC countSpec_Aux.2.2" expl="2. assertion">
<proof prover="1" timelimit="1"><result status="valid" time="0.27"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC countSpec_Aux.2.3" expl="3. assertion">
<proof prover="7" timelimit="1"><result status="valid" time="0.90" steps="543"/></proof>
......@@ -102,7 +102,7 @@
<proof prover="1"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC numof_or" expl="VC for numof_or">
<proof prover="1"><result status="valid" time="0.48"/></proof>
<proof prover="1"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="VC triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
......
......@@ -174,7 +174,7 @@
<proof prover="4"><result status="valid" time="0.79" steps="849"/></proof>
</goal>
</theory>
<theory name="BoundedIntegers" sum="a39bfb3d75b76fa467d963fc9a78a509">
<theory name="BoundedIntegers" sum="6eefdd2be3fbd510aa7ca7337821f54c">
<goal name="VC maximum_subarray" expl="VC for maximum_subarray">
<transf name="split_goal_wp">
<goal name="VC maximum_subarray.1" expl="1. loop invariant init">
......@@ -202,7 +202,7 @@
<proof prover="4"><result status="valid" time="0.06" steps="130"/></proof>
</goal>
<goal name="VC maximum_subarray.9" expl="9. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.50"/></proof>
<proof prover="5"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC maximum_subarray.10" expl="10. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.01" steps="31"/></proof>
......@@ -248,7 +248,7 @@
<proof prover="4"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="VC maximum_subarray.24" expl="24. loop invariant preservation">
<proof prover="5"><result status="valid" time="1.39"/></proof>
<proof prover="5"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="VC maximum_subarray.25" expl="25. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.01" steps="31"/></proof>
......
......@@ -69,6 +69,7 @@ run_dir double_wp "-L double_wp"
echo ""
echo "Score on ported programs : $success/$total"
echo ""
echo "=== Programs that remain to be ported ==="
run_dir to_port
......
......@@ -106,7 +106,7 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm63" sum="f64eaee885c2c0c2efa1917cecd2eaf2" expanded="true">
<theory name="EuclideanAlgorithm63" sum="40b32678ce74c347e73fb0ee700b3141" expanded="true">
<goal name="VC euclid" expl="VC for euclid" expanded="true">
</goal>
</theory>
......
......@@ -81,7 +81,7 @@
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="NQueens63" sum="07bf68afba2087cf180f35df40fc44f2">
<theory name="NQueens63" sum="fb46c7df3e4775fb14cde4f78d9db07a">
<goal name="VC check_is_consistent" expl="VC for check_is_consistent">
<proof prover="4"><result status="valid" time="0.36" steps="1142"/></proof>
</goal>
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../vstte12_two_way_sort.mlw">
<theory name="TwoWaySort" sum="9a53098fb91916babf96119c5dd734f6">
<theory name="TwoWaySort" sum="4afbe380f122290492cf67cd26b1b083">
<goal name="VC two_way_sort" expl="VC for two_way_sort">
<proof prover="0"><result status="valid" time="0.09" steps="365"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="363"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,17 +4,17 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../zeros.mlw" expanded="true">
<theory name="SetZeros" sum="b136046decfdee48dc5fb7f0d626f0d7" expanded="true">
<theory name="SetZeros" sum="58fcdb93939b6b2c3a5da96b5e9510e5" expanded="true">
<goal name="VC set_zeros" expl="VC for set_zeros" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="40"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="38"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
</theory>
<theory name="AllZeros" sum="627ccf550fb2bcf01aa3e45a5abeabf8" expanded="true">
<theory name="AllZeros" sum="ba9bdb0ddec80941daaf1170a6557f1f" expanded="true">
<goal name="VC all_zeros1" expl="VC for all_zeros1" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="85"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="117"/></proof>
</goal>
<goal name="VC all_zeros2" expl="VC for all_zeros2" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="76"/></proof>
......
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