Commit 19a3ca0c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update obsolete sessions.

parent 3aae32e7
......@@ -21,7 +21,7 @@
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="a461d2adc484fc2d2afb0b9f73473acf" expanded="true">
<theory name="BinarySearchInt32" sum="d40ebb1dbba84353a007cae5cf938f85" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="integer overflow">
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binomial_heap.mlw" expanded="true">
<theory name="BinomialHeap" sum="5b1dd2e701903b8fba3c565ace8f367e" expanded="true">
<theory name="BinomialHeap" sum="8d64901bf73863fd85973498d6d63561" expanded="true">
<goal name="WP_parameter size_nonnneg" expl="VC for size_nonnneg">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
......
......@@ -11,7 +11,7 @@
<prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="4000"/>
<file name="../bitcount.mlw" expanded="true">
<theory name="BitCount8bit_fact" sum="d7beb47fd57cce4adfd32e788b5fc6b6" expanded="true">
<theory name="BitCount8bit_fact" sum="99b5e737a47bc4d44af3991411b366b5" expanded="true">
<goal name="nth_as_bv_is_int" expl="">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.08"/></proof>
......@@ -119,7 +119,7 @@
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter step2.5.5" expl="assertion">
<proof prover="2"><result status="valid" time="2.74"/></proof>
<proof prover="2"><result status="valid" time="2.29"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
......@@ -128,7 +128,7 @@
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="3.14" steps="1615"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="2.63" steps="1615"/></proof>
</goal>
<goal name="WP_parameter step2.7" expl="postcondition">
<proof prover="2"><result status="valid" time="0.10"/></proof>
......@@ -246,7 +246,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" sum="b5bb23cfdbeddba673e2913aa853d26a" expanded="true">
<theory name="BitCounting32" sum="5cf5eb98e6421cc1fd2e02807127d18a" expanded="true">
<goal name="WP_parameter proof0" expl="VC for proof0" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter proof0.1" expl="assertion" expanded="true">
......@@ -352,7 +352,7 @@
<goal name="WP_parameter proof1.7.3" expl="VC for proof1">
<proof prover="3"><result status="valid" time="0.04" steps="96"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="5"><result status="valid" time="1.00"/></proof>
<proof prover="5"><result status="valid" time="0.73"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="97"/></proof>
</goal>
</transf>
......@@ -730,7 +730,7 @@
</transf>
</goal>
</theory>
<theory name="Hamming" sum="b941c28b1f53e32f396a99ff9ee6d06e" expanded="true">
<theory name="Hamming" sum="8a18ee6c3ad8edbde114cd8e4d7dd2fa" expanded="true">
<goal name="WP_parameter hammingD" expl="VC for hammingD">
<transf name="split_goal_wp">
<goal name="WP_parameter hammingD.1" expl="assertion">
......@@ -746,13 +746,13 @@
</transf>
</goal>
<goal name="symmetric" expl="">
<proof prover="3"><result status="valid" time="2.29" steps="1634"/></proof>
<proof prover="3"><result status="valid" time="1.96" steps="1634"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
<proof prover="6"><result status="valid" time="0.39" steps="599"/></proof>
</goal>
<goal name="numof_ytpmE" expl="">
<proof prover="2"><result status="valid" time="1.20"/></proof>
<proof prover="5"><result status="valid" time="1.30"/></proof>
<proof prover="2"><result status="valid" time="0.94"/></proof>
<proof prover="5"><result status="valid" time="0.97"/></proof>
</goal>
<goal name="WP_parameter separation" expl="VC for separation">
<transf name="split_goal_wp">
......@@ -783,7 +783,7 @@
<proof prover="3"><result status="timeout" time="6.00"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.39"/></proof>
<proof prover="6"><result status="valid" time="2.81" steps="1908"/></proof>
<proof prover="6"><result status="valid" time="2.27" steps="1908"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
......@@ -823,7 +823,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
</theory>
<theory name="AsciiCode" sum="3cf68ae30e5228e39a82ff5335f307c1" expanded="true">
<theory name="AsciiCode" sum="704687291f8f34ab2d4b9314539adea5" expanded="true">
<goal name="WP_parameter bv_even" expl="VC for bv_even">
<transf name="split_goal_wp">
<goal name="WP_parameter bv_even.1" expl="assertion">
......@@ -882,7 +882,7 @@
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter count_or.4" expl="assertion">
<proof prover="5"><result status="valid" time="1.81"/></proof>
<proof prover="5"><result status="valid" time="1.36"/></proof>
</goal>
<goal name="WP_parameter count_or.5" expl="postcondition">
<proof prover="2"><result status="valid" time="0.08"/></proof>
......@@ -946,7 +946,7 @@
<goal name="WP_parameter ascii.6" expl="postcondition">
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="1.55"/></proof>
<proof prover="5"><result status="valid" time="1.25"/></proof>
</goal>
<goal name="WP_parameter ascii.7" expl="postcondition">
<proof prover="3"><result status="valid" time="0.20" steps="148"/></proof>
......@@ -979,10 +979,10 @@
</goal>
<goal name="WP_parameter tmp.4" expl="postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="2"><result status="valid" time="4.31"/></proof>
<proof prover="2"><result status="valid" time="3.55"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="5.75"/></proof>
<proof prover="5"><result status="valid" time="1.42"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="2.06" steps="3154"/></proof>
<proof prover="5"><result status="valid" time="1.11"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="2.06" steps="3155"/></proof>
</goal>
</transf>
</goal>
......@@ -991,7 +991,7 @@
<proof prover="3"><result status="valid" time="1.51" steps="3019"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.13"/></proof>
<proof prover="6"><result status="valid" time="0.26" steps="514"/></proof>
<proof prover="6"><result status="valid" time="0.13" steps="514"/></proof>
</goal>
</theory>
</file>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="ab759a44e440a5696e3be5d5c1002f13">
<theory name="Test_proofinuse" sum="0005f9b0b6dd327d79b9311dcc38bc63">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
<transf name="split_goal_wp">
<goal name="WP_parameter shift_is_div.1" expl="assertion">
......@@ -33,7 +33,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="e69379c4cdd7999f5270b4b04a8a7851">
<theory name="Hackers_delight" sum="e8df673927d4283d55605cb67efe0a99">
<goal name="DM1" expl="">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -92,7 +92,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="1fd41f060d75d6937dd09fd3cd308955">
<theory name="Hackers_delight_mod" sum="1d16fc37232b5b1681032eb68a290f19">
<goal name="WP_parameter dm1" expl="VC for dm1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -154,7 +154,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="87e97acde0976021b8e959fbfeaf175d">
<theory name="Test_imperial_violet" sum="e1422ff2751327867185a34b23404d0a">
<goal name="bv32_bounds_bv" expl="">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -174,7 +174,7 @@
<proof prover="4"><result status="valid" time="0.25"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="3d879fd348d7e9a9a48b81536d51ff66">
<theory name="Test_from_bitvector_example" sum="2d8219908bc50228f5f5bdfdac5307c6">
<goal name="Test1" expl="">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector.why" expanded="true">
<theory name="BitVector" sum="56ab01db58e9813d50bb175d7c7d1f21">
<theory name="BitVector" sum="5720c2b4494f4318602469524b5a7701">
<goal name="Nth_bw_xor_v1true" expl="">
<proof prover="2"><result status="valid" time="0.08" steps="85"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -82,7 +82,7 @@
</theory>
<theory name="BV32_64" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestBv32" sum="aaff0ca7631b7a4da12a71cdb1d74453">
<theory name="TestBv32" sum="121c26467ae65841dfeca4723ab7a931">
<goal name="Test1" expl="">
<proof prover="2"><result status="valid" time="0.06" steps="72"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
......@@ -132,61 +132,61 @@
<proof prover="10"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="to_nat_0x00000001" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="86.14"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="62.13"/></proof>
</goal>
<goal name="to_nat_0x00000003" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="65.79"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="53.50"/></proof>
</goal>
<goal name="to_nat_0x00000007" expl="">
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="53.94"/></proof>
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="45.82"/></proof>
</goal>
<goal name="to_nat_0x0000000F" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="46.07"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="38.30"/></proof>
</goal>
<goal name="to_nat_0x0000001F" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="38.43"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="31.82"/></proof>
</goal>
<goal name="to_nat_0x0000003F" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="31.47"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="25.98"/></proof>
</goal>
<goal name="to_nat_0x0000007F" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="25.82"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="20.98"/></proof>
</goal>
<goal name="to_nat_0x000000FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="26.48"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="17.04"/></proof>
</goal>
<goal name="to_nat_0x000001FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="17.53"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="13.70"/></proof>
</goal>
<goal name="to_nat_0x000003FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="13.79"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="10.85"/></proof>
</goal>
<goal name="to_nat_0x000007FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="11.02"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="8.48"/></proof>
</goal>
<goal name="to_nat_0x00000FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="10.38"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.62"/></proof>
</goal>
<goal name="to_nat_0x00001FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.88"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="5.16"/></proof>
</goal>
<goal name="to_nat_0x00003FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="5.48"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="3.97"/></proof>
</goal>
<goal name="to_nat_0x00007FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.14"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="3.03"/></proof>
</goal>
<goal name="to_nat_0x0000FFFF" expl="">
<proof prover="6"><result status="valid" time="3.18"/></proof>
<proof prover="6"><result status="valid" time="2.32"/></proof>
</goal>
<goal name="to_nat_0x0001FFFF" expl="">
<proof prover="6"><result status="valid" time="2.32"/></proof>
<proof prover="6"><result status="valid" time="1.78"/></proof>
</goal>
<goal name="to_nat_0x0003FFFF" expl="">
<proof prover="6"><result status="valid" time="1.77"/></proof>
<proof prover="6"><result status="valid" time="1.38"/></proof>
</goal>
<goal name="to_nat_0x0007FFFF" expl="">
<proof prover="6"><result status="valid" time="1.56"/></proof>
<proof prover="6"><result status="valid" time="1.05"/></proof>
</goal>
<goal name="to_nat_0x000FFFFF" expl="">
<proof prover="6"><result status="valid" time="0.89"/></proof>
......
......@@ -10,7 +10,7 @@
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestDouble" sum="5ce7948642418735c961736e21b96aa2" expanded="true">
<theory name="TestDouble" sum="b7b2448ba36ad5c80868aff06a16bf4d" expanded="true">
<goal name="nth_one1" expl="" expanded="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
......
......@@ -10,7 +10,7 @@
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double_of_int.why" expanded="true">
<theory name="DoubleOfInt" sum="3dc175bd86df5ca76d252ec30fc990f7" expanded="true">
<theory name="DoubleOfInt" sum="75e5656e68b0fedba8979b7bbef041a1" expanded="true">
<goal name="nth_j1" expl="">
<proof prover="1"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
......@@ -28,7 +28,7 @@
</goal>
<goal name="nth_j6" expl="">
<proof prover="1"><result status="valid" time="0.07" steps="76"/></proof>
<proof prover="4"><result status="valid" time="2.46"/></proof>
<proof prover="4"><result status="valid" time="2.08"/></proof>
</goal>
<goal name="nth_j7" expl="">
<proof prover="1"><result status="valid" time="0.04" steps="76"/></proof>
......@@ -44,7 +44,7 @@
</goal>
<goal name="nth_const3" expl="">
<proof prover="1"><result status="valid" time="0.10" steps="98"/></proof>
<proof prover="4"><result status="valid" time="1.03"/></proof>
<proof prover="4"><result status="valid" time="0.71"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="nth_const4" expl="">
......@@ -54,7 +54,7 @@
</goal>
<goal name="nth_const5" expl="">
<proof prover="1"><result status="valid" time="0.11" steps="99"/></proof>
<proof prover="4"><result status="valid" time="1.07"/></proof>
<proof prover="4"><result status="valid" time="0.74"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="nth_const6" expl="">
......@@ -133,7 +133,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.28"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.75"/></proof>
<proof prover="8"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="nth_0_30" expl="">
......@@ -174,7 +174,7 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_neg" expl="">
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.06"/></proof>
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.74"/></proof>
</goal>
<goal name="lemma1_neg" expl="">
<proof prover="3" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
......@@ -190,7 +190,7 @@
<proof prover="4" timelimit="10"><result status="valid" time="1.98"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" expl="">
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="2.08"/></proof>
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="1.74"/></proof>
</goal>
<goal name="to_nat_bv32_bv64" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="90"/></proof>
......@@ -208,7 +208,7 @@
<proof prover="4"><result status="valid" time="2.00"/></proof>
</goal>
<goal name="nth_var3" expl="">
<proof prover="1"><result status="valid" time="1.39" steps="146"/></proof>
<proof prover="1"><result status="valid" time="1.12" steps="146"/></proof>
<proof prover="4"><result status="valid" time="1.02"/></proof>
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
......@@ -216,7 +216,7 @@
<proof prover="3" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="23.13"/></proof>
</goal>
<goal name="nth_var4" expl="">
<proof prover="1"><result status="valid" time="1.44" steps="148"/></proof>
<proof prover="1"><result status="valid" time="1.14" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.06"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
......@@ -226,12 +226,12 @@
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="nth_var6" expl="">
<proof prover="1"><result status="valid" time="1.41" steps="148"/></proof>
<proof prover="1"><result status="valid" time="1.13" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.08"/></proof>
<proof prover="8"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="nth_var7" expl="">
<proof prover="1"><result status="valid" time="1.39" steps="148"/></proof>
<proof prover="1"><result status="valid" time="1.13" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.07"/></proof>
<proof prover="8"><result status="valid" time="0.82"/></proof>
</goal>
......@@ -243,7 +243,7 @@
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="lemma3" expl="">
<proof prover="4"><result status="valid" time="2.44"/></proof>
<proof prover="4"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="nth_var9" expl="">
<proof prover="1"><result status="valid" time="0.10" steps="95"/></proof>
......@@ -285,7 +285,7 @@
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="var_value4" expl="">
<proof prover="1"><result status="valid" time="1.41" steps="104"/></proof>
<proof prover="1"><result status="valid" time="1.15" steps="104"/></proof>
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="pow31" expl="">
......@@ -298,10 +298,10 @@
<proof prover="2"><result status="valid" time="0.22"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.97"/></proof>
<proof prover="8"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="MainResult" expl="">
<proof prover="1"><result status="valid" time="1.56" steps="139"/></proof>
<proof prover="1"><result status="valid" time="1.25" steps="139"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.99"/></proof>
......
......@@ -7,24 +7,24 @@
<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="9d104c5eab3c1c89149eb7e9c9879bb3" expanded="true">
<theory name="TestNegAsXOR" sum="917d924985a49cf270f94a08ebdbeab3" expanded="true">
<goal name="Nth_j" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="sign_of_j" expl="">
<proof prover="1"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="3"><result status="valid" time="2.86"/></proof>
<proof prover="3"><result status="valid" time="2.38"/></proof>
</goal>
<goal name="mantissa_of_j" expl="">
<proof prover="1"><result status="valid" time="0.16" steps="121"/></proof>
<proof prover="3"><result status="valid" time="1.10"/></proof>
<proof prover="3"><result status="valid" time="0.77"/></proof>
<proof prover="5"><result status="valid" time="2.72"/></proof>
<proof prover="9"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="exp_of_j" expl="">
<proof prover="1"><result status="valid" time="0.17" steps="122"/></proof>
<proof prover="3"><result status="valid" time="0.82"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.10"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.62"/></proof>
<proof prover="9"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="int_of_bv" expl="">
......@@ -35,7 +35,7 @@
</goal>
<goal name="MainResultBits" expl="">
<proof prover="1"><result status="valid" time="0.15" steps="130"/></proof>
<proof prover="3"><result status="valid" time="1.03"/></proof>
<proof prover="3"><result status="valid" time="0.71"/></proof>
</goal>
<goal name="MainResultSign" expl="">
<proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
......@@ -48,28 +48,28 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Exp_of_xor_j" expl="">
<proof prover="1"><result status="valid" time="1.72" steps="492"/></proof>
<proof prover="1"><result status="valid" time="1.41" steps="492"/></proof>
<proof prover="3"><result status="valid" time="0.94"/></proof>
<proof prover="5"><result status="valid" time="2.98"/></proof>
<proof prover="9"><result status="valid" time="0.88"/></proof>
<proof prover="5"><result status="valid" time="2.48"/></proof>
<proof prover="9"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="Mantissa_of_xor_j" expl="">
<proof prover="3"><result status="valid" time="0.96"/></proof>
<proof prover="5"><result status="valid" time="3.36"/></proof>
<proof prover="5"><result status="valid" time="2.83"/></proof>
<proof prover="9"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="MainResultZero" expl="">
<proof prover="1"><result status="valid" time="0.07" steps="104"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="3.77"/></proof>
<proof prover="9"><result status="valid" time="1.30"/></proof>
<proof prover="5"><result status="valid" time="3.18"/></proof>
<proof prover="9"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="sign_neg" expl="">
<proof prover="1"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult" expl="">
<proof prover="1"><result status="valid" time="2.21" steps="320"/></proof>
<proof prover="1"><result status="valid" time="1.81" steps="320"/></proof>
</goal>
</theory>
</file>
......
......@@ -10,7 +10,7 @@
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../power2.why" expanded="true">
<theory name="Pow2int" sum="9fc82536cb7d687719957627f5566f96">
<theory name="Pow2int" sum="bef1069d66f5988e998039f1095194c2">
<goal name="Power_1" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -18,7 +18,7 @@
<proof prover="10"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="1" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="1" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.61"/></proof>
</goal>
<goal name="pow2pos" expl="">
<proof prover="1" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.49"/></proof>
......@@ -231,7 +231,7 @@
</goal>
<goal name="pow2_34" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.63"/></proof>
<proof prover="6"><result status="valid" time="0.45"/></proof>
<proof prover="9"><result status="valid" time="0.69"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
......@@ -243,8 +243,8 @@
</goal>
<goal name="pow2_36" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.72"/></proof>
<proof prover="9"><result status="valid" time="0.87"/></proof>
<proof prover="6"><result status="valid" time="0.52"/></proof>
<proof prover="9"><result status="valid" time="0.63"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="pow2_37" expl="">
......@@ -255,13 +255,13 @@
</goal>
<goal name="pow2_38" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.81"/></proof>
<proof prover="6"><result status="valid" time="0.61"/></proof>
<proof prover="9"><result status="valid" time="0.82"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="41"/></proof>
</goal>
<goal name="pow2_39" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.84"/></proof>
<proof prover="6"><result status="valid" time="0.65"/></proof>
<proof prover="9"><result status="valid" time="0.89"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
......@@ -273,7 +273,7 @@
</goal>
<goal name="pow2_41" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.98"/></proof>
<proof prover="6"><result status="valid" time="0.73"/></proof>
<proof prover="9"><result status="valid" time="1.01"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
......@@ -285,7 +285,7 @@
</goal>
<goal name="pow2_43" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="1.11"/></proof>
<proof prover="6"><result status="valid" time="0.89"/></proof>
<proof prover="9"><result status="valid" time="1.16"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
......@@ -297,20 +297,20 @@
</goal>
<goal name="pow2_45" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="1.33"/></proof>
<proof prover="6"><result status="valid" time="1.04"/></proof>
<proof prover="9"><result status="valid" time="1.30"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="pow2_46" expl="">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="1.42"/></proof>
<proof prover="9"><result status="valid" time="1.44"/></proof>
<proof prover="6"><result status="valid" time="1.16"/></proof>
<proof prover="9"><result status="valid" time="1.17"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="pow2_47" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.56"/></proof>
<proof prover="9"><result status="valid" time="1.53"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.22"/></proof>
<proof prover="9"><result status="valid" time="1.25"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="pow2_48" expl="">
......@@ -334,19 +334,19 @@
<goal name="pow2_51" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="7"><result status="valid" time="2.08"/></proof>
<proof prover="9"><result status="valid" time="1.77"/></proof>
<proof prover="9"><result status="valid" time="1.46"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="54"/></proof>
</goal>
<goal name="pow2_52" expl="">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="6" timelimit="8"><result status="valid" time="2.31"/></proof>
<proof prover="9"><result status="valid" time="1.90"/></proof>
<proof prover="6" timelimit="8"><result status="valid" time="1.94"/></proof>
<proof prover="9"><result status="valid" time="1.54"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="55"/></proof>
</goal>
<goal name="pow2_53" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="2.80"/></proof>
<proof prover="9"><result status="valid" time="1.95"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="2.23"/></proof>
<proof prover="9"><result status="valid" time="1.63"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="56"/></proof>
</goal>
<goal name="pow2_54" expl="">
......@@ -357,50 +357,50 @@
</goal>
<goal name="pow2_55" expl="">