Commit 54190a07 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 04189cd4
......@@ -14,9 +14,9 @@
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="1ae28c49a2dbfd082c313f20f784c903" expanded="true">
<theory name="BinarySearchInt32" sum="b34d4c5433527516ec6c219a31652ac1" 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>
<proof prover="3"><result status="valid" time="3.03" steps="3682"/></proof>
</goal>
</theory>
<theory name="BinarySearchBoolean" sum="a3018fd5a00da6568cce022e1cf9030a" expanded="true">
......
......@@ -97,7 +97,7 @@
</transf>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="0ffe15153f7e23ef8f6eea186bc06455" expanded="true">
<theory name="BinarySearchInt32" sum="62b7dad9a854fd61d39dff3098f7e86e" 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">
......
......@@ -9,7 +9,7 @@
<prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="8" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../bitcount.mlw" expanded="true">
<theory name="BitCount8bit_fact" sum="aa8761342879ed0c81e4166b0122b949">
<theory name="BitCount8bit_fact" sum="500c5b98a2d57ca4b380a85013c2abdb">
<goal name="nth_as_bv_is_int">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.08"/></proof>
......@@ -110,7 +110,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC step2.5.5" expl="5. assertion">
<proof prover="2"><result status="valid" time="2.83"/></proof>
<proof prover="2"><result status="valid" time="3.85"/></proof>
</goal>
</transf>
</goal>
......@@ -234,7 +234,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" sum="353887c84db3e6de1766f3b9ac2e231c">
<theory name="BitCounting32" sum="7b34d8d609d6c7e5175ba342d79b4460">
<goal name="VC proof0" expl="VC for proof0">
<transf name="split_goal_wp">
<goal name="VC proof0.1" expl="1. assertion">
......@@ -334,7 +334,7 @@
</goal>
<goal name="VC proof1.7.3" expl="3. VC for proof1">
<proof prover="3"><result status="valid" time="0.04" steps="92"/></proof>
<proof prover="5"><result status="valid" time="0.93"/></proof>
<proof prover="5"><result status="valid" time="1.24"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="93"/></proof>
</goal>
</transf>
......@@ -507,7 +507,7 @@
<proof prover="3"><result status="valid" time="0.05" steps="113"/></proof>
<proof prover="5"><result status="valid" time="0.10"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="109"/></proof>
<proof prover="8"><result status="valid" time="0.52"/></proof>
<proof prover="8"><result status="valid" time="0.71"/></proof>
</goal>
<goal name="VC proof3.10" expl="10. assertion">
<proof prover="2"><result status="valid" time="0.12"/></proof>
......@@ -522,7 +522,7 @@
<goal name="VC proof3.12" expl="12. assertion">
<transf name="split_goal_wp">
<goal name="VC proof3.12.1" expl="1. VC for proof3">
<proof prover="1"><result status="valid" time="1.86"/></proof>
<proof prover="1"><result status="valid" time="2.19"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="96"/></proof>
<proof prover="5"><result status="valid" time="0.10"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="97"/></proof>
......@@ -700,28 +700,28 @@
</transf>
</goal>
</theory>
<theory name="Hamming" sum="1ee0ba3bf19ff4a370d0a92d324593ab">
<theory name="Hamming" sum="d0a37aeeb2127daaac672243e9ec1776">
<goal name="VC hammingD" expl="VC for hammingD">
<transf name="split_goal_wp">
<goal name="VC hammingD.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="0.80" steps="423"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="2.72" steps="516"/></proof>
<proof prover="6"><result status="valid" time="3.18" steps="516"/></proof>
</goal>
<goal name="VC hammingD.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="1.12" steps="837"/></proof>
<proof prover="6"><result status="valid" time="1.40" steps="837"/></proof>
</goal>
</transf>
</goal>
<goal name="symmetric">
<proof prover="1"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="3.41" steps="2722"/></proof>
<proof prover="3"><result status="valid" time="4.03" steps="2722"/></proof>
<proof prover="6"><result status="valid" time="0.39" steps="591"/></proof>
</goal>
<goal name="numof_ytpmE">
<proof prover="2"><result status="valid" time="1.15"/></proof>
<proof prover="5"><result status="valid" time="1.21"/></proof>
<proof prover="2"><result status="valid" time="1.59"/></proof>
<proof prover="5"><result status="valid" time="1.58"/></proof>
</goal>
<goal name="VC separation" expl="VC for separation">
<transf name="split_goal_wp">
......@@ -750,7 +750,7 @@
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.34"/></proof>
<proof prover="5"><result status="valid" time="0.39"/></proof>
<proof prover="6"><result status="valid" time="2.54" steps="1626"/></proof>
<proof prover="6"><result status="valid" time="3.05" steps="1626"/></proof>
</goal>
<goal name="VC triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
......@@ -765,7 +765,7 @@
<proof prover="8"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC triangleInequalityInt.1.2" expl="2. VC for triangleInequalityInt">
<proof prover="2" timelimit="10"><result status="valid" time="5.60"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="8.00"/></proof>
</goal>
</transf>
</goal>
......@@ -775,7 +775,7 @@
<proof prover="3"><result status="valid" time="0.03" steps="80"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
<proof prover="8"><result status="valid" time="0.58"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
</transf>
</goal>
......@@ -788,7 +788,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="AsciiCode" sum="808d836999eb2e2981008f2dbc314a46">
<theory name="AsciiCode" sum="967d4a4d706fcf243c564a17b160ce27">
<goal name="VC bv_even" expl="VC for bv_even">
<transf name="split_goal_wp">
<goal name="VC bv_even.1" expl="1. assertion">
......@@ -806,7 +806,7 @@
<goal name="VC bv_even.4" expl="4. assertion">
<transf name="split_goal_wp">
<goal name="VC bv_even.4.1" expl="1. VC for bv_even">
<proof prover="6"><result status="valid" time="1.43" steps="1341"/></proof>
<proof prover="6"><result status="valid" time="1.69" steps="1341"/></proof>
</goal>
<goal name="VC bv_even.4.2" expl="2. VC for bv_even">
<proof prover="6"><result status="valid" time="0.06" steps="142"/></proof>
......@@ -847,7 +847,7 @@
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC count_or.4" expl="4. assertion">
<proof prover="5"><result status="valid" time="2.04"/></proof>
<proof prover="5"><result status="valid" time="2.80"/></proof>
</goal>
<goal name="VC count_or.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -911,12 +911,12 @@
<goal name="VC ascii.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="5"><result status="valid" time="1.46"/></proof>
<proof prover="5"><result status="valid" time="1.98"/></proof>
</goal>
<goal name="VC ascii.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="148"/></proof>
<proof prover="5"><result status="valid" time="0.54"/></proof>
<proof prover="5"><result status="valid" time="0.72"/></proof>
<proof prover="6"><result status="valid" time="0.18" steps="211"/></proof>
</goal>
</transf>
......@@ -940,7 +940,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC tmp.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.70"/></proof>
<proof prover="1"><result status="valid" time="0.90"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="56dbf919cc4930dbaacdba6442726774">
<theory name="Test_proofinuse" sum="ab6cb21974d9dad55465526025aab172">
<goal name="VC shift_is_div" expl="VC for shift_is_div">
<proof prover="1" timelimit="1"><result status="valid" time="0.11" steps="111"/></proof>
</goal>
......@@ -20,7 +20,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="041513d729f25a9829ccf37998908999">
<theory name="Hackers_delight" sum="d7d08def57656cb9ef83aa6883f38e90">
<goal name="DM1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -79,7 +79,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="314d43f81abd2e8ef023a2e67dbc4103">
<theory name="Hackers_delight_mod" sum="34c7dfce28597643e7ba84a66a3e0375">
<goal name="VC dm1" expl="VC for dm1">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -141,7 +141,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="5d131d7f925510a25cf8bd5fa3d623d2">
<theory name="Test_imperial_violet" sum="f4860878663ae0ea64a6e9bc49f62882">
<goal name="bv32_bounds_bv">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -181,7 +181,7 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC add.8" expl="8. loop invariant preservation">
<proof prover="1" timelimit="1"><result status="valid" time="1.10" steps="647"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="1.35" steps="647"/></proof>
</goal>
<goal name="VC add.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......@@ -192,7 +192,7 @@
</transf>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="0fa4262a9f3e0cb284583810b9d600ff">
<theory name="Test_from_bitvector_example" sum="40ae1afdbc21aa5df46dd4066990745d">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -7,25 +7,25 @@
<prover id="5" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="a00cfd18735acebdc89dfc4930ac5fb2" expanded="true">
<theory name="TestNegAsXOR" sum="bad680d63e71d3ee2f7ffa0141d4af0f" expanded="true">
<goal name="Nth_j">
<proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="sign_of_j">
<proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="3"><result status="valid" time="2.82"/></proof>
<proof prover="3"><result status="valid" time="3.55"/></proof>
</goal>
<goal name="mantissa_of_j">
<proof prover="1"><result status="valid" time="0.16" steps="121"/></proof>
<proof prover="3"><result status="valid" time="0.85"/></proof>
<proof prover="3"><result status="valid" time="1.12"/></proof>
<proof prover="5"><result status="valid" time="2.61"/></proof>
<proof prover="9"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="exp_of_j">
<proof prover="1"><result status="valid" time="0.17" steps="122"/></proof>
<proof prover="3"><result status="valid" time="0.82"/></proof>
<proof prover="3"><result status="valid" time="1.08"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.63"/></proof>
<proof prover="9"><result status="valid" time="0.73"/></proof>
<proof prover="9"><result status="valid" time="0.91"/></proof>
</goal>
<goal name="int_of_bv">
<proof prover="1"><result status="valid" time="0.06" steps="94"/></proof>
......@@ -35,7 +35,7 @@
</goal>
<goal name="MainResultBits">
<proof prover="1"><result status="valid" time="0.15" steps="130"/></proof>
<proof prover="3"><result status="valid" time="0.82"/></proof>
<proof prover="3"><result status="valid" time="1.04"/></proof>
</goal>
<goal name="MainResultSign">
<proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
......@@ -49,13 +49,13 @@
</goal>
<goal name="Exp_of_xor_j">
<proof prover="1"><result status="valid" time="1.72" steps="492"/></proof>
<proof prover="3"><result status="valid" time="0.97"/></proof>
<proof prover="3"><result status="valid" time="1.24"/></proof>
<proof prover="5"><result status="valid" time="2.98"/></proof>
<proof prover="9"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="Mantissa_of_xor_j">
<proof prover="3"><result status="valid" time="0.96"/></proof>
<proof prover="5"><result status="valid" time="2.74"/></proof>
<proof prover="3"><result status="valid" time="1.22"/></proof>
<proof prover="5"><result status="valid" time="3.18"/></proof>
<proof prover="9"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="MainResultZero">
......@@ -69,7 +69,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult">
<proof prover="1"><result status="valid" time="1.88" steps="320"/></proof>
<proof prover="1"><result status="valid" time="2.34" steps="320"/></proof>
</goal>
</theory>
</file>
......
......@@ -13,7 +13,7 @@
<prover id="8" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" expanded="true">
<theory name="Bitwalker" sum="9e2086079d345ddc6500bd6ac11fac30" expanded="true">
<theory name="Bitwalker" sum="9a21253dfd6ca71d98a38f9ddae88193" expanded="true">
<goal name="nth64">
<proof prover="0"><result status="valid" time="0.10" steps="93"/></proof>
</goal>
......@@ -195,7 +195,7 @@
</goal>
<goal name="VC peek.15" expl="15. loop variant decrease">
<proof prover="0"><result status="valid" time="0.06" steps="99"/></proof>
<proof prover="3"><result status="valid" time="2.42"/></proof>
<proof prover="3"><result status="valid" time="2.77"/></proof>
</goal>
<goal name="VC peek.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04" steps="99"/></proof>
......@@ -311,8 +311,8 @@
</goal>
<goal name="VC poke.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC poke.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="87"/></proof>
......@@ -322,24 +322,20 @@
<goal name="VC poke.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="89"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.07"/></proof>
<proof prover="10"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC poke.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="88"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
<proof prover="10"><result status="valid" time="0.11"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="88"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC poke.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="90"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC poke.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC poke.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="88"/></proof>
......@@ -349,15 +345,19 @@
<goal name="VC poke.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="89"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.07"/></proof>
<proof prover="10"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC poke.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="90"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="90"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
<proof prover="10"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC poke.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="92"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC poke.12" expl="12. precondition">
<proof prover="0"><result status="valid" time="0.04" steps="136"/></proof>
......@@ -459,7 +459,7 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke.34" expl="34. postcondition">
<proof prover="3"><result status="valid" time="2.66"/></proof>
<proof prover="3"><result status="valid" time="3.18"/></proof>
</goal>
</transf>
</goal>
......@@ -553,7 +553,7 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC pokethenpeek.9" expl="9. assertion">
<proof prover="7" timelimit="5"><result status="valid" time="0.93" steps="678"/></proof>
<proof prover="7" timelimit="5"><result status="valid" time="1.14" steps="678"/></proof>
<proof prover="8"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC pokethenpeek.10" expl="10. postcondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bubble_sort.mlw" expanded="true">
<theory name="BubbleSort" sum="1531a9b29a50ede74534b0efbac9724d" expanded="true">
<theory name="BubbleSort" sum="936176f96cd02d8c15a5dc3ae0623b7b" expanded="true">
<goal name="VC bubble_sort" expl="VC for bubble_sort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC bubble_sort.1" expl="1. loop invariant init">
......
......@@ -9,7 +9,7 @@
<prover id="8" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../euclideandivision.why" expanded="true">
<theory name="Test" sum="3cb3c9906da38c258770d7ffcde5a5cd" expanded="true">
<theory name="Test" sum="dcf1b9be9cc7539939694648af57ee2f" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../floats.why" expanded="true">
<theory name="TestGappa" sum="0212aee6ef6d767a0f51ca8a2925a828" expanded="true">
<theory name="TestGappa" sum="764180df31197c66661a15b48342bc0e" expanded="true">
<goal name="Round_single_01" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../intreal.why" expanded="true">
<theory name="IntReal" sum="c554e83e9bde4ee6b64d253c6f27d4d8" expanded="true">
<theory name="IntReal" sum="28c948eed935a025c6f9108aacc5230d" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
......@@ -10,7 +10,7 @@
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
<file name="../real.why" expanded="true">
<theory name="Test" sum="f930be850aa22b603301174419cda7db" expanded="true">
<theory name="Test" sum="7623a8a7853825fa94c01f85974eb028" expanded="true">
<goal name="G1" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
......@@ -33,7 +33,7 @@
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="TestInfix" sum="2665d48e7626fbbd77985b2f32e0fcf2" expanded="true">
<theory name="TestInfix" sum="e3a144e3e8ef683ee32bcc98d33e0562" expanded="true">
<goal name="Add" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
......@@ -93,7 +93,7 @@
</goal>
<goal name="Sqrt_four" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8" timelimit="67" memlimit="1000"><result status="valid" time="22.56"/></proof>
<proof prover="8" timelimit="67" memlimit="1000"><result status="valid" time="27.30"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12" timelimit="5" memlimit="1000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
......@@ -121,7 +121,7 @@
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="TrigonometryTest" sum="e9117dcf6465925bcbebf07e3d99bb04" expanded="true">
<theory name="TrigonometryTest" sum="5794cd25de6688b3f55498681778de56" expanded="true">
<goal name="Cos_2_pi" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.09"/></proof>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../decrease1.mlw" expanded="true">
<theory name="Decrease1" sum="a2ab71223278916b25ab96c60cc79d85" expanded="true">
<theory name="Decrease1" sum="55f466e42f61d728f3e0f4973c3cadce" expanded="true">
<goal name="VC decrease1_induction" expl="VC for decrease1_induction" expanded="true">
<proof prover="9"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compiler.mlw">
<theory name="Compile_aexpr" sum="7a1cf2d7c9649ee4ca61e169e4b8b119">
<theory name="Compile_aexpr" sum="cb57dd980047541f82f3f518cfe318c0">
<goal name="VC compile_aexpr" expl="VC for compile_aexpr">
<transf name="split_goal_wp">
<goal name="VC compile_aexpr.1" expl="1. variant decrease">
......@@ -117,7 +117,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="87"/></proof>
</goal>
</theory>
<theory name="Compile_bexpr" sum="ae61494125bf6c6b968f3b73fbff5399">
<theory name="Compile_bexpr" sum="a7fd6ae40e56d340c5b107b12044e210">
<goal name="VC compile_bexpr" expl="VC for compile_bexpr">
<transf name="split_goal_wp">
<goal name="VC compile_bexpr.1" expl="1. variant decrease">
......@@ -330,7 +330,7 @@
<proof prover="0"><result status="valid" time="0.08" steps="151"/></proof>
</goal>
</theory>
<theory name="Compile_com" sum="89613ca260a5fc035680d112c088fa0d">
<theory name="Compile_com" sum="769d7248aaa2b38bcbfedc7da9d07dad">
<goal name="loop_variant_lemma">
<proof prover="0"><result status="valid" time="0.05" steps="29"/></proof>
</goal>
......@@ -382,14 +382,14 @@
<goal name="loop_variant_acc.3.6" expl="6.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="loop_variant_acc.3.6.1" expl="1.">
<proof prover="1"><result status="valid" time="2.55"/></proof>
<proof prover="1"><result status="valid" time="1.90"/></proof>
</goal>
</transf>
</goal>
<goal name="loop_variant_acc.3.7" expl="7.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="loop_variant_acc.3.7.1" expl="1.">
<proof prover="0"><result status="valid" time="0.09" steps="110"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="109"/></proof>
</goal>
</transf>
</goal>
......@@ -470,7 +470,7 @@
<proof prover="0"><result status="valid" time="0.11" steps="33"/></proof>
</goal>
<goal name="VC compile_com.6.3.1.1.1.6" expl="6. VC for compile_com">
<proof prover="0"><result status="valid" time="0.21" steps="33"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="33"/></proof>
</goal>
<goal name="VC compile_com.6.3.1.1.1.7" expl="7. VC for compile_com">
<proof prover="0"><result status="valid" time="0.10" steps="34"/></proof>
......@@ -543,7 +543,7 @@
<proof prover="0"><result status="valid" time="0.12" steps="55"/></proof>
</goal>
<goal name="VC compile_com.6.5.1.1.1.13" expl="13. VC for compile_com">
<proof prover="0"><result status="valid" time="0.81" steps="605"/></proof>
<proof prover="0"><result status="valid" time="0.61" steps="605"/></proof>
</goal>
<goal name="VC compile_com.6.5.1.1.1.14" expl="14. VC for compile_com">
<proof prover="0"><result status="valid" time="0.12" steps="61"/></proof>
......@@ -604,10 +604,10 @@
</transf>
</goal>
<goal name="VC compile_com.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="0.22" steps="11"/></proof>
<proof prover="0"><result status="valid" time="0.08" steps="11"/></proof>
</goal>
<goal name="VC compile_com.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.22" steps="11"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="11"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="ae5a0bf29b55ad0f369f0131f351d52a">
<theory name="Compiler_logic" sum="af1936aac2cae7a282d2300324a1920e">
<goal name="seq_wp_lemma">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../specs.mlw">
<theory name="VM_instr_spec" sum="17c08329fc66ca05a14a3a537fb64283">
<theory name="VM_instr_spec" sum="a2d376bbabfff098d8d58fcfaf7df286">
<goal name="VC ifunf" expl="VC for ifunf">
<transf name="split_goal_wp">
<goal name="VC ifunf.1" expl="1. precondition">
......@@ -54,7 +54,7 @@
<goal name="VC ivarf" expl="VC for ivarf">
<transf name="split_goal_wp">
<goal name="VC ivarf.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="1.24"/></proof>
<proof prover="1"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="VC ivarf.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.07" steps="30"/></proof>
......@@ -141,7 +141,7 @@
<goal name="VC ibranchf" expl="VC for ibranchf">
<transf name="split_goal_wp">
<goal name="VC ibranchf.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="3.63"/></proof>
<proof prover="1"><result status="valid" time="4.68"/></proof>
</goal>
<goal name="VC ibranchf.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.08" steps="30"/></proof>
......
......@@ -28,7 +28,7 @@
</transf>
</goal>
</theory>
<theory name="Vm" sum="918a5a17d2ce84bec57249e80a720c85">
<theory name="Vm" sum="d7c20117c0d6aafa86a32197bc29cbd9">
<goal name="codeseq_at_app_right">
<proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="4000" memlimit="4000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="4000" memlimit="4000"/>
<file name="../esterel.mlw" expanded="true">
<theory name="Esterel" sum="fa333b2c6770e50cc56ebdc816c82165" expanded="true">
<theory name="Esterel" sum="a31e00167dd5443866ecf5e98e40791c" expanded="true">
<goal name="VC union" expl="VC for union">
<proof prover="1"><result status="valid" time="0.16" steps="268"/></proof>
</goal>
......@@ -55,7 +55,7 @@
<proof prover="2"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="VC maxUnion.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="1.54" steps="2018"/></proof>
<proof prover="1"><result status="valid" time="1.82" steps="2018"/></proof>
</goal>
<goal name="VC maxUnion.5" expl="5. postcondition">
<transf name="split_goal_wp">
......
......@@ -8,7 +8,7 @@
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gcd.mlw" expanded="true">
<theory name="EuclideanAlgorithm" sum="93083dc87e1612939f080d411978440f" expanded="true">
<theory name="EuclideanAlgorithm" sum="39fd6f4231fda19046ddbaa3fe323190" expanded="true">
<goal name="VC euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="VC euclid.1" expl="1. check modulo by zero">
......@@ -26,12 +26,12 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithmIterative" sum="4841a879f96158e78cf1e196ec0e2c3b" expanded="true">
<theory name="EuclideanAlgorithmIterative" sum="8d8cdd602eed94c46d8d51bbd8c3b6c3" expanded="true">
<goal name="VC euclid" expl="VC for euclid">