add eq_sub to bit vector theory

update test suite add out of bound axiom for nth test eq_sub update test suite

add eq_sub to bit vector theory
update test suite add out of bound axiom for nth test eq_sub update test suite
cfa84394 · Clément Fumex · Clement Fumex · 6c2488fb · cfa84394 · cfa84394
Commit cfa84394 authored Jul 09, 2015 by Clément Fumex Committed by Clement Fumex Jul 10, 2015
--- a/drivers/smt-libv2-bv.gen
+++ b/drivers/smt-libv2-bv.gen
@@ -19,10 +19,12 @@ theory bv.BV_Gen
  syntax function lsl_bv "(bvshl %1 %2)"
  syntax function asr_bv "(bvashr %1 %2)"
  syntax predicate eq "(= %1 %2)"
-  remove prop Extensionality

+  remove prop nth_out_of_bound
  remove prop Nth_zero
  remove prop Nth_ones
+  remove prop eq_sub_equiv
+  remove prop Extensionality
  remove prop Nth_bw_or
  remove prop Nth_bw_and
  remove prop Nth_bw_xor

--- a/examples/binary_search/why3session.xml
+++ b/examples/binary_search/why3session.xml
@@ -23,7 +23,7 @@
 <proof prover="4"><result status="valid" time="0.03"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchInt32" sum="1a20b53b88547b45b31a04796cdc6796" expanded="true">
+<theory name="BinarySearchInt32" sum="b0206e6010f9baba3c77f13cd10417bd" 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">

--- a/examples/binary_search/why3shapes.gz
+++ b/examples/binary_search/why3shapes.gz
--- a/examples/bitvector_examples/why3session.xml
+++ b/examples/bitvector_examples/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../bitvector_examples.mlw" expanded="true">
-<theory name="Test_proofinuse" sum="28f69746dc8ff9c44df602d0c0d5d0b8" expanded="true">
+<theory name="Test_proofinuse" sum="1aca3c7bef635dbd5aecf175ff827b71" expanded="true">
 <goal name="WP_parameter shift_is_div" expl="VC for shift_is_div" expanded="true">
 <transf name="split_goal_wp" expanded="true">
  <goal name="WP_parameter shift_is_div.1" expl="1. assertion" expanded="true">
@@ -40,7 +40,7 @@
 <proof prover="2"><result status="valid" time="0.08"/></proof>
 </goal>
 </theory>
-<theory name="Hackers_delight" sum="9705eaccc6076bac3885e79a54965be4" expanded="true">
+<theory name="Hackers_delight" sum="36d4b67a06ae48dc17c7462056da280d" expanded="true">
 <goal name="DM1" expanded="true">
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 <proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -103,7 +103,7 @@
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 </goal>
 </theory>
-<theory name="Hackers_delight_mod" sum="d52e2c470f4cc499dd89711163d487dc" expanded="true">
+<theory name="Hackers_delight_mod" sum="67f9a61e4ed788c2b8acae3d1081c0e0" expanded="true">
 <goal name="WP_parameter dm1" expl="VC for dm1" expanded="true">
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -172,7 +172,7 @@
 <proof prover="2"><result status="valid" time="0.07"/></proof>
 </goal>
 </theory>
-<theory name="Test_imperial_violet" sum="bcb782e1a7e132b2f42dad1f91362e75" expanded="true">
+<theory name="Test_imperial_violet" sum="cb6416d5f85dca726fc4b756e7e46b0c" expanded="true">
 <goal name="bv32_bounds_bv" expanded="true">
 <proof prover="0"><result status="valid" time="0.13" steps="144"/></proof>
 <proof prover="1"><result status="valid" time="0.25"/></proof>
@@ -199,9 +199,9 @@
 <proof prover="1"><result status="valid" time="0.95"/></proof>
 </goal>
 </theory>
-<theory name="Test_from_bitvector_example" sum="22d1d76b63ec655dcadb3387aad2a5b3" expanded="true">
+<theory name="Test_from_bitvector_example" sum="5500775d7c19e733a69515bfb7464569" expanded="true">
 <goal name="Test1" expanded="true">
- <proof prover="0"><result status="valid" time="0.14" steps="96"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="98"/></proof>
 <proof prover="1"><result status="valid" time="0.22"/></proof>
 <proof prover="2"><result status="valid" time="0.03"/></proof>
 <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -213,7 +213,7 @@
 <proof prover="3"><result status="valid" time="0.01"/></proof>
 </goal>
 <goal name="Test3" expanded="true">
- <proof prover="0"><result status="valid" time="0.06" steps="85"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="88"/></proof>
 <proof prover="1"><result status="valid" time="0.19"/></proof>
 <proof prover="2"><result status="valid" time="0.03"/></proof>
 <proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -231,13 +231,13 @@
 <proof prover="3"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="Test6" expanded="true">
- <proof prover="0"><result status="valid" time="0.06" steps="129"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="133"/></proof>
 <proof prover="1"><result status="valid" time="0.32"/></proof>
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 <proof prover="3"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="WP_parameter lsr31" expl="VC for lsr31" expanded="true">
- <proof prover="1"><result status="valid" time="0.58"/></proof>
+ <proof prover="1"><result status="valid" time="0.37"/></proof>
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 <proof prover="3"><result status="valid" time="0.00"/></proof>
 </goal>
@@ -389,7 +389,7 @@
 </goal>
 <goal name="to_int_0x0003FFFF" expanded="true">
 <proof prover="0"><result status="valid" time="0.13" steps="172"/></proof>
- <proof prover="1"><result status="valid" time="0.56"/></proof>
+ <proof prover="1"><result status="valid" time="0.40"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 <proof prover="3"><result status="valid" time="0.01"/></proof>
 </goal>

--- a/examples/bitvector_examples/why3shapes.gz
+++ b/examples/bitvector_examples/why3shapes.gz
--- a/examples/hackers-delight/why3session.xml
+++ b/examples/hackers-delight/why3session.xml
@@ -7,60 +7,60 @@
 <prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
 <file name="../hackers-delight.mlw" expanded="true">
-<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
+<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Utils_Spec" sum="847a297558090f626aad0b2d693c227e" expanded="true">
- <goal name="countZero" expanded="true">
+<theory name="Utils_Spec" sum="610234791a002b9c10f7c59264163ffb" expanded="true">
+ <goal name="countZero">
 <proof prover="1"><result status="valid" time="0.03"/></proof>
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="numOfZero" expanded="true">
- <proof prover="0"><result status="valid" time="0.47" steps="228"/></proof>
+ <goal name="numOfZero">
+ <proof prover="0"><result status="valid" time="0.47" steps="236"/></proof>
 <proof prover="3"><result status="valid" time="0.33"/></proof>
 </goal>
- <goal name="countStep" expanded="true">
+ <goal name="countStep">
 <proof prover="1" timelimit="30"><result status="valid" time="4.95"/></proof>
 </goal>
- <goal name="WP_parameter numof_shift" expl="VC for numof_shift" expanded="true">
+ <goal name="WP_parameter numof_shift" expl="VC for numof_shift">
 <proof prover="1"><result status="valid" time="0.24"/></proof>
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 <proof prover="3"><result status="valid" time="0.14"/></proof>
 </goal>
- <goal name="WP_parameter countSpec_Aux" expl="VC for countSpec_Aux" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <goal name="WP_parameter countSpec_Aux.1" expl="1. postcondition" expanded="true">
+ <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.47" steps="265"/></proof>
  <proof prover="1"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.28"/></proof>
  </goal>
-  <goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease" expanded="true">
+  <goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease">
  <proof prover="1"><result status="valid" time="0.02"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.41"/></proof>
  </goal>
-  <goal name="WP_parameter countSpec_Aux.3" expl="3. assertion" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
-   <goal name="WP_parameter countSpec_Aux.3.1" expl="1. assertion" expanded="true">
+  <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="3"><result status="valid" time="0.84"/></proof>
   </goal>
-   <goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion" expanded="true">
+   <goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion">
   <proof prover="3"><result status="valid" time="0.27"/></proof>
   </goal>
-   <goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion" expanded="true">
+   <goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion">
   <proof prover="0"><result status="valid" time="0.51" steps="158"/></proof>
   </goal>
-   <goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion" expanded="true">
+   <goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion">
   <proof prover="3" timelimit="15"><result status="valid" time="3.83"/></proof>
   </goal>
  </transf>
  </goal>
-  <goal name="WP_parameter countSpec_Aux.4" expl="4. postcondition" expanded="true">
+  <goal name="WP_parameter countSpec_Aux.4" expl="4. postcondition">
  <proof prover="1"><result status="valid" time="0.30"/></proof>
  </goal>
 </transf>
 </goal>
- <goal name="countSpec" expanded="true">
- <proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
+ <goal name="countSpec">
+ <proof prover="0"><result status="valid" time="0.05" steps="74"/></proof>
 <proof prover="1"><result status="valid" time="0.10"/></proof>
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -68,189 +68,189 @@
 <goal name="WP_parameter hamming_spec" expl="VC for hamming_spec" expanded="true">
 <transf name="split_goal_wp" expanded="true">
  <goal name="WP_parameter hamming_spec.1" expl="1. assertion" expanded="true">
-  <proof prover="0"><result status="valid" time="1.47" steps="592"/></proof>
+  <proof prover="0"><result status="valid" time="2.43" steps="838"/></proof>
  <proof prover="3"><result status="valid" time="0.06"/></proof>
  </goal>
-  <goal name="WP_parameter hamming_spec.2" expl="2. postcondition" expanded="true">
+  <goal name="WP_parameter hamming_spec.2" expl="2. postcondition">
  <proof prover="2"><result status="valid" time="0.14"/></proof>
  </goal>
 </transf>
 </goal>
- <goal name="symmetric" expanded="true">
+ <goal name="symmetric">
 <proof prover="1"><result status="valid" time="0.11"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="separation" expanded="true">
+ <goal name="separation">
 <proof prover="1"><result status="valid" time="0.19"/></proof>
 <proof prover="2"><result status="valid" time="0.12"/></proof>
 </goal>
- <goal name="WP_parameter numof_or" expl="VC for numof_or" expanded="true">
+ <goal name="WP_parameter numof_or" expl="VC for numof_or">
 <proof prover="1"><result status="valid" time="0.53"/></proof>
 <proof prover="2"><result status="valid" time="0.06"/></proof>
 <proof prover="3"><result status="valid" time="0.14"/></proof>
 </goal>
- <goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <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="0"><result status="valid" time="0.04" steps="72"/></proof>
+ <goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion">
+  <transf name="split_goal_wp">
+   <goal name="WP_parameter triangleInequalityInt.1.1" expl="1. VC for triangleInequalityInt">
+   <proof prover="0"><result status="valid" time="0.04" steps="74"/></proof>
   <proof prover="1"><result status="valid" time="0.06"/></proof>
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
-   <goal name="WP_parameter triangleInequalityInt.1.2" expl="2. VC for triangleInequalityInt" expanded="true">
-   <proof prover="2"><result status="valid" time="0.17"/></proof>
+   <goal name="WP_parameter triangleInequalityInt.1.2" expl="2. VC for triangleInequalityInt">
+   <proof prover="2"><result status="valid" time="0.47"/></proof>
   </goal>
  </transf>
  </goal>
-  <goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition" expanded="true">
+  <goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
  <proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.09"/></proof>
  </goal>
 </transf>
 </goal>
- <goal name="triangleInequality" expanded="true">
+ <goal name="triangleInequality">
 <proof prover="1" timelimit="15"><result status="valid" time="2.35"/></proof>
 </goal>
 </theory>
-<theory name="Hackers_delight" sum="275dc4d80fc97952f381d86f9f73fc33" expanded="true">
- <goal name="WP_parameter ascii" expl="VC for ascii" expanded="true">
+<theory name="Hackers_delight" sum="e816aa8b35a31288aafa204946296549" expanded="true">
+ <goal name="WP_parameter ascii" expl="VC for ascii">
 <proof prover="1"><result status="valid" time="0.09"/></proof>
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="asciiProp" expanded="true">
- <proof prover="1" timelimit="20"><result status="valid" time="0.85"/></proof>
+ <goal name="asciiProp">
+ <proof prover="1" timelimit="20"><result status="valid" time="0.66"/></proof>
 <proof prover="2" timelimit="20"><result status="valid" time="2.11"/></proof>
 </goal>
- <goal name="iso" expanded="true">
+ <goal name="iso">
 <proof prover="1"><result status="valid" time="0.43"/></proof>
 </goal>
- <goal name="grayIsGray" expanded="true">
+ <goal name="grayIsGray">
 <proof prover="1"><result status="valid" time="0.09"/></proof>
 </goal>
- <goal name="nthGray" expanded="true">
+ <goal name="nthGray">
 <proof prover="1"><result status="valid" time="0.05"/></proof>
 <proof prover="3"><result status="valid" time="1.46"/></proof>
 </goal>
- <goal name="lastNthGray" expanded="true">
+ <goal name="lastNthGray">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="1.02"/></proof>
+ <proof prover="3"><result status="valid" time="1.27"/></proof>
 </goal>
- <goal name="nthBinary" expanded="true">
+ <goal name="nthBinary">
 <proof prover="1" timelimit="30"><result status="valid" time="0.22"/></proof>
 </goal>
- <goal name="evenOdd" expanded="true">
+ <goal name="evenOdd">
 <proof prover="1"><result status="valid" time="0.14"/></proof>
 </goal>
- <goal name="DM1" expanded="true">
+ <goal name="DM1">
 <proof prover="1"><result status="valid" time="0.01"/></proof>
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="DM2" expanded="true">
+ <goal name="DM2">
 <proof prover="1"><result status="valid" time="0.05"/></proof>
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="DM3" expanded="true">
+ <goal name="DM3">
 <proof prover="1"><result status="valid" time="0.07"/></proof>
 <proof prover="2"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="DM4" expanded="true">
+ <goal name="DM4">
 <proof prover="1"><result status="valid" time="0.11"/></proof>
 </goal>
- <goal name="DM5" expanded="true">
+ <goal name="DM5">
 <proof prover="1"><result status="valid" time="0.10"/></proof>
 </goal>
- <goal name="DM6" expanded="true">
+ <goal name="DM6">
 <proof prover="1"><result status="valid" time="0.07"/></proof>
 </goal>
- <goal name="DM7" expanded="true">
+ <goal name="DM7">
 <proof prover="1"><result status="valid" time="0.08"/></proof>
 </goal>
- <goal name="DM8" expanded="true">
+ <goal name="DM8">
 <proof prover="1"><result status="valid" time="0.09"/></proof>
 </goal>
- <goal name="DMtest" expanded="true">
+ <goal name="DMtest">
 <proof prover="1"><result status="valid" time="0.07"/></proof>
 <proof prover="2"><result status="valid" time="0.18"/></proof>
 </goal>
- <goal name="Aa" expanded="true">
+ <goal name="Aa">
 <proof prover="1"><result status="valid" time="0.06"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="Ac" expanded="true">
+ <goal name="Ac">
 <proof prover="1"><result status="valid" time="0.07"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="Ad" expanded="true">
+ <goal name="Ad">
 <proof prover="1"><result status="valid" time="0.06"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="Ae" expanded="true">
- <proof prover="0"><result status="valid" time="0.05" steps="74"/></proof>
+ <goal name="Ae">
+ <proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="3"><result status="valid" time="0.08"/></proof>
 </goal>
- <goal name="Af" expanded="true">
+ <goal name="Af">
 <proof prover="1"><result status="valid" time="0.03"/></proof>
 <proof prover="2"><result status="valid" time="0.09"/></proof>
 </goal>
- <goal name="Aj" expanded="true">
+ <goal name="Aj">
 <proof prover="1"><result status="valid" time="0.02"/></proof>
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="An" expanded="true">
+ <goal name="An">
 <proof prover="1"><result status="valid" time="0.12"/></proof>
 </goal>
- <goal name="Ao" expanded="true">
+ <goal name="Ao">
 <proof prover="1"><result status="valid" time="0.13"/></proof>
 </goal>
- <goal name="Aq" expanded="true">
+ <goal name="Aq">
 <proof prover="1"><result status="valid" time="0.08"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="At" expanded="true">
+ <goal name="At">
 <proof prover="1"><result status="valid" time="0.12"/></proof>
 </goal>
- <goal name="Au" expanded="true">
+ <goal name="Au">
 <proof prover="1"><result status="valid" time="0.13"/></proof>
 </goal>
- <goal name="Av" expanded="true">
+ <goal name="Av">
 <proof prover="1"><result status="valid" time="0.12"/></proof>
 <proof prover="2"><result status="valid" time="0.03"/></proof>
 </goal>
- <goal name="IE1" expanded="true">
+ <goal name="IE1">
 <proof prover="1"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="IE2" expanded="true">
+ <goal name="IE2">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="IEa" expanded="true">
+ <goal name="IEa">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="IEb" expanded="true">
+ <goal name="IEb">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="IE3" expanded="true">
+ <goal name="IE3">
 <proof prover="1"><result status="valid" time="0.03"/></proof>
 </goal>
- <goal name="IE4" expanded="true">
+ <goal name="IE4">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="SR1" expanded="true">
+ <goal name="SR1">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="RS_left" expanded="true">
+ <goal name="RS_left">
 <proof prover="1"><result status="valid" time="0.11"/></proof>
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="RS_right" expanded="true">
+ <goal name="RS_right">
 <proof prover="1"><result status="valid" time="0.09"/></proof>
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="BP" expanded="true">
+ <goal name="BP">
 <proof prover="1"><result status="valid" time="0.10"/></proof>
 </goal>
 </theory>

--- a/examples/hackers-delight/why3shapes.gz
+++ b/examples/hackers-delight/why3shapes.gz
--- a/examples/in_progress/bitwalker_abstract2/why3session.xml
+++ b/examples/in_progress/bitwalker_abstract2/why3session.xml
--- a/examples/in_progress/bitwalker_abstract2/why3shapes.gz
+++ b/examples/in_progress/bitwalker_abstract2/why3shapes.gz
--- a/examples/logic/bitvectors/why3session.xml
+++ b/examples/logic/bitvectors/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../bitvectors.why" expanded="true">
-<theory name="TestBV" sum="963c694e921f3386f04b0405c5dd8d3f" expanded="true">
+<theory name="TestBV" sum="2f88fb831f7ca34916a60c0d40459d0a" expanded="true">
 <goal name="g1">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -69,7 +69,7 @@
 <proof prover="3"><result status="timeout" time="4.99"/></proof>
 </goal>
 <goal name="g4a">
- <proof prover="0"><result status="valid" time="0.28" steps="161"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="161"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 <proof prover="3"><result status="valid" time="0.00"/></proof>
 </goal>

--- a/examples/logic/bitvectors/why3shapes.gz
+++ b/examples/logic/bitvectors/why3shapes.gz
--- a/examples/queens_bv/why3session.xml
+++ b/examples/queens_bv/why3session.xml
@@ -20,17 +20,17 @@
 </theory>
 <theory name="BitsSpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="Bits" sum="2c6dbbc852f8c746d08c2442fe9921e3" expanded="true">
+<theory name="Bits" sum="38f4786c9c18f4fc521a37a17e25dda7" expanded="true">
 <goal name="WP_parameter empty" expl="VC for empty">
 <proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
 <proof prover="1"><result status="valid" time="0.06"/></proof>
 </goal>
 <goal name="WP_parameter is_empty" expl="VC for is_empty">
- <proof prover="0"><result status="valid" time="0.11" steps="102"/></proof>
+ <proof prover="0"><result status="valid" time="0.11" steps="107"/></proof>
 <proof prover="1"><result status="valid" time="0.30"/></proof>
 </goal>
 <goal name="WP_parameter remove_singleton" expl="VC for remove_singleton">
- <proof prover="0"><result status="valid" time="0.62" steps="544"/></proof>
+ <proof prover="0"><result status="valid" time="0.62" steps="583"/></proof>
 <proof prover="1"><result status="valid" time="2.15"/></proof>
 </goal>
 <goal name="WP_parameter add_singleton" expl="VC for add_singleton">
@@ -41,7 +41,7 @@
  <goal name="WP_parameter mul2.1" expl="1. type invariant">
  <transf name="split_goal_wp">
   <goal name="WP_parameter mul2.1.1" expl="1. type invariant">
-   <proof prover="0"><result status="valid" time="2.82" steps="908"/></proof>
+   <proof prover="0"><result status="valid" time="2.82" steps="915"/></proof>
   </goal>
   <goal name="WP_parameter mul2.1.2" expl="2. type invariant">
   <proof prover="0"><result status="valid" time="0.05" steps="83"/></proof>
@@ -63,10 +63,10 @@
 </transf>
 </goal>
 <goal name="WP_parameter div2" expl="VC for div2">
- <proof prover="0"><result status="valid" time="0.13" steps="136"/></proof>
+ <proof prover="0"><result status="valid" time="0.13" steps="134"/></proof>
 </goal>
 <goal name="WP_parameter diff" expl="VC for diff">
- <proof prover="0"><result status="valid" time="0.24" steps="220"/></proof>
+ <proof prover="0"><result status="valid" time="0.24" steps="223"/></proof>
 <proof prover="1"><result status="valid" time="0.66"/></proof>
 </goal>
 <goal name="bits_interval_is_zero_equ">
@@ -76,38 +76,38 @@
 <goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick">
 <transf name="split_goal_wp">
  <goal name="WP_parameter rightmost_bit_trick.1" expl="1. assertion">
-  <proof prover="1"><result status="valid" time="2.98"/></proof>
+  <proof prover="1"><result status="valid" time="1.73"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick.2" expl="2. assertion">
-  <proof prover="0"><result status="valid" time="0.07" steps="118"/></proof>
+  <proof prover="0"><result status="valid" time="0.07" steps="120"/></proof>
  <proof prover="1"><result status="valid" time="0.22"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick.3" expl="3. assertion">
  <proof prover="3"><result status="valid" time="0.08"/></proof>
-  <proof prover="4"><result status="valid" time="0.07"/></proof>
+  <proof prover="4"><result status="valid" time="0.23"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick.4" expl="4. assertion">
-  <proof prover="0"><result status="valid" time="0.26" steps="148"/></proof>
+  <proof prover="0"><result status="valid" time="0.13" steps="133"/></proof>
  <proof prover="1"><result status="valid" time="0.78"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick.5" expl="5. assertion">
  <proof prover="3"><result status="valid" time="0.13"/></proof>
-  <proof prover="4"><result status="valid" time="0.11"/></proof>
+  <proof prover="4"><result status="valid" time="0.25"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick.6" expl="6. assertion">
-  <proof prover="1"><result status="valid" time="1.83"/></proof>
+  <proof prover="1"><result status="valid" time="4.29"/></proof>
  <proof prover="3"><result status="valid" time="0.14"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick.7" expl="7. type invariant">
  <transf name="split_goal_wp">
   <goal name="WP_parameter rightmost_bit_trick.7.1" expl="1. type invariant">
-   <proof prover="0"><result status="valid" time="0.15" steps="116"/></proof>
+   <proof prover="0"><result status="valid" time="0.15" steps="118"/></proof>
   <proof prover="1"><result status="valid" time="0.07"/></proof>
   <proof prover="3"><result status="valid" time="0.13"/></proof>
   <proof prover="4"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter rightmost_bit_trick.7.2" expl="2. type invariant">
-   <proof prover="0"><result status="valid" time="0.14" steps="208"/></proof>
+   <proof prover="0"><result status="valid" time="0.14" steps="212"/></proof>
   <proof prover="1"><result status="valid" time="0.24"/></proof>
   <proof prover="3"><result status="valid" time="0.12"/></proof>
   <proof prover="4"><result status="valid" time="0.05"/></proof>
@@ -132,13 +132,14 @@
 </transf>
 </goal>
 <goal name="WP_parameter below" expl="VC for below">
- <proof prover="0"><result status="valid" time="8.24" steps="827"/></proof>
+ <proof prover="0"><result status="valid" time="5.26" steps="869"/></proof>
+ <proof prover="1"><result status="valid" time="1.14"/></proof>
 </goal>
 </theory>
-<theory name="NQueensBits" sum="c9cb2c3e4e06c5345f09b19c801a7da1" expanded="true">
- <goal name="WP_parameter t" expl="VC for t">
- <transf name="split_goal_wp">
-  <goal name="WP_parameter t.1" expl="1. assertion">
+<theory name="NQueensBits" sum="a118c39f5de341751db6886f305251a0" expanded="true">
+ <goal name="WP_parameter t" expl="VC for t" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="WP_parameter t.1" expl="1. assertion" expanded="true">
  <proof prover="0" timelimit="30"><result status="valid" time="16.39" steps="2856"/></proof>
  </goal>
  <goal name="WP_parameter t.2" expl="2. loop invariant init">
@@ -391,7 +392,7 @@
   <proof prover="3" timelimit="30"><result status="valid" time="0.30"/></proof>
   </goal>
   <goal name="WP_parameter t.48.4" expl="4. loop invariant preservation">
-   <proof prover="1" timelimit="30"><result status="valid" time="3.20"/></proof>
+   <proof prover="1" timelimit="30"><result status="valid" time="2.14"/></proof>
   <proof prover="3" timelimit="30"><result status="valid" time="0.69"/></proof>
   </goal>
  </transf>
@@ -403,7 +404,7 @@
   </goal>
   <goal name="WP_parameter t.49.2" expl="2. loop invariant preservation">
   <proof prover="0" timelimit="30"><result status="valid" time="2.21"