Commit f41d9379 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update obsolete sessions.

parent 3489d1a0
......@@ -11,7 +11,7 @@
<prover id="6" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitcount.mlw" proved="true">
<theory name="BitCount8bit_fact" proved="true" sum="02606ce12395f0ad45fd12ef8d84e596">
<theory name="BitCount8bit_fact" proved="true" sum="ce5bf4ea6b0dd49c2f2ccdbe8aa792bd">
<goal name="nth_as_bv_is_int" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.16" steps="166"/></proof>
......@@ -36,7 +36,7 @@
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter step1.2" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.17" steps="294"/></proof>
<proof prover="1"><result status="valid" time="0.29" steps="294"/></proof>
<proof prover="3"><result status="valid" time="0.17" steps="151"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
......@@ -219,7 +219,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" proved="true" sum="d5ad1e97cb81202bd50a599e10f3e7ab">
<theory name="BitCounting32" proved="true" sum="857c22d5dd71e8cd46bf3ed318ae0f09">
<goal name="WP_parameter proof0" expl="VC for proof0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter proof0.0" expl="assertion" proved="true">
......@@ -697,7 +697,7 @@
</transf>
</goal>
</theory>
<theory name="Hamming" proved="true" sum="b941c28b1f53e32f396a99ff9ee6d06e">
<theory name="Hamming" proved="true" sum="dbbf085bba45382baa2cd71df91e2dd0">
<goal name="WP_parameter hammingD" expl="VC for hammingD" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter hammingD.0" expl="assertion" proved="true">
......@@ -788,7 +788,7 @@
<proof prover="5"><result status="valid" time="0.10"/></proof>
</goal>
</theory>
<theory name="AsciiCode" proved="true" sum="3cf68ae30e5228e39a82ff5335f307c1">
<theory name="AsciiCode" proved="true" sum="b3346cbb487c123b3b52d74a74d62c45">
<goal name="WP_parameter bv_even" expl="VC for bv_even" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter bv_even.0" expl="assertion" proved="true">
......@@ -847,7 +847,7 @@
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter count_or.3" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="1.81"/></proof>
<proof prover="5"><result status="valid" time="1.37"/></proof>
</goal>
<goal name="WP_parameter count_or.4" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="81"/></proof>
......@@ -944,8 +944,8 @@
</goal>
<goal name="WP_parameter tmp.3" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="4.31"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="2.06" steps="3154"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="5.75"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="2.06" steps="3155"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="6.48"/></proof>
<proof prover="5"><result status="valid" time="1.42"/></proof>
<proof prover="6"><result status="valid" time="0.26"/></proof>
</goal>
......
This diff is collapsed.
......@@ -8,7 +8,7 @@
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../specs.mlw" proved="true">
<theory name="VM_instr_spec" proved="true" sum="ad8a3721e677b50f148fb592a5e47fa0">
<theory name="VM_instr_spec" proved="true" sum="5dd153da014e29247d6e95de4c0d5333">
<goal name="WP_parameter ifunf" expl="VC for ifunf" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter ifunf.0" expl="assertion" proved="true">
......
......@@ -11,7 +11,7 @@
<prover id="6" name="Eprover" version="1.8-001" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../euler001.mlw" proved="true">
<theory name="DivModHints" proved="true" sum="85d2840a9bc90f1571e3822f8c831780">
<theory name="DivModHints" proved="true" sum="6f77cd46f4f6ca514a80124063f6a33c">
<goal name="mod_div_unique" proved="true">
<transf name="assert" proved="true" arg1="(q - div x y) * y + (r - mod x y) = 0">
<goal name="mod_div_unique.0" proved="true">
......@@ -19,22 +19,22 @@
</goal>
<goal name="mod_div_unique.1" proved="true">
<transf name="case" proved="true" arg1="q - div x y &gt;= 1">
<goal name="mod_div_unique.1.0" proved="true">
<goal name="mod_div_unique.1.0" expl="true case" proved="true">
<proof prover="6"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="mod_div_unique.1.1" proved="true">
<goal name="mod_div_unique.1.1" expl="false case" proved="true">
<transf name="case" proved="true" arg1="q - div x y &lt;= -1">
<goal name="mod_div_unique.1.1.0" proved="true">
<goal name="mod_div_unique.1.1.0" expl="false case (true case)" proved="true">
<transf name="assert" proved="true" arg1="(y * (q - div x y) &lt;= - y)">
<goal name="mod_div_unique.1.1.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.66"/></proof>
<proof prover="2"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="mod_div_unique.1.1.0.1" proved="true">
<goal name="mod_div_unique.1.1.0.1" expl="false case (true case)" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="mod_div_unique.1.1.1" proved="true">
<goal name="mod_div_unique.1.1.1" expl="false case" proved="true">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -47,10 +47,10 @@
<transf name="introduce_premises" proved="true" >
<goal name="mod_succ_1.0" proved="true">
<transf name="case" proved="true" arg1="(x &lt; y)">
<goal name="mod_succ_1.0.0" proved="true">
<goal name="mod_succ_1.0.0" expl="true case" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="mod_succ_1.0.1" proved="true">
<goal name="mod_succ_1.0.1" expl="false case" proved="true">
<transf name="assert" proved="true" arg1="(exists q:int. exists r:int. (x + 1 = y * q + r) /\ (r &lt; y) /\ (r &gt;= 0))">
<goal name="mod_succ_1.0.1.0" proved="true">
<transf name="exists" proved="true" arg1="(div (x + 1) y)">
......@@ -63,25 +63,25 @@
</goal>
</transf>
</goal>
<goal name="mod_succ_1.0.1.1" proved="true">
<goal name="mod_succ_1.0.1.1" expl="false case" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="mod_succ_1.0.1.1.0" proved="true">
<goal name="mod_succ_1.0.1.1.0" expl="false case" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="mod_succ_1.0.1.1.0.0" proved="true">
<goal name="mod_succ_1.0.1.1.0.0" expl="false case" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="mod_succ_1.0.1.1.0.0.0" proved="true">
<goal name="mod_succ_1.0.1.1.0.0.0" expl="false case" proved="true">
<transf name="rewrite" proved="true" arg1="h1">
<goal name="mod_succ_1.0.1.1.0.0.0.0" proved="true">
<goal name="mod_succ_1.0.1.1.0.0.0.0" expl="false case" proved="true">
<transf name="case" proved="true" arg1="(r = 0)">
<goal name="mod_succ_1.0.1.1.0.0.0.0.0" proved="true">
<goal name="mod_succ_1.0.1.1.0.0.0.0.0" expl="false case (true case)" proved="true">
<proof prover="5" memlimit="1000"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="mod_succ_1.0.1.1.0.0.0.0.1" proved="true">
<goal name="mod_succ_1.0.1.1.0.0.0.0.1" expl="false case" proved="true">
<transf name="assert" proved="true" arg1="(x = y * q + (r-1))">
<goal name="mod_succ_1.0.1.1.0.0.0.0.1.0" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="7" timelimit="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="mod_succ_1.0.1.1.0.0.0.0.1.1" proved="true">
<goal name="mod_succ_1.0.1.1.0.0.0.0.1.1" expl="false case" proved="true">
<proof prover="3" memlimit="2000"><result status="valid" time="2.19" steps="53"/></proof>
</goal>
</transf>
......
......@@ -8,7 +8,7 @@
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.3" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../inverse_in_place.mlw" proved="true">
<theory name="InverseInPlace" proved="true" sum="c2ab810a0020582a928fb620a26a9fa1">
<theory name="InverseInPlace" proved="true" sum="d6404b3c56d2c6cfc15390ec33f7392c">
<goal name="is_permutation_inverse" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
......@@ -83,7 +83,7 @@
</goal>
<goal name="WP_parameter inverse_in_place.13" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="2.79"/></proof>
<proof prover="4"><result status="valid" time="3.34"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.14" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.46"/></proof>
......
......@@ -15,7 +15,7 @@
<prover id="10" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.3.2" timelimit="2" steplimit="0" memlimit="1000"/>
<file name="../knuth_prime_numbers.mlw" proved="true">
<theory name="PrimeNumbers" proved="true" sum="4e6281562079bb06b173a2237db04a26">
<theory name="PrimeNumbers" proved="true" sum="6550cbedc0c19c9611f6cb6986837c1e">
<goal name="exists_prime" proved="true">
<proof prover="3" timelimit="10" memlimit="0" edited="knuth_prime_numbers_WP_PrimeNumbers_exists_prime_1.v"><result status="valid" time="0.40"/></proof>
</goal>
......
......@@ -10,7 +10,7 @@
</theory>
<theory name="HashTable" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MaxMatrixMemo" proved="true" sum="219f32c43fd20bfa2cdb14a8219f11e2">
<theory name="MaxMatrixMemo" proved="true" sum="5b42bdc9be102550da348e63e14f4c26">
<goal name="sum_ind" proved="true">
<proof prover="0" timelimit="47" memlimit="0"><result status="valid" time="0.15" steps="45"/></proof>
</goal>
......
......@@ -8,7 +8,7 @@
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../quicksort.mlw" proved="true">
<theory name="Quicksort" proved="true" sum="e2ce40232d6da5372b38a6a9ea72d93a">
<theory name="Quicksort" proved="true" sum="965ad995aed207e39546ee22443583e3">
<goal name="WP_parameter quick_rec" expl="VC for quick_rec" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter quick_rec.0" expl="index in array bounds" proved="true">
......@@ -221,7 +221,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</theory>
<theory name="Quicksort3way" proved="true" sum="2e873de01db508cb089c0ce4ef6e9719">
<theory name="Quicksort3way" proved="true" sum="1cb1dc3b245dbd764092d74158806328">
<goal name="WP_parameter quick_rec" expl="VC for quick_rec" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter quick_rec.0" expl="index in array bounds" proved="true">
......@@ -386,7 +386,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</theory>
<theory name="Test" proved="true" sum="6cdb2ce7f4eb0d761daf24e6f68aeb1f">
<theory name="Test" proved="true" sum="411520a763f0c4a8890c3be99970416f">
<goal name="WP_parameter test1" expl="VC for test1" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
......
......@@ -12,7 +12,7 @@
<prover id="7" name="Z3" version="4.3.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bv.why">
<theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503">
<theory name="CheckBV64" sum="7e8a7e7576a1ea44722bda34dc4315dd">
<goal name="ok_zero" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -227,7 +227,7 @@
</goal>
<goal name="smoke6">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.46"/></proof>
<proof prover="1"><result status="unknown" time="0.68"/></proof>
<proof prover="3" timelimit="1"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5"><result status="timeout" time="1.00"/></proof>
......@@ -281,7 +281,7 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g3a" proved="true">
<proof prover="1"><result status="valid" time="0.81"/></proof>
<proof prover="1"><result status="valid" time="1.20"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -342,7 +342,7 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Nth_Bv_bw_and" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="219"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="209"/></proof>
<proof prover="1"><result status="valid" time="0.20"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
......@@ -404,7 +404,7 @@
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950">
<theory name="CheckBV32" sum="7f83731525208233c34727098dfc973c">
<goal name="ok_zero" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -644,7 +644,7 @@
<proof prover="8"><result status="unknown" time="0.01"/></proof>
</goal>
</theory>
<theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16">
<theory name="CheckBV16" sum="fb1903a07ca6adb30f2b8c3ee975c2f4">
<goal name="ok_zero" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -741,7 +741,7 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ok13" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.50"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -861,7 +861,7 @@
</goal>
<goal name="smoke6">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.70"/></proof>
<proof prover="1"><result status="unknown" time="0.45"/></proof>
<proof prover="3" timelimit="1"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="0.98"/></proof>
<proof prover="5"><result status="timeout" time="1.00"/></proof>
......@@ -889,7 +889,7 @@
<proof prover="8"><result status="unknown" time="0.01"/></proof>
</goal>
</theory>
<theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767">
<theory name="CheckBV8" sum="b165aa59501e844178563866236be8fa">
<goal name="ok_zero" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
......
......@@ -27,7 +27,7 @@
<prover id="22" name="CVC4" version="1.5" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="23" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../div.why">
<theory name="EuclideanDivTest" sum="da32af7f9607b7df69daf270bd5c10cc">
<theory name="EuclideanDivTest" sum="f681554b176848eb80aa280a963f7b44">
<goal name="ok1" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -82,7 +82,7 @@
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="unknown" time="1.72"/></proof>
<proof prover="14"><result status="unknown" time="2.06"/></proof>
<proof prover="15"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="19"><result status="valid" time="0.02" steps="0"/></proof>
......@@ -299,7 +299,7 @@
<proof prover="23"><result status="unknown" time="1.92"/></proof>
</goal>
</theory>
<theory name="ComputerDivTest" sum="6ab164b7322ab7c63b0e43326553ed39">
<theory name="ComputerDivTest" sum="a20f961d6e8e381a10b2bd458c94d3f3">
<goal name="ok1" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -448,7 +448,7 @@
<proof prover="20"><result status="timeout" time="1.00"/></proof>
<proof prover="21"><result status="unknown" time="0.02"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23" memlimit="0"><result status="unknown" time="1.07"/></proof>
<proof prover="23" memlimit="0"><result status="unknown" time="2.05"/></proof>
</goal>
<goal name="smoke2">
<proof prover="0"><result status="unknown" time="0.05"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="PolyPaver" version="0.3" timelimit="3600" steplimit="0" memlimit="1000"/>
<file name="../polypaver.why">
<theory name="TestReal" sum="237f987f3ba27b23cd7c92d0aee93cf7">
<theory name="TestReal" sum="e0c7514367a882fec2ff542c489f8ce6">
<goal name="add1">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
......@@ -12,10 +12,10 @@
<proof prover="0" timelimit="5"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="exp_hyp" proved="true">
<proof prover="0" timelimit="120"><result status="valid" time="16.23"/></proof>
<proof prover="0" timelimit="120"><result status="valid" time="18.19"/></proof>
</goal>
<goal name="g1" proved="true">
<proof prover="0"><result status="valid" time="626.99"/></proof>
<proof prover="0"><result status="valid" time="690.67"/></proof>
</goal>
</theory>
</file>
......
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