Commit 6c51b1e8 authored by MARCHE Claude's avatar MARCHE Claude

bit-vector theory: do not remove all the axioms for SMT solvers but only some of them

parent 18c56fdb
......@@ -20,7 +20,28 @@ theory bv.BV_Gen
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
remove allprops
(* Warning: we should NOT remove all the axioms using "allprops" *)
remove prop to_uint_add
remove prop to_uint_add_bounded
remove prop to_uint_sub
remove prop to_uint_sub_bounded
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_mul_bounded
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
remove prop lsr_bv_is_lsr
remove prop to_uint_lsr
remove prop asr_bv_is_asr
remove prop lsl_bv_is_lsl
remove prop to_uint_lsl
remove prop rotate_left_bv_is_rotate_left
remove prop rotate_right_bv_is_rotate_right
remove prop Extensionality
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
......
......@@ -3,27 +3,24 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="10" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="7c8646b76f7105e1357a0dac5eef6893" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.17" steps="55"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.17" steps="59"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" sum="fd005960645f7d3c23e93b34d869829e" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="39"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="7bcdc213da0ebbcf4ac39df39f0b78b1" expanded="true">
<theory name="BinarySearchInt32" sum="84d73d964ac2e52c2a4c56e898a3c5f5" 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="1. integer overflow">
......@@ -73,8 +70,8 @@
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="3.60"/></proof>
<proof prover="5"><result status="valid" time="1.36" steps="179"/></proof>
<proof prover="2"><result status="valid" time="4.16"/></proof>
<proof prover="5"><result status="valid" time="1.68" steps="179"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="98"/></proof>
......@@ -94,7 +91,7 @@
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="3.46"/></proof>
<proof prover="5"><result status="valid" time="1.31" steps="180"/></proof>
<proof prover="5"><result status="valid" time="1.99" steps="180"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="100"/></proof>
......
......@@ -8,7 +8,7 @@
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<file name="../bitcount.mlw" expanded="true">
<theory name="BitCount8bit_fact" sum="740413d607ad035d2474aa6fcc9095b0">
<theory name="BitCount8bit_fact" sum="5751fad0b4d740cb2042ca2423c25c5e">
<goal name="nth_as_bv_is_int">
<proof prover="0"><result status="valid" time="0.18" steps="95"/></proof>
</goal>
......@@ -20,12 +20,12 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter step1.1.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="0.33"/></proof>
<proof prover="2"><result status="valid" time="0.59"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter step1.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="4.07" steps="668"/></proof>
<proof prover="0"><result status="valid" time="3.36" steps="668"/></proof>
</goal>
<goal name="WP_parameter step1.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.80" steps="189"/></proof>
......@@ -66,13 +66,13 @@
<proof prover="0"><result status="valid" time="0.65" steps="152"/></proof>
</goal>
<goal name="WP_parameter step2.5.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.56" steps="144"/></proof>
<proof prover="0"><result status="valid" time="0.75" steps="144"/></proof>
</goal>
<goal name="WP_parameter step2.5.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter step2.5.5" expl="5. assertion">
<proof prover="5" timelimit="30"><result status="valid" time="9.07"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="7.94"/></proof>
</goal>
</transf>
</goal>
......@@ -108,7 +108,7 @@
<proof prover="0"><result status="valid" time="1.10" steps="198"/></proof>
</goal>
<goal name="WP_parameter prove.8" expl="8. postcondition">
<proof prover="2"><result status="valid" time="0.30"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
......@@ -137,7 +137,7 @@
</transf>
</goal>
</theory>
<theory name="BitCount32bit_fact" sum="b6880c10a1e77dc1b17e81f0dffb63b0">
<theory name="BitCount32bit_fact" sum="feff8f0feb8c8d8608f0ee7b4afd41f9">
<goal name="WP_parameter step1" expl="VC for step1">
<transf name="split_goal_wp">
<goal name="WP_parameter step1.1" expl="1. assertion">
......@@ -146,7 +146,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter step1.1.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="1.50"/></proof>
<proof prover="1"><result status="valid" time="1.98"/></proof>
</goal>
</transf>
</goal>
......@@ -154,7 +154,7 @@
<proof prover="0"><result status="valid" time="3.97" steps="668"/></proof>
</goal>
<goal name="WP_parameter step1.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.59" steps="189"/></proof>
<proof prover="0"><result status="valid" time="0.85" steps="189"/></proof>
</goal>
</transf>
</goal>
......@@ -192,10 +192,10 @@
<proof prover="0"><result status="valid" time="0.07" steps="90"/></proof>
</goal>
<goal name="WP_parameter step2.5.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.73" steps="156"/></proof>
<proof prover="0"><result status="valid" time="1.00" steps="156"/></proof>
</goal>
<goal name="WP_parameter step2.5.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.69" steps="134"/></proof>
<proof prover="0"><result status="valid" time="0.44" steps="134"/></proof>
</goal>
<goal name="WP_parameter step2.5.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -253,7 +253,7 @@
<proof prover="0"><result status="valid" time="0.10" steps="91"/></proof>
</goal>
<goal name="WP_parameter step3.7.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="1.17" steps="170"/></proof>
<proof prover="0"><result status="valid" time="0.88" steps="170"/></proof>
</goal>
<goal name="WP_parameter step3.7.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="1.61" steps="166"/></proof>
......@@ -268,15 +268,15 @@
<proof prover="0"><result status="valid" time="0.03" steps="89"/></proof>
</goal>
<goal name="WP_parameter step3.7.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="0.66" steps="116"/></proof>
<proof prover="0"><result status="valid" time="0.37" steps="116"/></proof>
</goal>
<goal name="WP_parameter step3.7.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.70" steps="117"/></proof>
<proof prover="0"><result status="valid" time="0.52" steps="117"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter step3.8" expl="8. postcondition">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter step3.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.11"/></proof>
......@@ -455,7 +455,7 @@
</transf>
</goal>
</theory>
<theory name="Hamming" sum="35ecca56e9aa178d324fcb694e764bc4">
<theory name="Hamming" sum="9b58a779c8feb91b51e2fe7d25688ccd">
<goal name="WP_parameter hammingD" expl="VC for hammingD">
<transf name="split_goal_wp">
<goal name="WP_parameter hammingD.1" expl="1. assertion">
......@@ -475,7 +475,7 @@
<goal name="WP_parameter separation" expl="VC for separation">
<transf name="split_goal_wp">
<goal name="WP_parameter separation.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="1.92" steps="483"/></proof>
<proof prover="0"><result status="valid" time="1.57" steps="483"/></proof>
</goal>
<goal name="WP_parameter separation.2" expl="2. postcondition">
<transf name="split_goal_wp">
......@@ -493,14 +493,14 @@
<proof prover="2"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<proof prover="1"><result status="valid" time="8.27"/></proof>
<proof prover="1"><result status="valid" time="11.15"/></proof>
</goal>
<goal name="triangleInequality">
<proof prover="0"><result status="valid" time="0.05" steps="69"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="AsciiCode" sum="48ae2dd0d4ba3331da9c91281b7a4b68">
<theory name="AsciiCode" sum="f67bed5792b810f04247cdacac9712a9">
<goal name="WP_parameter bv_even" expl="VC for bv_even">
<transf name="split_goal_wp">
<goal name="WP_parameter bv_even.1" expl="1. assertion">
......@@ -510,7 +510,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter bv_even.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="1.83"/></proof>
<proof prover="1"><result status="valid" time="3.26"/></proof>
</goal>
<goal name="WP_parameter bv_even.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="1.42"/></proof>
......@@ -525,7 +525,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter numof_or" expl="VC for numof_or">
<proof prover="2"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="WP_parameter count_or" expl="VC for count_or">
<transf name="split_goal_wp">
......@@ -550,7 +550,7 @@
<goal name="WP_parameter ascii" expl="VC for ascii">
<transf name="split_goal_wp">
<goal name="WP_parameter ascii.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.32" steps="119"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="119"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter ascii.2" expl="2. assertion">
......@@ -575,7 +575,7 @@
<proof prover="0"><result status="valid" time="0.19" steps="126"/></proof>
</goal>
<goal name="WP_parameter ascii.4.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.58" steps="165"/></proof>
<proof prover="0"><result status="valid" time="0.36" steps="165"/></proof>
</goal>
<goal name="WP_parameter ascii.4.4" expl="4. assertion">
<proof prover="4"><result status="valid" time="0.03"/></proof>
......@@ -604,7 +604,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter tmp.3" expl="3. postcondition">
<proof prover="4"><result status="valid" time="0.59"/></proof>
<proof prover="4"><result status="valid" time="3.80"/></proof>
</goal>
<goal name="WP_parameter tmp.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="2.33" steps="575"/></proof>
......@@ -616,14 +616,14 @@
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
<theory name="GrayCode" sum="d12d6c16d77aa2e0a431490232d609d5" expanded="true">
<theory name="GrayCode" sum="52c91491e78d2a73a7ea96356c874527" expanded="true">
<goal name="iso">
<proof prover="2"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter grayIsGray" expl="VC for grayIsGray" expanded="true">
</goal>
<goal name="nthGray">
<proof prover="0"><result status="valid" time="1.95" steps="487"/></proof>
<proof prover="0"><result status="valid" time="1.38" steps="487"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="lastNthGray">
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="cc40a339e91f8798e286caa7bb80a0e0">
<theory name="Test_proofinuse" sum="6b66e25b5fba98cd9a569192093d2257">
<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="1. assertion">
......@@ -33,7 +33,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="79374fa0e16f15839d139d3dc19925ac">
<theory name="Hackers_delight" sum="41a1e6758d65c0bae347df784a0a0970">
<goal name="DM1">
<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="a95ebf9a8bf11ace664e844cc233ea3a">
<theory name="Hackers_delight_mod" sum="e2658a0de77f1745305297696b3dcc78">
<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="c2bb087b9b1f9714b1604e01d385f9fe">
<theory name="Test_imperial_violet" sum="2b80e9425b02301d47c3e3bd4d79e11f">
<goal name="bv32_bounds_bv">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -174,7 +174,7 @@
<proof prover="4"><result status="valid" time="0.16"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="a8178d2d670a7c2eb3ce6242edd99c0e">
<theory name="Test_from_bitvector_example" sum="c7e027222e90d7cf95c32003b033da18">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<prover id="5" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<file name="../bitwalker.mlw" expanded="true">
<theory name="Bitwalker" sum="7873e88736848debe329f2e4d0306035" expanded="true">
<theory name="Bitwalker" sum="5f74f72afed1573d231ce92e0072a9e5" expanded="true">
<goal name="nth64">
<proof prover="0"><result status="valid" time="0.10" steps="88"/></proof>
</goal>
......@@ -26,7 +26,7 @@
</goal>
<goal name="WP_parameter nth_ultpre0.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.47" steps="210"/></proof>
<proof prover="6"><result status="valid" time="0.17"/></proof>
<proof prover="6"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
</goal>
......@@ -121,7 +121,7 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="1.46" steps="612"/></proof>
<proof prover="0"><result status="valid" time="1.46" steps="611"/></proof>
</goal>
</transf>
</goal>
......@@ -317,10 +317,10 @@
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.9" expl="9. postcondition">
<proof prover="3"><result status="valid" time="1.51"/></proof>
<proof prover="3"><result status="valid" time="2.02"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.10" expl="10. postcondition">
<proof prover="3"><result status="valid" time="0.81"/></proof>
<proof prover="3"><result status="valid" time="1.26"/></proof>
</goal>
</transf>
</goal>
......@@ -508,10 +508,10 @@
<proof prover="0"><result status="valid" time="0.29" steps="129"/></proof>
</goal>
<goal name="WP_parameter poke.27" expl="27. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.20" steps="125"/></proof>
<proof prover="0"><result status="valid" time="1.52" steps="125"/></proof>
</goal>
<goal name="WP_parameter poke.28" expl="28. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.45" steps="119"/></proof>
<proof prover="0"><result status="valid" time="0.75" steps="119"/></proof>
</goal>
<goal name="WP_parameter poke.29" expl="29. loop variant decrease">
<proof prover="0"><result status="valid" time="0.20" steps="104"/></proof>
......@@ -646,7 +646,7 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter pokethenpeek.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="1.58" steps="486"/></proof>
<proof prover="0"><result status="valid" time="1.07" steps="364"/></proof>
</goal>
<goal name="WP_parameter pokethenpeek.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.18" steps="97"/></proof>
......
......@@ -9,7 +9,7 @@
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Utils_Spec" sum="1a4656700b43facbed02dc710dee707b" expanded="true">
<theory name="Utils_Spec" sum="8d66aa65cf0031e1020f4029b30f5d6e" expanded="true">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -17,7 +17,7 @@
<proof prover="0"><result status="valid" time="0.70" steps="241"/></proof>
</goal>
<goal name="countStep">
<proof prover="1"><result status="valid" time="6.13"/></proof>
<proof prover="1"><result status="valid" time="7.33"/></proof>
</goal>
<goal name="WP_parameter numof_shift" expl="VC for numof_shift">
<proof prover="1"><result status="valid" time="0.24"/></proof>
......@@ -28,12 +28,12 @@
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="1.06" steps="282"/></proof>
<proof prover="0"><result status="valid" time="0.71" steps="282"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3" expl="3. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter countSpec_Aux.3.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.22" steps="150"/></proof>
<proof prover="0"><result status="valid" time="0.37" steps="150"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="3.97" steps="535"/></proof>
......@@ -42,7 +42,7 @@
<proof prover="0"><result status="valid" time="0.51" steps="162"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion">
<proof prover="5"><result status="valid" time="4.30"/></proof>
<proof prover="5"><result status="valid" time="3.20"/></proof>
</goal>
</transf>
</goal>
......@@ -71,12 +71,12 @@
<proof prover="1"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter numof_or" expl="VC for numof_or">
<proof prover="1"><result status="valid" time="0.53"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="3.36"/></proof>
<proof prover="4"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="78"/></proof>
......@@ -87,12 +87,12 @@
<proof prover="0"><result status="valid" time="5.87" steps="726"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="26cb4b8b52fdf2b9695b4739a03ceea8" expanded="true">
<theory name="Hackers_delight" sum="617e4501d9edb885b1602897d4f5946e" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="asciiProp">
<proof prover="1"><result status="valid" time="1.16"/></proof>
<proof prover="1"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="iso">
<proof prover="1"><result status="valid" time="0.43"/></proof>
......@@ -101,7 +101,7 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="nthGray">
<proof prover="0"><result status="valid" time="1.67" steps="542"/></proof>
<proof prover="0"><result status="valid" time="1.67" steps="544"/></proof>
</goal>
<goal name="lastNthGray">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="4323a4a26de18896077cd90d9a37ffcf" expanded="true">
<theory name="TestBV" sum="4865db8e2eaaed56c326f2db4d1f8135" expanded="true">
<goal name="g1">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......
This diff is collapsed.
......@@ -8,11 +8,11 @@
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" expanded="true">
<theory name="Rmbt" sum="8b7e47a05b0ba582f9171c5d62077316" expanded="true">
<theory name="Rmbt" sum="6445b4e19089da0d1885e4a56720b0af" expanded="true">
<goal name="WP_parameter min_elt" expl="VC for min_elt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter min_elt.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="2.18" steps="182"/></proof>
<proof prover="0"><result status="valid" time="0.76" steps="183"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
......
......@@ -8,7 +8,7 @@
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../bv.why" expanded="true">
<theory name="CheckBV64" sum="3667990497edb88e067efe68d8b0bb8b" expanded="true">
<theory name="CheckBV64" sum="924d69a2ab94b2c86fe8c9ed16a284ed" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -246,7 +246,7 @@
</goal>
<goal name="f2" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="1.17"/></proof>
<proof prover="1"><result status="unknown" time="0.77"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -323,19 +323,19 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Nth_Bv_bw_and" expanded="true">
<proof prover="0"><result status="valid" time="0.15" steps="164"/></proof>
<proof prover="0"><result status="valid" time="0.31" steps="157"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_Bv_bw_or" expanded="true">
<proof prover="0"><result status="valid" time="0.18" steps="190"/></proof>
<proof prover="0"><result status="valid" time="0.43" steps="190"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_Bv_bw_xor" expanded="true">
<proof prover="0"><result status="valid" time="0.54" steps="234"/></proof>
<proof prover="0"><result status="valid" time="0.34" steps="234"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -385,7 +385,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="CheckBV32" sum="32c898047541b7dddb4509df1082a714" expanded="true">
<theory name="CheckBV32" sum="a20bb735a9bd80ad59aa332112583db0" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -553,7 +553,7 @@
</goal>
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.43"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.75"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -588,7 +588,7 @@
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.98"/></proof>
<proof prover="1"><result status="unknown" time="1.25"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -608,7 +608,7 @@
<proof prover="4"><result status="timeout" time="4.99"/></proof>
</goal>
</theory>
<theory name="CheckBV16" sum="48ef2f5bab124330528a2a0693742385" expanded="true">
<theory name="CheckBV16" sum="1e2b04b4b36c64a8073154d136a386e5" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -804,7 +804,7 @@
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="0.78"/></proof>
<proof prover="1"><result status="unknown" time="0.53"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -831,7 +831,7 @@
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
</theory>
<theory name="CheckBV8" sum="a92468f6e69e618390432ba249f6522a" expanded="true">
<theory name="CheckBV8" sum="a04987af6bd7d770f56a439329cbebc9" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -1027,7 +1027,7 @@
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.51"/></proof>
<proof prover="1"><result status="unknown" time="0.72"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......
......@@ -228,9 +228,9 @@ theory BV_Gen
axiom to_int_extensionality:
forall v,v':t. to_int v = to_int v' -> v = v'
(*
(**)
predicate uint_in_range (i : int) = (Int.(<=) 0 i) /\ (Int.(<=) i max_int)
*)
(**)
axiom to_uint_bounds :
(*
......
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