Commit f3e3cf55 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

replay some obsolete sessions

parent cd6f6f82
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tree_of_array.mlw" expanded="true">
<theory name="TreeOfArray" sum="8373eb09557f090cd5d424929bc33f4e" expanded="true">
<theory name="TreeOfArray" sum="ceb158ee461d93483317cf8cff23a810" expanded="true">
<goal name="VC tree_of_array_aux" expl="VC for tree_of_array_aux" expanded="true">
<proof prover="0"><result status="valid" time="1.46" steps="1359"/></proof>
<proof prover="0"><result status="valid" time="1.17" steps="1359"/></proof>
</goal>
<goal name="VC tree_of_array" expl="VC for tree_of_array" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
......
......@@ -4,12 +4,12 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw" expanded="true">
<theory name="TreeOfList" sum="6f055985d39134853f51e6a9d10c6079" expanded="true">
<theory name="TreeOfList" sum="416c0b668112951fca2f111d21fa0791" expanded="true">
<goal name="VC tree_of_list_aux" expl="VC for tree_of_list_aux">
<proof prover="1"><result status="valid" time="0.73" steps="1452"/></proof>
</goal>
<goal name="VC tree_of_list" expl="VC for tree_of_list">
<proof prover="1"><result status="valid" time="0.02" steps="108"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
</theory>
</file>
......
......@@ -42,12 +42,12 @@
</transf>
</goal>
</theory>
<theory name="GilbreathCardTrick" sum="b9e9444a9b101531b521cbdb014cfa87">
<theory name="GilbreathCardTrick" sum="c022cadfb1b8213da58f67c08242580d">
<goal name="VC shuffle" expl="VC for shuffle">
<proof prover="1"><result status="valid" time="2.17" steps="3619"/></proof>
</goal>
<goal name="VC card_trick" expl="VC for card_trick">
<proof prover="1"><result status="valid" time="0.16" steps="607"/></proof>
<proof prover="1"><result status="valid" time="0.16" steps="552"/></proof>
</goal>
</theory>
</file>
......
......@@ -14,7 +14,7 @@
</theory>
<theory name="Graph_sig" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="BuildMaze" sum="88150c56d76e8d94e5c39e5e3558d5e3" expanded="true">
<theory name="BuildMaze" sum="719843e55d9634d80b05ce9546a43834" expanded="true">
<goal name="Ineq1" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="Ineq1.1" expl="1.">
......@@ -346,7 +346,7 @@
<proof prover="1"><result status="valid" time="0.12" steps="506"/></proof>
</goal>
<goal name="VC build_maze" expl="VC for build_maze" expanded="true">
<proof prover="1"><result status="valid" time="0.35" steps="778"/></proof>
<proof prover="1" timelimit="60" memlimit="3000"><result status="valid" time="0.79" steps="697"/></proof>
</goal>
</theory>
</file>
......
......@@ -5,15 +5,15 @@
<prover id="2" 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"/>
<file name="../vacid_0_sparse_array.mlw" expanded="true">
<theory name="SparseArray" sum="549afd3ab706382e3916fec804ac2671" expanded="true">
<theory name="SparseArray" sum="61ac12b09d5b4441dd1a6ef4fa4ab1e6" expanded="true">
<goal name="VC create" expl="VC for create">
<proof prover="2"><result status="valid" time="0.00" steps="25"/></proof>
</goal>
<goal name="VC test" expl="VC for test">
<proof prover="2"><result status="valid" time="0.02" steps="34"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC get" expl="VC for get">
<proof prover="2"><result status="valid" time="0.01" steps="30"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="permutation">
<transf name="split_goal_wp">
......@@ -31,22 +31,22 @@
<goal name="VC set" expl="VC for set">
<transf name="split_goal_wp">
<goal name="VC set.1" expl="1. index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC set.2" expl="2. type invariant">
<proof prover="2"><result status="valid" time="0.08" steps="249"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="255"/></proof>
</goal>
<goal name="VC set.3" expl="3. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="21"/></proof>
</goal>
<goal name="VC set.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.08" steps="145"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="171"/></proof>
</goal>
<goal name="VC set.5" expl="5. index in array bounds">
<proof prover="2"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC set.6" expl="6. index in array bounds">
<proof prover="2"><result status="valid" time="0.02" steps="56"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="VC set.7" expl="7. type invariant">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -54,20 +54,20 @@
<goal name="VC set.8" expl="8. postcondition">
<transf name="split_goal_wp">
<goal name="VC set.8.1" expl="1. VC for set">
<proof prover="2"><result status="valid" time="0.04" steps="119"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="123"/></proof>
</goal>
<goal name="VC set.8.2" expl="2. VC for set">
<proof prover="2"><result status="valid" time="0.43" steps="527"/></proof>
<proof prover="2"><result status="valid" time="1.12" steps="550"/></proof>
</goal>
</transf>
</goal>
<goal name="VC set.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.06" steps="105"/></proof>
<proof prover="2"><result status="valid" time="0.06" steps="104"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Harness" sum="2eb3b69ff9e134fa8ed2deedc8c15672" expanded="true">
<theory name="Harness" sum="6729282620a564e10dbaa46c8cef1fd0" expanded="true">
<goal name="VC default" expl="VC for default">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -78,7 +78,7 @@
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness">
<proof prover="2"><result status="valid" time="0.60" steps="2246"/></proof>
<proof prover="2"><result status="valid" time="1.01" steps="2039"/></proof>
</goal>
<goal name="VC bench" expl="VC for bench">
<proof prover="2"><result status="valid" time="0.02" steps="172"/></proof>
......
......@@ -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="4afbe380f122290492cf67cd26b1b083">
<theory name="TwoWaySort" sum="9a53098fb91916babf96119c5dd734f6">
<goal name="VC two_way_sort" expl="VC for two_way_sort">
<proof prover="0"><result status="valid" time="0.09" steps="363"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="365"/></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="58fcdb93939b6b2c3a5da96b5e9510e5" expanded="true">
<theory name="SetZeros" sum="b136046decfdee48dc5fb7f0d626f0d7" expanded="true">
<goal name="VC set_zeros" expl="VC for set_zeros" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="38"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="40"/></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="ba9bdb0ddec80941daaf1170a6557f1f" expanded="true">
<theory name="AllZeros" sum="627ccf550fb2bcf01aa3e45a5abeabf8" expanded="true">
<goal name="VC all_zeros1" expl="VC for all_zeros1" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="117"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="85"/></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