Commit 5c35938d authored by Andrei Paskevich's avatar Andrei Paskevich

upgrade to Alt-Ergo 2.0.0, CVC4 1.5, Z3 4.6.0, Eprover 2.0 where possible

parent 2c0ebae6
......@@ -2,23 +2,23 @@
<!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="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw" proved="true">
<theory name="AddListRec" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="92"/></proof>
</goal>
<goal name="VC main" expl="VC for main" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main" expl="VC for main" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
This diff is collapsed.
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" proved="true">
<theory name="Algo64" proved="true">
<goal name="VC quicksort" expl="VC for quicksort" proved="true">
<proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof>
<proof prover="1"><result status="valid" time="0.67" steps="1799"/></proof>
</goal>
<goal name="VC qs" expl="VC for qs" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="57"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" proved="true">
<theory name="Algo65" proved="true">
<goal name="VC find" expl="VC for find" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="1688"/></proof>
<proof prover="1"><result status="valid" time="0.52" steps="1756"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" proved="true">
<theory name="AllDistinct" proved="true">
<goal name="VC all_distinct" expl="VC for all_distinct" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="270"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="263"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,19 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" proved="true">
<theory name="M" proved="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="135"/></proof>
<proof prover="1"><result status="valid" time="0.11" steps="137"/></proof>
</goal>
</theory>
<theory name="InsertionSortExample" proved="true">
<goal name="VC path_init_l2" expl="VC for path_init_l2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="22"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="VC path_l2_exit" expl="VC for path_l2_exit" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,16 +2,16 @@
<!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="10" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw" proved="true">
<theory name="Sum" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
</theory>
<theory name="Division" proved="true">
<goal name="VC division" expl="VC for division" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,19 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../balance.mlw" proved="true">
<theory name="Puzzle8" proved="true">
<goal name="VC solve3" expl="VC for solve3" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="47"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
<goal name="VC solve8" expl="VC for solve8" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="291"/></proof>
<proof prover="1"><result status="valid" time="0.13" steps="267"/></proof>
</goal>
</theory>
<theory name="Puzzle12" proved="true">
<goal name="VC solve12" expl="VC for solve12" proved="true">
<proof prover="0"><result status="valid" time="0.53" steps="1379"/></proof>
<proof prover="1"><result status="valid" time="0.53" steps="1204"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bellman_ford.mlw" proved="true">
<theory name="Graph" proved="true">
<goal name="VC s" expl="VC for s" proved="true">
......@@ -37,7 +37,7 @@
<goal name="long_path_reduction" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="long_path_reduction.0" proved="true">
<proof prover="11"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="long_path_reduction.1" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
......@@ -174,7 +174,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="VC relax.0.2" expl="VC for relax" proved="true">
<proof prover="11"><result status="valid" time="0.54"/></proof>
<proof prover="0"><result status="valid" time="0.91"/></proof>
</goal>
<goal name="VC relax.0.3" expl="VC for relax" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="117"/></proof>
......@@ -294,7 +294,7 @@
<goal name="VC bellman_ford.0.0.0" expl="loop invariant init" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC bellman_ford.0.0.0.0" expl="loop invariant init" proved="true">
<proof prover="11"><result status="valid" time="0.19"/></proof>
<proof prover="0"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC bellman_ford.0.0.0.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
......@@ -375,7 +375,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="164"/></proof>
</goal>
<goal name="VC bellman_ford.12.6" expl="VC for bellman_ford" proved="true">
<proof prover="1"><result status="valid" time="0.34" steps="672"/></proof>
<proof prover="1"><result status="valid" time="0.20" steps="672"/></proof>
</goal>
<goal name="VC bellman_ford.12.7" expl="VC for bellman_ford" proved="true">
<proof prover="1"><result status="valid" time="0.14" steps="239"/></proof>
......
......@@ -2,11 +2,11 @@
<!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="10" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" proved="true">
<theory name="BinaryMultiplication" proved="true">
<goal name="VC binary_mult" expl="VC for binary_mult" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="49"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="63"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,32 +2,31 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_search.mlw" proved="true">
<theory name="BinarySearch" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="0.05" steps="88"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="132"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchBranchless" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="218"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="1.27" steps="8288"/></proof>
<proof prover="0"><result status="valid" time="2.65" steps="9890"/></proof>
</goal>
</theory>
<theory name="BinarySearchBoolean" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="194"/></proof>
<proof prover="0"><result status="valid" time="0.08" steps="245"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,10 +4,10 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" proved="true">
<theory name="BinarySort" proved="true">
<goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
<proof prover="0"><result status="valid" time="0.54"/></proof>
<file name="../binary_sort.mlw">
<theory name="BinarySort">
<goal name="VC occ_shift" expl="VC for occ_shift">
<proof prover="0" obsolete="true"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC binary_sort" expl="VC for binary_sort" proved="true">
<transf name="split_vc" proved="true" >
......
......@@ -2,51 +2,51 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_sqrt.mlw" proved="true">
<theory name="BinarySqrt" proved="true">
<goal name="VC sqrt" expl="VC for sqrt" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC sqrt.0" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC sqrt.1" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sqrt.2" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC sqrt.3" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC sqrt.4" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="27"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC sqrt.5" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC sqrt.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC sqrt.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC sqrt.8" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.22" steps="135"/></proof>
<proof prover="3"><result status="valid" time="0.22" steps="135"/></proof>
</goal>
<goal name="VC sqrt.9" expl="postcondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC sqrt.9.0" expl="VC for sqrt" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC sqrt.9.1" expl="VC for sqrt" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC sqrt.9.1.0" expl="VC for sqrt" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sqrt.9.1.1" expl="VC for sqrt" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.00" steps="16"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
</transf>
</goal>
......@@ -55,7 +55,7 @@
</transf>
</goal>
<goal name="VC sqrt_main" expl="VC for sqrt_main" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,12 +3,11 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" proved="true">
<theory name="Test_proofinuse" proved="true">
<goal name="VC shift_is_div" expl="VC for shift_is_div" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="117"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="117"/></proof>
</goal>
<goal name="VC mask" expl="VC for mask" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -150,10 +149,10 @@
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_ule" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="72"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="72"/></proof>
</goal>
<goal name="to_int_ult" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="72"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="bv32_bounds_0" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -182,10 +181,10 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add.6" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="137"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="138"/></proof>
</goal>
<goal name="VC add.7" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.36" steps="2847"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.16" steps="267"/></proof>
</goal>
<goal name="VC add.8" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
......
This diff is collapsed.
......@@ -3,14 +3,14 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bresenham.mlw" proved="true">
<theory name="M" proved="true">
<goal name="closest" proved="true">
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC bresenham" expl="VC for bresenham" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="70"/></proof>
<proof prover="1"><result status="valid" time="0.12" steps="70"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,96 +2,96 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bubble_sort.mlw" proved="true">
<theory name="BubbleSort" proved="true">
<goal name="VC bubble_sort" expl="VC for bubble_sort" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC bubble_sort.0" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC bubble_sort.1" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC bubble_sort.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC bubble_sort.3" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC bubble_sort.4" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC bubble_sort.5" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="19"/></proof>
</goal>
<goal name="VC bubble_sort.6" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC bubble_sort.7" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC bubble_sort.8" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC bubble_sort.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC bubble_sort.10" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="151"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="220"/></proof>
</goal>
<goal name="VC bubble_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="179"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="177"/></proof>
</goal>
<goal name="VC bubble_sort.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="383"/></proof>
<proof prover="1"><result status="valid" time="0.18" steps="391"/></proof>
</goal>
<goal name="VC bubble_sort.13" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="103"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="112"/></proof>
</goal>
<goal name="VC bubble_sort.14" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC bubble_sort.15" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC bubble_sort.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="31"/></proof>
</goal>
<goal name="VC bubble_sort.17" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC bubble_sort.18" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC bubble_sort.19" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="42"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
</goal>
<goal name="VC bubble_sort.20" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC bubble_sort.21" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC bubble_sort.22" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC bubble_sort.23" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC bubble_sort.24" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC test2" expl="VC for test2" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="40"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
</goal>
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,14 +2,14 @@
<!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="10" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../checking_a_large_routine.mlw" proved="true">
<theory name="CheckingALargeRoutine" proved="true">
<goal name="VC routine" expl="VC for routine" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC routine2" expl="VC for routine2" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,30 +2,30 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count_list.mlw" expanded="true">
<theory name="CoincidenceCount" sum="5a4dc27c2f8f9d2b3e530dad4453a106" expanded="true">
<goal name="Transitive.Trans" expl="" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count_list.mlw" proved="true">
<theory name="CoincidenceCount" proved="true">
<goal name="Transitive.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC coincidence_count" expl="VC for coincidence_count" expanded="true">
<proof prover="2"><result status="valid" time="2.20" steps="9859"/></proof>
<goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
<proof prover="0"><result status="valid" time="2.20" steps="9039"/></proof>
</goal>
</theory>
<theory name="CoincidenceCountAnyType" sum="b39ec7c4324a1482358d394d40b938dd" expanded="true">
<goal name="Transitive.Trans" expl="" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<theory name="CoincidenceCountAnyType" proved="true">
<goal name="Transitive.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC coincidence_count" expl="VC for coincidence_count">
<proof prover="2"><result status="valid" time="0.65" steps="4194"/></proof>
<goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
<proof prover="0"><result