- Add nth_bv_def and eq_sub_bv_def axioms to bv.BV_Gen and remove nth_bv

definitions in smtlib-bv driver. - Add no-bv.gen driver file targeted to provers without support for the smtlib bv theory (or for the no_bv variants). - update realization & tests

- Add nth_bv_def and eq_sub_bv_def axioms to bv.BV_Gen and remove nth_bv
definitions in smtlib-bv driver. - Add no-bv.gen driver file targeted to provers without support for the smtlib bv theory (or for the no_bv variants). - update realization & tests
590a8eb5 · Clément Fumex · 34ca0de3 · 590a8eb5 · 590a8eb5 · 590a8eb5
Commit 590a8eb5 authored Nov 30, 2015 by Clément Fumex
28 changed files
--- a/drivers/alt_ergo.drv
+++ b/drivers/alt_ergo.drv
 (* Driver for Alt-Ergo version >= 0.95 *)

 import "alt_ergo_common.drv"
+import "no-bv.gen"

 theory BuiltIn


--- a/drivers/cvc4.drv
+++ b/drivers/cvc4.drv
@@ -8,6 +8,7 @@ prelude "(set-logic AUFNIRA)"
 *)

 import "smt-libv2.drv"
+import "no-bv.gen"
 import "discrimination.gen"

 transformation "inline_trivial"

--- a/drivers/no-bv.gen
+++ b/drivers/no-bv.gen
+(* Why3 driver for noBV alternatives on bit-vector theories *)
+
+theory bv.BV_Gen
+  remove prop nth_bv_def
+  remove prop eq_sub_bv_def
+
+  remove prop to_uint_add
+  remove prop to_uint_sub
+  remove prop to_uint_mul
+end
\ No newline at end of file
--- a/drivers/smt-libv2-bv.gen
+++ b/drivers/smt-libv2-bv.gen
@@ -22,16 +22,25 @@ theory bv.BV_Gen

  (* Warning: we should NOT remove all the axioms using "allprops" *)

+  remove prop size_pos
  remove prop nth_out_of_bound
  remove prop Nth_zero
  remove prop Nth_ones
  remove prop two_power_size_val
  remove prop max_int_val
-  remove prop eq_sub_equiv
  remove prop Nth_bw_or
  remove prop Nth_bw_and
  remove prop Nth_bw_xor
  remove prop Nth_bw_not
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop lsr_zero
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop asr_zero
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+  remove prop lsl_zero
  remove prop Nth_rotate_left
  remove prop Nth_rotate_right

@@ -72,12 +81,6 @@ theory bv.BV64
  syntax function zero "#x0000000000000000"
  syntax function ones "#xFFFFFFFFFFFFFFFF"

-  syntax function nth_bv
-    "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
-(* possible alternative definition :
-    "(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
-*)
-
  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
 end
@@ -88,9 +91,6 @@ theory bv.BV32
  syntax function zero "#x00000000"
  syntax function ones "#xFFFFFFFF"

-  syntax function nth_bv
-    "(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
-
  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
 end
@@ -101,9 +101,6 @@ theory bv.BV16
  syntax function zero "#x0000"
  syntax function ones "#xFFFF"

-  syntax function nth_bv
-    "(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
-
  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
 end
@@ -114,9 +111,6 @@ theory bv.BV8
  syntax function zero "#x00"
  syntax function ones "#xFF"

-  syntax function nth_bv
-    "(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
-
  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
 end

--- a/drivers/z3_432.drv
+++ b/drivers/z3_432.drv
@@ -9,6 +9,7 @@ model_parser "smtv2"


 import "smt-libv2.drv"
+import "no-bv.gen"
 import "discrimination.gen"

 transformation "inline_trivial"

--- a/examples/binary_search/why3session.xml
+++ b/examples/binary_search/why3session.xml
@@ -2,9 +2,9 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
-<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
-<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
+<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" 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">
@@ -20,7 +20,7 @@
 <proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchInt32" sum="84d73d964ac2e52c2a4c56e898a3c5f5" expanded="true">
+<theory name="BinarySearchInt32" sum="be00e964eb6971d378bc5e7bb474a32c" 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">
@@ -70,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="4.16"/></proof>
-  <proof prover="5"><result status="valid" time="1.68" steps="179"/></proof>
+  <proof prover="2"><result status="valid" time="3.48"/></proof>
+  <proof prover="5"><result status="valid" time="1.34" 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>
@@ -91,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.99" steps="180"/></proof>
+  <proof prover="5"><result status="valid" time="1.35" 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>

--- a/examples/binary_search/why3shapes.gz
+++ b/examples/binary_search/why3shapes.gz
--- a/examples/bitcount/why3session.xml
+++ b/examples/bitcount/why3session.xml
@@ -2,13 +2,13 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
-<prover id="1" name="CVC3" version="2.4.1" timelimit="30" memlimit="1000"/>
-<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"/>
-<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="30" memlimit="1000"/>
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="1" name="CVC3" version="2.4.1" timelimit="30" steplimit="1" memlimit="1000"/>
+<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"/>
+<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="30" steplimit="1" memlimit="1000"/>
 <file name="../bitcount.mlw" expanded="true">
-<theory name="BitCount8bit_fact" sum="5751fad0b4d740cb2042ca2423c25c5e" expanded="true">
+<theory name="BitCount8bit_fact" sum="82f55971729b6150d50930dbb531ed9c" expanded="true">
 <goal name="nth_as_bv_is_int">
 <proof prover="0"><result status="valid" time="0.18" steps="95"/></proof>
 </goal>
@@ -25,10 +25,10 @@
  </transf>
  </goal>
  <goal name="WP_parameter step1.2" expl="2. postcondition">
-  <proof prover="0"><result status="valid" time="3.36" steps="668"/></proof>
+  <proof prover="0"><result status="valid" time="2.88" 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>
+  <proof prover="0"><result status="valid" time="0.50" steps="189"/></proof>
  </goal>
 </transf>
 </goal>
@@ -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.75" steps="144"/></proof>
+   <proof prover="0"><result status="valid" time="0.42" 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"><result status="valid" time="7.94"/></proof>
+   <proof prover="5"><result status="valid" time="5.20"/></proof>
   </goal>
  </transf>
  </goal>
@@ -80,7 +80,7 @@
  <proof prover="2"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="WP_parameter step2.7" expl="7. postcondition">
-  <proof prover="0"><result status="valid" time="0.50" steps="133"/></proof>
+  <proof prover="0"><result status="valid" time="0.32" steps="133"/></proof>
  </goal>
 </transf>
 </goal>
@@ -137,19 +137,23 @@
 </transf>
 </goal>
 </theory>
-<theory name="BitCounting32" sum="9f25f7ff7a6a81cbcd2f8a85a25ec49b" expanded="true">
- <goal name="WP_parameter proof0" expl="VC for proof0">
- <transf name="split_goal_wp">
+<theory name="BitCounting32" sum="10b4e91da18a7fca9af40b70ea189ff4" 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="1. assertion">
  <proof prover="0"><result status="valid" time="0.04" steps="81"/></proof>
  </goal>
  <goal name="WP_parameter proof0.2" expl="2. assertion">
  <proof prover="0"><result status="valid" time="0.03" steps="79"/></proof>
  </goal>
-  <goal name="WP_parameter proof0.3" expl="3. assertion">
-  <transf name="split_goal_wp">
-   <goal name="WP_parameter proof0.3.1" expl="1. VC for proof0">
-   <proof prover="2"><result status="valid" time="0.12"/></proof>
+  <goal name="WP_parameter proof0.3" expl="3. assertion" expanded="true">
+  <transf name="split_goal_wp" expanded="true">
+   <goal name="WP_parameter proof0.3.1" expl="1. VC for proof0" expanded="true">
+   <transf name="introduce_premises" expanded="true">
+    <goal name="WP_parameter proof0.3.1.1" expl="1. VC for proof0" expanded="true">
+    <proof prover="2" steplimit="-1"><result status="valid" time="0.17"/></proof>
+    </goal>
+   </transf>
   </goal>
   <goal name="WP_parameter proof0.3.2" expl="2. VC for proof0">
   <proof prover="0"><result status="valid" time="0.04" steps="110"/></proof>
@@ -160,7 +164,7 @@
  </transf>
  </goal>
  <goal name="WP_parameter proof0.4" expl="4. postcondition">
-  <proof prover="0"><result status="valid" time="0.45" steps="305"/></proof>
+  <proof prover="0"><result status="valid" time="0.29" steps="305"/></proof>
  </goal>
 </transf>
 </goal>
@@ -226,7 +230,7 @@
  <proof prover="0"><result status="valid" time="0.06" steps="91"/></proof>
  </goal>
  <goal name="WP_parameter proof2.8" expl="8. assertion">
-  <proof prover="0"><result status="valid" time="0.91" steps="153"/></proof>
+  <proof prover="0"><result status="valid" time="0.58" steps="153"/></proof>
  </goal>
  <goal name="WP_parameter proof2.9" expl="9. assertion">
  <proof prover="0"><result status="valid" time="0.80" steps="151"/></proof>
@@ -279,7 +283,7 @@
  <proof prover="0"><result status="valid" time="0.05" steps="93"/></proof>
  </goal>
  <goal name="WP_parameter proof3.10" expl="10. assertion">
-  <proof prover="0"><result status="valid" time="1.02" steps="157"/></proof>
+  <proof prover="0"><result status="valid" time="0.57" steps="157"/></proof>
  </goal>
  <goal name="WP_parameter proof3.11" expl="11. assertion">
  <proof prover="0"><result status="valid" time="0.06" steps="93"/></proof>
@@ -378,11 +382,11 @@
 </transf>
 </goal>
 </theory>
-<theory name="Hamming" sum="dfdc0f1acb686591cb859b028bb81cbe" expanded="true">
+<theory name="Hamming" sum="d1fbefaa3e308a6b50a604fbf93f3876" expanded="true">
 <goal name="WP_parameter hammingD" expl="VC for hammingD">
 <transf name="split_goal_wp">
  <goal name="WP_parameter hammingD.1" expl="1. assertion">
-  <proof prover="0"><result status="valid" time="1.42" steps="409"/></proof>
+  <proof prover="0"><result status="valid" time="1.00" steps="409"/></proof>
  </goal>
  <goal name="WP_parameter hammingD.2" expl="2. postcondition">
  <proof prover="4"><result status="valid" time="0.02"/></proof>
@@ -393,19 +397,19 @@
 <proof prover="4"><result status="valid" time="0.05"/></proof>
 </goal>
 <goal name="numof_ytpmE">
- <proof prover="2"><result status="valid" time="1.89"/></proof>
+ <proof prover="2"><result status="valid" time="1.04"/></proof>
 </goal>
 <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.87" steps="473"/></proof>
+  <proof prover="0"><result status="valid" time="1.23" steps="473"/></proof>
  </goal>
  <goal name="WP_parameter separation.2" expl="2. postcondition">
  <transf name="split_goal_wp">
-   <goal name="WP_parameter separation.2.1" expl="1. postcondition">
-   <proof prover="0"><result status="valid" time="0.03" steps="73"/></proof>
+   <goal name="WP_parameter separation.2.1" expl="1. VC for separation">
+   <proof prover="0"><result status="valid" time="0.04" steps="73"/></proof>
   </goal>
-   <goal name="WP_parameter separation.2.2" expl="2. postcondition">
+   <goal name="WP_parameter separation.2.2" expl="2. VC for separation">
   <proof prover="0"><result status="valid" time="0.65" steps="313"/></proof>
   </goal>
  </transf>
@@ -413,17 +417,17 @@
 </transf>
 </goal>
 <goal name="WP_parameter numof_or" expl="VC for numof_or">
- <proof prover="2"><result status="valid" time="0.50"/></proof>
+ <proof prover="2"><result status="valid" time="0.32"/></proof>
 </goal>
 <goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
- <proof prover="1"><result status="valid" time="9.24"/></proof>
+ <proof prover="1"><result status="valid" time="7.31"/></proof>
 </goal>
 <goal name="triangleInequality">
- <proof prover="0"><result status="valid" time="0.05" steps="75"/></proof>
+ <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="65a00d71812a6ba057f736c4159b37f1" expanded="true">
+<theory name="AsciiCode" sum="a0efd55626df3e4e4cb720eead890c7a" 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="1. assertion">
@@ -433,10 +437,10 @@
  <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="2.41"/></proof>
+  <proof prover="1"><result status="valid" time="3.21"/></proof>
  </goal>
  <goal name="WP_parameter bv_even.4" expl="4. assertion">
-  <proof prover="1"><result status="valid" time="1.75"/></proof>
+  <proof prover="1"><result status="valid" time="0.42"/></proof>
  </goal>
  <goal name="WP_parameter bv_even.5" expl="5. postcondition">
  <proof prover="0"><result status="valid" time="0.09" steps="115"/></proof>
@@ -448,7 +452,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.38"/></proof>
+ <proof prover="2"><result status="valid" time="0.22"/></proof>
 </goal>
 <goal name="WP_parameter count_or" expl="VC for count_or">
 <transf name="split_goal_wp">
@@ -462,7 +466,7 @@
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="WP_parameter count_or.4" expl="4. assertion">
-  <proof prover="5" timelimit="5"><result status="valid" time="2.21"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="1.43"/></proof>
  </goal>
  <goal name="WP_parameter count_or.5" expl="5. postcondition">
  <proof prover="0"><result status="valid" time="0.06" steps="74"/></proof>
@@ -473,7 +477,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.13" steps="117"/></proof>
+  <proof prover="0"><result status="valid" time="0.30" steps="244"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="WP_parameter ascii.2" expl="2. assertion">
@@ -492,13 +496,13 @@
  <goal name="WP_parameter ascii.4" expl="4. assertion">
  <transf name="split_goal_wp">
   <goal name="WP_parameter ascii.4.1" expl="1. assertion">
-   <proof prover="0"><result status="valid" time="0.08" steps="100"/></proof>
+   <proof prover="0"><result status="valid" time="0.08" steps="94"/></proof>
   </goal>
   <goal name="WP_parameter ascii.4.2" expl="2. assertion">
-   <proof prover="0"><result status="valid" time="0.19" steps="123"/></proof>
+   <proof prover="0"><result status="valid" time="0.19" steps="119"/></proof>
   </goal>
   <goal name="WP_parameter ascii.4.3" expl="3. assertion">
-   <proof prover="0"><result status="valid" time="0.55" steps="162"/></proof>
+   <proof prover="0"><result status="valid" time="0.55" steps="177"/></proof>
   </goal>
   <goal name="WP_parameter ascii.4.4" expl="4. assertion">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
@@ -530,12 +534,12 @@
  <proof prover="4"><result status="valid" time="0.98"/></proof>
  </goal>
  <goal name="WP_parameter tmp.4" expl="4. postcondition">
-  <proof prover="0"><result status="valid" time="1.89" steps="575"/></proof>
+  <proof prover="0"><result status="valid" time="1.38" steps="575"/></proof>
  </goal>
 </transf>
 </goal>
 <goal name="asciiProp">
- <proof prover="0"><result status="valid" time="0.40" steps="235"/></proof>
+ <proof prover="0"><result status="valid" time="0.24" steps="235"/></proof>
 <proof prover="2"><result status="valid" time="0.05"/></proof>
 </goal>
 </theory>

--- a/examples/bitcount/why3shapes.gz
+++ b/examples/bitcount/why3shapes.gz
--- a/examples/bitvector_examples/why3session.xml
+++ b/examples/bitvector_examples/why3session.xml
@@ -2,18 +2,18 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
-<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"/>
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<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="6b66e25b5fba98cd9a569192093d2257">
+<theory name="Test_proofinuse" sum="07c8006854818f4db988d4a84c3268d8">
 <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.66" steps="137"/></proof>
+  <proof prover="0"><result status="valid" time="0.48" steps="137"/></proof>
  </goal>
  <goal name="WP_parameter shift_is_div.3" expl="3. assertion">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
@@ -33,7 +33,7 @@
 <proof prover="2"><result status="valid" time="0.08"/></proof>
 </goal>
 </theory>
-<theory name="Hackers_delight" sum="41a1e6758d65c0bae347df784a0a0970">
+<theory name="Hackers_delight" sum="395a75dc4b0cc7fc0536ed41f36f5037">
 <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="e2658a0de77f1745305297696b3dcc78">
+<theory name="Hackers_delight_mod" sum="3368368fc763a9636a041fa5fbf676b5">
 <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="2b80e9425b02301d47c3e3bd4d79e11f">
+<theory name="Test_imperial_violet" sum="ba5c44837be65648a368ce40462016a6">
 <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="c7e027222e90d7cf95c32003b033da18">
+<theory name="Test_from_bitvector_example" sum="be711e308d713570e8236111ea0953af">
 <goal name="Test1">
 <proof prover="2"><result status="valid" time="0.03"/></proof>
 </goal>

--- a/examples/bitvector_examples/why3shapes.gz
+++ b/examples/bitvector_examples/why3shapes.gz
--- a/examples/bitwalker/why3session.xml
+++ b/examples/bitwalker/why3session.xml
@@ -2,14 +2,14 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
-<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
-<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
-<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
-<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"/>
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
 <file name="../bitwalker.mlw" expanded="true">
-<theory name="Bitwalker" sum="5f74f72afed1573d231ce92e0072a9e5" expanded="true">
+<theory name="Bitwalker" sum="9755ce6626677472899148634ff24705" expanded="true">
 <goal name="nth64">
 <proof prover="0"><result status="valid" time="0.10" steps="88"/></proof>
 </goal>
@@ -25,8 +25,8 @@
  <proof prover="1"><result status="valid" time="0.16"/></proof>
  </goal>
  <goal name="WP_parameter nth_ultpre0.3" expl="3. postcondition">
-  <proof prover="0"><result status="valid" time="0.52" steps="210"/></proof>
-  <proof prover="6"><result status="valid" time="0.30"/></proof>
+  <proof prover="0"><result status="valid" time="0.36" steps="198"/></proof>
+  <proof prover="6"><result status="valid" time="0.12"/></proof>
  </goal>
 </transf>
 </goal>
@@ -61,7 +61,7 @@
  </goal>
  <goal name="WP_parameter poke_64bit_bv.9" expl="9. postcondition">
  <proof prover="0"><result status="valid" time="0.34" steps="188"/></proof>
-  <proof prover="6"><result status="valid" time="0.22"/></proof>
+  <proof prover="6"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="WP_parameter poke_64bit_bv.10" expl="10. postcondition">
  <proof prover="0"><result status="valid" time="0.29" steps="163"/></proof>
@@ -81,13 +81,13 @@
  <proof prover="0"><result status="valid" time="0.04" steps="78"/></proof>
  </goal>
  <goal name="WP_parameter poke_64bit.4" expl="4. VC for poke_64bit">
-  <proof prover="1"><result status="valid" time="0.07"/></proof>
+  <proof prover="1"><result status="valid" time="0.31"/></proof>
  </goal>
  <goal name="WP_parameter poke_64bit.5" expl="5. VC for poke_64bit">
-  <proof prover="1"><result status="valid" time="0.06"/></proof>
+  <proof prover="1"><result status="valid" time="0.18"/></proof>
  </goal>
  <goal name="WP_parameter poke_64bit.6" expl="6. VC for poke_64bit">
-  <proof prover="1"><result status="valid" time="0.06"/></proof>
+  <proof prover="1"><result status="valid" time="0.32"/></proof>
  </goal>
  <goal name="WP_parameter poke_64bit.7" expl="7. VC for poke_64bit">
  <proof prover="1"><result status="valid" time="0.07"/></proof>
@@ -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.56" steps="611"/></proof>
+  <proof prover="0"><result status="valid" time="1.56" steps="612"/></proof>
  </goal>
 </transf>
 </goal>
@@ -238,7 +238,7 @@
  </goal>
  <goal name="WP_parameter peek.19" expl="19. loop invariant preservation">
  <proof prover="5"><result status="valid" time="0.02"/></proof>
-  <proof prover="6"><result status="valid" time="0.25"/></proof>
+  <proof prover="6"><result status="valid" time="0.11"/></proof>
  </goal>
  <goal name="WP_parameter peek.20" expl="20. loop variant decrease">
  <proof prover="0"><result status="valid" time="0.14" steps="104"/></proof>
@@ -276,7 +276,7 @@
  <proof prover="3"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="WP_parameter peek_64bit.5" expl="5. VC for peek_64bit">
-  <proof prover="1"><result status="valid" time="0.06"/></proof>
+  <proof prover="1"><result status="valid" time="0.22"/></proof>
  </goal>
  <goal name="WP_parameter peek_64bit.6" expl="6. postcondition">
  <proof prover="0"><result status="valid" time="0.07" steps="133"/></proof>
@@ -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.68"/></proof>
+  <proof prover="3"><result status="valid" time="0.83"/></proof>
  </goal>
  <goal name="WP_parameter poke_8bit.10" expl="10. postcondition">
-  <proof prover="3"><result status="valid" time="0.88"/></proof>
+  <proof prover="3"><result status="valid" time="0.09"/></proof>
  </goal>
 </transf>
 </goal>
@@ -357,7 +357,7 @@
  <goal name="WP_parameter poke_8bit_array.6" expl="6. precondition">
  <proof prover="0"><result status="valid" time="0.34" steps="196"/></proof>
  <proof prover="1"><result status="valid" time="0.08"/></proof>
-  <proof prover="3"><result status="valid" time="1.52"/></proof>
+  <proof prover="3"><result status="valid" time="1.26"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="WP_parameter poke_8bit_array.7" expl="7. index in array bounds">

--- a/examples/bitwalker/why3shapes.gz
+++ b/examples/bitwalker/why3shapes.gz
--- a/examples/hackers-delight.mlw
+++ b/examples/hackers-delight.mlw
@@ -131,9 +131,9 @@ module Utils_Spec
  let lemma triangleInequalityInt (a b c : t) : unit
    ensures {to_uint (hammingD a b) + to_uint (hammingD b c) >= to_uint (hammingD a c)}
  =
-    assert {numof (nth_diff a b) 0 32 + numof (nth_diff b c) 0 32 >=
-    numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >=
-    numof (nth_diff a c) 0 32}
+    assert {numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >= numof (nth_diff a c) 0 32
+             by
+            forall j:int. 0 <= j < 32 -> nth_diff a c j -> fun_or (nth_diff a b) (nth_diff b c) j}

  lemma triangleInequality: forall a b c.
    uge (add (hammingD a b) (hammingD b c)) (hammingD a c)

--- a/examples/hackers-delight/why3session.xml
+++ b/examples/hackers-delight/why3session.xml
@@ -2,14 +2,16 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
-<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
-<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"/>
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.4.0" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="1.10.prv" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
 <file name="../hackers-delight.mlw" expanded="true">
 <theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Utils_Spec" sum="8d66aa65cf0031e1020f4029b30f5d6e" expanded="true">
+<theory name="Utils_Spec" sum="9fc49581a1bc529e9494ae285461e220" expanded="true">
 <goal name="countZero">
 <proof prover="1"><result status="valid" time="0.03"/></proof>
 </goal>
@@ -17,7 +19,7 @@
 <proof prover="0"><result status="valid" time="0.70" steps="241"/></proof>