Skip to content

why3
why3
Commit 6c985576 authored by Clément Fumex's avatar Clément Fumex
Browse files
Options

remove unecessary axioms from bv theory clones and consequently fix examples

parent 98920324
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 815 additions and 814 deletions
examples/binary_search/why3session.xml
View file @ 6c985576
......@@ -20,87 +20,87 @@
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="be00e964eb6971d378bc5e7bb474a32c" expanded="true">
<theory name="BinarySearchInt32" sum="e1d44ffe67ec79d3738d89b5a90b5f4e" 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">
<proof prover="5"><result status="valid" time="0.02" steps="70"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="74"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="73"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="5"><result status="valid" time="0.12" steps="95"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="93"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="75"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="74"/></proof>
</goal>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="78"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="77"/></proof>
</goal>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="86"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="90"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="89"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="5"><result status="valid" time="0.01" steps="83"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="82"/></proof>
</goal>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow">
<proof prover="5"><result status="valid" time="0.04" steps="98"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="97"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="5"><result status="valid" time="0.11" steps="115"/></proof>
<proof prover="5"><result status="valid" time="0.11" steps="113"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="5"><result status="valid" time="0.27" steps="135"/></proof>
<proof prover="5"><result status="valid" time="0.27" steps="132"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="90"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="89"/></proof>
</goal>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="94"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="93"/></proof>
</goal>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow">
<proof prover="5"><result status="valid" time="0.03" steps="111"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="110"/></proof>
</goal>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02" steps="98"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="97"/></proof>
</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.48"/></proof>
<proof prover="5"><result status="valid" time="1.34" steps="179"/></proof>
<proof prover="5"><result status="valid" time="1.34" steps="176"/></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>
<proof prover="5"><result status="valid" time="0.02" steps="97"/></proof>
</goal>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="94"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="93"/></proof>
</goal>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="96"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="112"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="111"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02" steps="100"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<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.35" steps="180"/></proof>
<proof prover="5"><result status="valid" time="1.35" steps="177"/></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>
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="5"><result status="valid" time="0.08" steps="124"/></proof>
<proof prover="5"><result status="valid" time="0.08" steps="123"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="5"><result status="valid" time="0.01" steps="89"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="88"/></proof>
</goal>
</transf>
</goal>
......
examples/bitcount/why3session.xml
View file @ 6c985576
This diff is collapsed.
examples/bitvector_examples/why3session.xml
View file @ 6c985576
......@@ -6,20 +6,20 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="07c8006854818f4db988d4a84c3268d8">
<theory name="Test_proofinuse" sum="01976ddc6bd80d04acbe32f98fd3ce49">
<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">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.48" steps="137"/></proof>
<proof prover="0"><result status="valid" time="0.48" steps="136"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="1.22" steps="204"/></proof>
<proof prover="0"><result status="valid" time="1.22" steps="203"/></proof>
</goal>
</transf>
</goal>
......@@ -33,7 +33,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="395a75dc4b0cc7fc0536ed41f36f5037">
<theory name="Hackers_delight" sum="a0944cec62c66f9386bc79e4c44a0f16">
<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="3368368fc763a9636a041fa5fbf676b5">
<theory name="Hackers_delight_mod" sum="32d38cd9c48389171edd12feea17b382">
<goal name="WP_parameter dm1" expl="VC for dm1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -154,27 +154,27 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="ba5c44837be65648a368ce40462016a6">
<theory name="Test_imperial_violet" sum="3b53ccfb24b0e5076075a7389a6e49e5">
<goal name="bv32_bounds_bv">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="to_int_ule">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="to_int_ult">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="bv32_bounds_0">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="bv32_bounds">
<proof prover="0"><result status="valid" time="0.03" steps="71"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="4"><result status="valid" time="0.16"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="be711e308d713570e8236111ea0953af">
<theory name="Test_from_bitvector_example" sum="6b18dfa01a56b248764549f53590545a">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......
examples/bitwalker/why3session.xml
View file @ 6c985576
This diff is collapsed.
examples/hackers-delight/why3session.xml
View file @ 6c985576
......@@ -11,12 +11,12 @@
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Utils_Spec" sum="9fc49581a1bc529e9494ae285461e220" expanded="true">
<theory name="Utils_Spec" sum="b1d2e3d07b9e6cc8c94261984c153613" expanded="true">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="numOfZero">
<proof prover="0"><result status="valid" time="0.70" steps="241"/></proof>
<proof prover="0"><result status="valid" time="0.70" steps="245"/></proof>
</goal>
<goal name="countStep">
<proof prover="1"><result status="valid" time="3.07"/></proof>
......@@ -27,21 +27,21 @@
<goal name="WP_parameter countSpec_Aux" expl="VC for countSpec_Aux">
<transf name="split_goal_wp">
<goal name="WP_parameter countSpec_Aux.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.71" steps="282"/></proof>
<proof prover="0"><result status="valid" time="0.71" steps="277"/></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.20" steps="150"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="149"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="2.59" steps="535"/></proof>
<proof prover="0"><result status="valid" time="2.59" steps="534"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.51" steps="162"/></proof>
<proof prover="0"><result status="valid" time="0.51" steps="153"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion">
<proof prover="5"><result status="valid" time="2.29"/></proof>
......@@ -54,7 +54,7 @@
</transf>
</goal>
<goal name="countSpec">
<proof prover="0"><result status="valid" time="0.05" steps="74"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="70"/></proof>
</goal>
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec">
<transf name="split_goal_wp">
......@@ -80,27 +80,27 @@
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter triangleInequalityInt.1.1" expl="1. VC for triangleInequalityInt" expanded="true">
<proof prover="3"><result status="valid" time="0.06" steps="133"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="132"/></proof>
<proof prover="5"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.1.2" expl="2. VC for triangleInequalityInt" expanded="true">
<proof prover="2"><result status="valid" time="0.56"/></proof>
<proof prover="3"><result status="valid" time="0.28" steps="258"/></proof>
<proof prover="3"><result status="valid" time="0.28" steps="257"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.21"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="109"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="108"/></proof>
</goal>
</transf>
</goal>
<goal name="triangleInequality">
<proof prover="0"><result status="valid" time="4.49" steps="726"/></proof>
<proof prover="0"><result status="valid" time="4.49" steps="724"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="20348474bf14b2e0397f38eb0d273205" expanded="true">
<theory name="Hackers_delight" sum="84e0d744dbc0570b981d4bb3668fa3de" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
......@@ -114,7 +114,7 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="nthGray">
<proof prover="0"><result status="valid" time="1.23" steps="544"/></proof>
<proof prover="0"><result status="valid" time="1.23" steps="532"/></proof>
</goal>
<goal name="lastNthGray">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -156,13 +156,13 @@
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Ac">
<proof prover="0"><result status="valid" time="0.47" steps="319"/></proof>
<proof prover="0"><result status="valid" time="0.47" steps="308"/></proof>
</goal>
<goal name="Ad">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Ae">
<proof prover="0"><result status="valid" time="0.05" steps="71"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="70"/></proof>
</goal>
<goal name="Af">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......
examples/logic/bitvectors/why3session.xml
View file @ 6c985576
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="91c100138a6a2604b6b10a1c52ef233c" expanded="true">
<theory name="TestBV" sum="6c2c5b15e24e53abc1436fd01209978b" 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>
......@@ -62,12 +62,12 @@
<proof prover="4"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g4a">
<proof prover="0"><result status="valid" time="0.14" steps="85"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="84"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g4b">
<proof prover="0"><result status="valid" time="0.06" steps="85"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="84"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -100,12 +100,12 @@
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="g6a">
<proof prover="0"><result status="valid" time="0.03" steps="72"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g6b">
<proof prover="0"><result status="valid" time="0.02" steps="72"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -136,7 +136,7 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="gtt">
<proof prover="0"><result status="valid" time="0.13" steps="80"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="79"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
......
examples/queens_bv/why3session.xml
View file @ 6c985576
This diff is collapsed.
examples/rightmostbittrick/why3session.xml
View file @ 6c985576
......@@ -8,11 +8,11 @@
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" expanded="true">
<theory name="Rmbt" sum="878556699fa845f3c95c99b591364617" expanded="true">
<theory name="Rmbt" sum="20adbd3247e4350745dafae5c88a22b8" expanded="true">
<goal name="WP_parameter rightmost_position_set" expl="VC for rightmost_position_set" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter rightmost_position_set.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.05" steps="82"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="80"/></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>
......@@ -23,7 +23,7 @@
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter rightmost_position_set.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="1.25" steps="250"/></proof>
<proof prover="0"><result status="valid" time="1.25" steps="240"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -32,14 +32,14 @@
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter rightmost_position_set.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter rightmost_position_set.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
......@@ -50,8 +50,8 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter rightmost_position_set.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="70"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -65,7 +65,7 @@
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter rightmost_bit_trick.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.04" steps="69"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="68"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
......@@ -76,26 +76,26 @@
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="97"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="98"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.18" steps="125"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="122"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.6" expl="6. postcondition">
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.7" expl="7. postcondition">
<proof prover="2"><result status="valid" time="0.18"/></proof>
<goal name="WP_parameter rightmost_bit_trick.7" expl="7. postcondition" expanded="true">
<proof prover="2" steplimit="-1"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.15" steps="134"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="133"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
......
examples/tests-provers/bv/why3session.xml
View file @ 6c985576
This diff is collapsed.
theories/bv.why
View file @ 6c985576
......@@ -402,11 +402,10 @@ theory BV64
clone export BV_Gen with
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
constant max_int = max_int,
goal size_pos,
goal two_power_size_val,
goal max_int_val
end
......@@ -418,11 +417,10 @@ theory BV32
clone export BV_Gen with
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
constant max_int = max_int,
goal size_pos,
goal two_power_size_val,
goal max_int_val
end
......@@ -434,11 +432,10 @@ theory BV16
clone export BV_Gen with
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
constant max_int = max_int,
goal size_pos,
goal two_power_size_val,
goal max_int_val
end
......@@ -450,11 +447,10 @@ theory BV8
clone export BV_Gen with
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
constant max_int = max_int,
goal size_pos,
goal two_power_size_val,
goal max_int_val
end
......
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