diff --git a/drivers/cvc4_bv.gen b/drivers/cvc4_bv.gen
index 4d4f8618384c4509908ff724910862d7fc50cc16..b28a7bdd8845ff237f1d24eebd6f6465d8ca37c3 100644
--- a/drivers/cvc4_bv.gen
+++ b/drivers/cvc4_bv.gen
@@ -4,67 +4,19 @@
 theory bv.BV64
   syntax converter of_int "(_ bv%1 64)"
   syntax function to_uint "(bv2nat %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
 
 theory bv.BV32
   syntax converter of_int "(_ bv%1 32)"
   syntax function to_uint "(bv2nat %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
 
 theory bv.BV16
   syntax converter of_int "(_ bv%1 16)"
   syntax function to_uint "(bv2nat %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
 
 theory bv.BV8
   syntax converter of_int "(_ bv%1 8)"
   syntax function to_uint "(bv2nat %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
diff --git a/drivers/smt-libv2-bv.gen b/drivers/smt-libv2-bv.gen
index 25fef83856b39e64c52cb13374ac0b1b98ed95a0..a30aee0e510a6996201c4c71e4de45cad9a1667e 100644
--- a/drivers/smt-libv2-bv.gen
+++ b/drivers/smt-libv2-bv.gen
@@ -20,26 +20,7 @@ theory bv.BV_Gen
   syntax function asr_bv "(bvashr %1 %2)"
   syntax predicate eq "(= %1 %2)"
 
-  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 Extensionality
-  remove prop Nth_bw_or
-  remove prop Nth_bw_and
-  remove prop Nth_bw_xor
-  remove prop Nth_bw_not
-  remove prop Nth_rotate_left
-  remove prop Nth_rotate_right
-  remove prop Nth_bv_is_nth
-  remove prop Lsr_nth_low
-  remove prop Lsr_nth_high
-  remove prop Asr_nth_low
-  remove prop Asr_nth_high
-  remove prop Lsl_nth_low
-  remove prop Lsl_nth_high
+  remove allprops
 
   syntax predicate ult "(bvult %1 %2)"
   syntax predicate ule "(bvule %1 %2)"
@@ -107,8 +88,7 @@ theory bv.BV8
 end
 
 theory bv.BVConverter_Gen
-  remove prop toSmall_to_uint
-  remove prop toBig_to_uint
+   remove allprops
 end
 
 theory bv.BVConverter_32_64
@@ -142,75 +122,5 @@ theory bv.BVConverter_8_16
 end
 
 theory bv.Pow2int
-
-  remove prop Power_0
-  remove prop Power_s
-  remove prop Power_1
-  remove prop Power_sum
-  remove prop pow2pos
-  remove prop pow2_0
-  remove prop pow2_1
-  remove prop pow2_2
-  remove prop pow2_3
-  remove prop pow2_4
-  remove prop pow2_5
-  remove prop pow2_6
-  remove prop pow2_7
-  remove prop pow2_8
-  remove prop pow2_9
-  remove prop pow2_10
-  remove prop pow2_11
-  remove prop pow2_12
-  remove prop pow2_13
-  remove prop pow2_14
-  remove prop pow2_15
-  remove prop pow2_16
-  remove prop pow2_17
-  remove prop pow2_18
-  remove prop pow2_19
-  remove prop pow2_20
-  remove prop pow2_21
-  remove prop pow2_22
-  remove prop pow2_23
-  remove prop pow2_24
-  remove prop pow2_25
-  remove prop pow2_26
-  remove prop pow2_27
-  remove prop pow2_28
-  remove prop pow2_29
-  remove prop pow2_30
-  remove prop pow2_31
-  remove prop pow2_32
-  remove prop pow2_33
-  remove prop pow2_34
-  remove prop pow2_35
-  remove prop pow2_36
-  remove prop pow2_37
-  remove prop pow2_38
-  remove prop pow2_39
-  remove prop pow2_40
-  remove prop pow2_41
-  remove prop pow2_42
-  remove prop pow2_43
-  remove prop pow2_44
-  remove prop pow2_45
-  remove prop pow2_46
-  remove prop pow2_47
-  remove prop pow2_48
-  remove prop pow2_49
-  remove prop pow2_50
-  remove prop pow2_51
-  remove prop pow2_52
-  remove prop pow2_53
-  remove prop pow2_54
-  remove prop pow2_55
-  remove prop pow2_56
-  remove prop pow2_57
-  remove prop pow2_58
-  remove prop pow2_59
-  remove prop pow2_60
-  remove prop pow2_61
-  remove prop pow2_62
-  remove prop pow2_63
-  remove prop pow2_64
+  remove allprops
 end
diff --git a/drivers/z3_432.drv b/drivers/z3_432.drv
index c559aa5360a1f0625ab5f702f2cf806cc770eedd..2e88431d00950e5686fc55cc5fe58697a8bf1be6 100644
--- a/drivers/z3_432.drv
+++ b/drivers/z3_432.drv
@@ -28,7 +28,7 @@ transformation "eliminate_epsilon"
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
 
-(* Prepare for counter-example query: get rid of some quantifiers (makes it 
+(* Prepare for counter-example query: get rid of some quantifiers (makes it
 possible to query model values of the variables in premises) and introduce
 counter-example projections  *)
 transformation "prepare_for_counterexmp"
@@ -82,67 +82,19 @@ end
 theory bv.BV64
   syntax converter of_int "((_ int2bv 64) %1)"
   syntax function to_uint "(bv2int %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
 
 theory bv.BV32
   syntax converter of_int "((_ int2bv 32) %1)"
   syntax function to_uint "(bv2int %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
 
 theory bv.BV16
   syntax converter of_int "((_ int2bv 16) %1)"
   syntax function to_uint "(bv2int %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
 
 theory bv.BV8
   syntax converter of_int "((_ int2bv 8) %1)"
   syntax function to_uint "(bv2int %1)"
-  remove prop to_uint_of_int
-  remove prop to_uint_extensionality
-  remove prop to_uint_bounds
-
-  remove prop to_uint_add
-  remove prop to_uint_sub
-  remove prop to_uint_neg
-  remove prop to_uint_mul
-  remove prop to_uint_udiv
-  remove prop to_uint_urem
-  remove prop to_uint_lsr
-  remove prop to_uint_lsl
 end
diff --git a/examples/bitcount/why3session.xml b/examples/bitcount/why3session.xml
index 266d41b5ea1273a68db2928d8dfe0eda177b5cf1..217bda969df9bf4ff3967f9d0f1db2fcd44ebdad 100644
--- a/examples/bitcount/why3session.xml
+++ b/examples/bitcount/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="../bitcount.mlw" expanded="true">
-<theory name="BitCount8bit_fact" sum="0a9542b8845049b148e46227080d891f">
+<theory name="BitCount8bit_fact" sum="c75ce9e432c578193a79df3868b92c50">
  <goal name="nth_as_bv_is_int">
  <proof prover="0" timelimit="25" memlimit="1000"><result status="valid" time="0.32" steps="118"/></proof>
  <proof prover="1" timelimit="25"><result status="valid" time="0.33"/></proof>
@@ -86,7 +86,7 @@
    <proof prover="2"><result status="valid" time="0.07"/></proof>
    </goal>
    <goal name="WP_parameter step2.5.5" expl="5. assertion">
-   <proof prover="1" timelimit="25"><result status="valid" time="15.65"/></proof>
+   <proof prover="1" timelimit="25"><result status="valid" time="17.54"/></proof>
    </goal>
   </transf>
   </goal>
@@ -177,7 +177,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="BitCount32bit_fact" sum="7fdd50eb80427905b5fb8d3c73c0432e">
+<theory name="BitCount32bit_fact" sum="7fe1723c3933d65064c895efddfb876f" expanded="true">
  <goal name="WP_parameter step1" expl="VC for step1">
  <transf name="split_goal_wp">
   <goal name="WP_parameter step1.1" expl="1. assertion">
@@ -262,7 +262,7 @@
    <proof prover="3" timelimit="20"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="WP_parameter step2.5.5" expl="5. assertion">
-   <proof prover="1" timelimit="20"><result status="valid" time="5.22"/></proof>
+   <proof prover="1" timelimit="20"><result status="valid" time="5.92"/></proof>
    </goal>
   </transf>
   </goal>
@@ -357,7 +357,6 @@
    <goal name="WP_parameter step3.7.6" expl="6. assertion">
    <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.03" steps="90"/></proof>
    <proof prover="1" timelimit="20"><result status="valid" time="0.02"/></proof>
-   <proof prover="3" timelimit="20"><result status="valid" time="2.57"/></proof>
    </goal>
    <goal name="WP_parameter step3.7.7" expl="7. assertion">
    <proof prover="1" timelimit="20"><result status="valid" time="0.23"/></proof>
@@ -368,7 +367,7 @@
   </transf>
   </goal>
   <goal name="WP_parameter step3.8" expl="8. postcondition">
-  <proof prover="2" timelimit="20"><result status="valid" time="0.20"/></proof>
+  <proof prover="2" timelimit="20"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="WP_parameter step3.9" expl="9. postcondition">
   <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.46" steps="171"/></proof>
@@ -377,8 +376,8 @@
   </goal>
  </transf>
  </goal>
- <goal name="WP_parameter step4" expl="VC for step4">
- <transf name="split_goal_wp">
+ <goal name="WP_parameter step4" expl="VC for step4" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter step4.1" expl="1. precondition">
   <transf name="split_goal_wp">
    <goal name="WP_parameter step4.1.1" expl="1. VC for step4">
@@ -401,7 +400,7 @@
   <proof prover="2" timelimit="20"><result status="valid" time="0.05"/></proof>
   <proof prover="3" timelimit="20"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="WP_parameter step4.3" expl="3. precondition">
+  <goal name="WP_parameter step4.3" expl="3. precondition" expanded="true">
   <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.04" steps="75"/></proof>
   <proof prover="1" timelimit="20"><result status="valid" time="0.04"/></proof>
   <proof prover="2" timelimit="20"><result status="valid" time="0.03"/></proof>
@@ -447,8 +446,8 @@
   <proof prover="2" timelimit="20"><result status="valid" time="0.03"/></proof>
   <proof prover="3" timelimit="20"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="WP_parameter step4.9" expl="9. assertion">
-  <transf name="split_goal_wp">
+  <goal name="WP_parameter step4.9" expl="9. assertion" expanded="true">
+  <transf name="split_goal_wp" expanded="true">
    <goal name="WP_parameter step4.9.1" expl="1. assertion">
    <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.11" steps="143"/></proof>
    <proof prover="1" timelimit="20"><result status="valid" time="0.37"/></proof>
@@ -460,19 +459,17 @@
    <proof prover="1" timelimit="20"><result status="valid" time="2.90"/></proof>
    <proof prover="2" timelimit="20"><result status="valid" time="0.13"/></proof>
    </goal>
-   <goal name="WP_parameter step4.9.4" expl="4. assertion">
+   <goal name="WP_parameter step4.9.4" expl="4. assertion" expanded="true">
    <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.06" steps="90"/></proof>
    <proof prover="1" timelimit="20"><result status="valid" time="0.05"/></proof>
-   <proof prover="3" timelimit="20"><result status="valid" time="5.05"/></proof>
    </goal>
    <goal name="WP_parameter step4.9.5" expl="5. assertion">
    <proof prover="2" timelimit="20"><result status="valid" time="0.08"/></proof>
    <proof prover="3" timelimit="20"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter step4.9.6" expl="6. assertion">
+   <goal name="WP_parameter step4.9.6" expl="6. assertion" expanded="true">
    <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.05" steps="91"/></proof>
    <proof prover="1" timelimit="20"><result status="valid" time="0.06"/></proof>
-   <proof prover="3" timelimit="20"><result status="valid" time="1.55"/></proof>
    </goal>
    <goal name="WP_parameter step4.9.7" expl="7. assertion">
    <proof prover="1" timelimit="20"><result status="valid" time="0.51"/></proof>
@@ -610,7 +607,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="Hamming" sum="d2e0fa2839f0ea7f837e2de931961eca" expanded="true">
+<theory name="Hamming" sum="f58ac4e32def3758c49cf4ca64ad01d8">
  <goal name="WP_parameter hammingD" expl="VC for hammingD">
  <transf name="split_goal_wp">
   <goal name="WP_parameter hammingD.1" expl="1. assertion">
@@ -622,7 +619,7 @@
  </transf>
  </goal>
  <goal name="symmetric">
- <proof prover="1" timelimit="20"><result status="valid" time="6.96"/></proof>
+ <proof prover="1" timelimit="20"><result status="valid" time="7.86"/></proof>
  <proof prover="3" timelimit="20"><result status="valid" time="0.10"/></proof>
  </goal>
  <goal name="numof_ytpmE">
@@ -657,7 +654,7 @@
  <proof prover="2" timelimit="20"><result status="valid" time="0.04"/></proof>
  </goal>
 </theory>
-<theory name="AsciiCode" sum="2355b20157d5f66a9c56cab2c9c206e8" expanded="true">
+<theory name="AsciiCode" sum="0f11e672ebddf479fb932b64c9e6c843" 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">
@@ -778,7 +775,7 @@
   <proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
   </goal>
   <goal name="WP_parameter tmp.3" expl="3. postcondition" expanded="true">
-  <proof prover="2" timelimit="30"><result status="valid" time="18.28"/></proof>
+  <proof prover="2" timelimit="30"><result status="valid" time="23.99"/></proof>
   </goal>
   <goal name="WP_parameter tmp.4" expl="4. postcondition" expanded="true">
   <proof prover="0"><result status="valid" time="1.44" steps="572"/></proof>
@@ -789,7 +786,7 @@
  <proof prover="0" memlimit="1000"><result status="valid" time="0.27" steps="240"/></proof>
  </goal>
 </theory>
-<theory name="GrayCode" sum="84dd0ed6aa73f35416328e1c3f203705" expanded="true">
+<theory name="GrayCode" sum="08e01c52536014ef570bfe551bad657b" expanded="true">
  <goal name="iso" expanded="true">
  </goal>
  <goal name="WP_parameter grayIsGray" expl="VC for grayIsGray" expanded="true">
diff --git a/examples/bitcount/why3shapes.gz b/examples/bitcount/why3shapes.gz
index 83faffaf65523fa520f9233dc6b012abca1e2e06..d7b0cbee8443fd468d91384eb18cdf2ae5920ccf 100644
Binary files a/examples/bitcount/why3shapes.gz and b/examples/bitcount/why3shapes.gz differ
diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml
index 858ec7e0f3cfb03caaf7bcd901089589b6668349..3ae4595f14558c37acefea2ea5bdd34a09a69079 100644
--- 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="6fb94f39a17f6d336d37a4eb24fc9921" expanded="true">
+<theory name="Test_proofinuse" sum="bd0fd6bbcea5b5adc03536c5e643efb1" 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">
@@ -103,7 +103,7 @@
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
 </theory>
-<theory name="Hackers_delight_mod" sum="df93f6196fe77d1d941fdbcbcaace732" expanded="true">
+<theory name="Hackers_delight_mod" sum="a496501341c99e842ff5afc76bf4e611" 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="0916a7dc63483a6d85503c2aea8ed311" expanded="true">
+<theory name="Test_imperial_violet" sum="02f8456e7087c14a7dce80467987dec3" 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,7 +199,7 @@
  <proof prover="1"><result status="valid" time="0.95"/></proof>
  </goal>
 </theory>
-<theory name="Test_from_bitvector_example" sum="69d7af24e60703d28350a145d0e363f9" expanded="true">
+<theory name="Test_from_bitvector_example" sum="10570a298afc58c4a36facbd4f2facd5" expanded="true">
  <goal name="Test1" expanded="true">
  <proof prover="0"><result status="valid" time="0.14" steps="101"/></proof>
  <proof prover="1"><result status="valid" time="0.22"/></proof>
@@ -247,7 +247,7 @@
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="WP_parameter lsr29" expl="VC for lsr29" expanded="true">
- <proof prover="1"><result status="valid" time="0.52"/></proof>
+ <proof prover="1"><result status="valid" time="0.36"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz
index 9b3c46d15aa413c0ae14ccaa2c5222b58c3db809..055bbb4cb2554e450de89e69804015d87336152b 100644
Binary files a/examples/bitvector_examples/why3shapes.gz and b/examples/bitvector_examples/why3shapes.gz differ
diff --git a/examples/bitwalker/why3session.xml b/examples/bitwalker/why3session.xml
index 980209c8673b336cdee16ce73b698967f12bb233..caada37af8f4147455527826377b081b246fbadd 100644
--- a/examples/bitwalker/why3session.xml
+++ b/examples/bitwalker/why3session.xml
@@ -8,7 +8,7 @@
 <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"/>
 <file name="../bitwalker.mlw" expanded="true">
-<theory name="Bitwalker" sum="04c17077c9393556d197378eef4ec2fc" expanded="true">
+<theory name="Bitwalker" sum="d4430f5ae75e998e1d531d208d35f01e" expanded="true">
  <goal name="nth64">
  <proof prover="0"><result status="valid" time="0.10" steps="135"/></proof>
  <proof prover="3"><result status="valid" time="0.46"/></proof>
@@ -5820,7 +5820,7 @@
   <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter poke_64bit_bv.5" expl="5. VC for poke_64bit_bv">
-  <proof prover="1"><result status="valid" time="0.20"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter poke_64bit_bv.6" expl="6. VC for poke_64bit_bv">
@@ -5828,7 +5828,7 @@
   <proof prover="2"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="WP_parameter poke_64bit_bv.7" expl="7. VC for poke_64bit_bv">
-  <proof prover="1"><result status="valid" time="0.20"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter poke_64bit_bv.8" expl="8. VC for poke_64bit_bv">
@@ -6272,7 +6272,7 @@
    </goal>
    <goal name="WP_parameter poke.22.3" expl="3. assertion">
    <proof prover="0"><result status="valid" time="0.13" steps="102"/></proof>
-   <proof prover="1"><result status="valid" time="0.23"/></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.12"/></proof>
    </goal>
@@ -6304,7 +6304,7 @@
   </goal>
   <goal name="WP_parameter poke.27" expl="27. loop invariant preservation">
   <proof prover="0"><result status="valid" time="1.20" steps="128"/></proof>
-  <proof prover="2"><result status="valid" time="0.25"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="WP_parameter poke.28" expl="28. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.42" steps="122"/></proof>
diff --git a/examples/bitwalker/why3shapes.gz b/examples/bitwalker/why3shapes.gz
index af9c6fb59608d99586e57fee6997e510a92ecf52..fad0fcd7395d1b72bac314121d03e90a60c992e4 100644
Binary files a/examples/bitwalker/why3shapes.gz and b/examples/bitwalker/why3shapes.gz differ
diff --git a/examples/hackers-delight/why3session.xml b/examples/hackers-delight/why3session.xml
index 4e08b2a18e0b3a20c527936b7800fe1b7e9d23aa..9590089e1c5600367c3018d97f24449b03883e7e 100644
--- a/examples/hackers-delight/why3session.xml
+++ b/examples/hackers-delight/why3session.xml
@@ -10,14 +10,14 @@
 <file name="../hackers-delight.mlw" expanded="true">
 <theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Utils_Spec" sum="3f0ae9505cd1d20116a2836d82f8ab3d" expanded="true">
+<theory name="Utils_Spec" sum="48173d335d17e665b5bf6ed0b7333c02" 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">
  <proof prover="0"><result status="valid" time="0.47" steps="239"/></proof>
- <proof prover="3"><result status="valid" time="0.33"/></proof>
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
  </goal>
  <goal name="countStep">
  <proof prover="1" timelimit="30"><result status="valid" time="4.95"/></proof>
@@ -30,14 +30,14 @@
  <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="0"><result status="valid" time="0.03" steps="86"/></proof>
   <proof prover="1"><result status="valid" time="0.04"/></proof>
-  <proof prover="3"><result status="valid" time="0.28"/></proof>
+  <proof prover="3"><result status="valid" time="0.07"/></proof>
   </goal>
   <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>
+  <proof prover="3"><result status="valid" time="0.66"/></proof>
   </goal>
   <goal name="WP_parameter countSpec_Aux.3" expl="3. assertion">
   <transf name="split_goal_wp">
@@ -69,7 +69,7 @@
  <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="2.43" steps="944"/></proof>
+  <proof prover="0"><result status="valid" time="2.43" steps="956"/></proof>
   <proof prover="3"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="WP_parameter hamming_spec.2" expl="2. postcondition">
@@ -83,7 +83,7 @@
  </goal>
  <goal name="separation">
  <proof prover="1"><result status="valid" time="0.19"/></proof>
- <proof prover="2"><result status="valid" time="0.52"/></proof>
+ <proof prover="2"><result status="valid" time="0.10"/></proof>
  </goal>
  <goal name="WP_parameter numof_or" expl="VC for numof_or">
  <proof prover="1"><result status="valid" time="0.53"/></proof>
@@ -93,8 +93,8 @@
  <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">
-  <proof prover="2" timelimit="70"><result status="valid" time="0.77"/></proof>
-  <proof prover="4"><result status="valid" time="0.75"/></proof>
+  <proof prover="2" timelimit="70"><result status="valid" time="1.34"/></proof>
+  <proof prover="4"><result status="valid" time="1.31"/></proof>
   </goal>
   <goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition" expanded="true">
   <proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
@@ -107,14 +107,14 @@
  <proof prover="1" timelimit="15"><result status="valid" time="2.35"/></proof>
  </goal>
 </theory>
-<theory name="Hackers_delight" sum="c1471f5279d8e24b7242c18b19325bf4" expanded="true">
+<theory name="Hackers_delight" sum="144a5949c45c6cffa10ffc47afc51177" 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">
  <proof prover="1" timelimit="20"><result status="valid" time="0.66"/></proof>
- <proof prover="2" timelimit="20"><result status="valid" time="2.72"/></proof>
+ <proof prover="2" timelimit="20"><result status="valid" time="1.69"/></proof>
  </goal>
  <goal name="iso">
  <proof prover="1"><result status="valid" time="0.43"/></proof>
diff --git a/examples/hackers-delight/why3shapes.gz b/examples/hackers-delight/why3shapes.gz
index 427ca350c5ead4e165bfe9a0f1ae2e03b232e7dd..d72288e9a505e1b3eb27c71aab8f457a257b3898 100644
Binary files a/examples/hackers-delight/why3shapes.gz and b/examples/hackers-delight/why3shapes.gz differ
diff --git a/examples/queens_bv/why3session.xml b/examples/queens_bv/why3session.xml
index f9ab1d7ee4deccd5460f998d4aed8a075466c837..b0538ea97279c742dcb041cf8d3b4dfdb7d7f7ea 100644
--- a/examples/queens_bv/why3session.xml
+++ b/examples/queens_bv/why3session.xml
@@ -20,7 +20,7 @@
 </theory>
 <theory name="BitsSpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="Bits" sum="89d1f7f114f012f8e0dea70cfcddc67e">
+<theory name="Bits" sum="6cd5db16655631752af29773c65bc6c2">
  <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>
@@ -31,7 +31,7 @@
  </goal>
  <goal name="WP_parameter remove_singleton" expl="VC for remove_singleton">
  <proof prover="0"><result status="valid" time="0.90" steps="668"/></proof>
- <proof prover="1"><result status="valid" time="1.73"/></proof>
+ <proof prover="1"><result status="valid" time="2.29"/></proof>
  </goal>
  <goal name="WP_parameter add_singleton" expl="VC for add_singleton">
  <proof prover="1"><result status="valid" time="1.17"/></proof>
@@ -127,7 +127,7 @@
  <proof prover="1"><result status="valid" time="1.52"/></proof>
  </goal>
 </theory>
-<theory name="NQueensBits" sum="3a6aea3add6d6b05881981ce9401f001" expanded="true">
+<theory name="NQueensBits" sum="cfb4c367c0c6e2b8f7d6a8cce009c9e4" 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">
@@ -2192,7 +2192,7 @@
   </goal>
   <goal name="WP_parameter t.19" expl="19. assertion">
   <proof prover="0"><result status="valid" time="0.25" steps="156"/></proof>
-  <proof prover="1"><result status="valid" time="1.29"/></proof>
+  <proof prover="1"><result status="valid" time="0.87"/></proof>
   <proof prover="3"><result status="valid" time="0.11"/></proof>
   <proof prover="4"><result status="valid" time="0.04"/></proof>
   </goal>
@@ -2208,7 +2208,7 @@
   <goal name="WP_parameter t.22" expl="22. assertion">
   <transf name="split_goal_wp">
    <goal name="WP_parameter t.22.1" expl="1. assertion">
-   <proof prover="1" timelimit="30"><result status="valid" time="4.35"/></proof>
+   <proof prover="1" timelimit="30"><result status="valid" time="5.89"/></proof>
    <proof prover="3" timelimit="30"><result status="valid" time="0.31"/></proof>
    <proof prover="4" timelimit="30"><result status="valid" time="0.87"/></proof>
    </goal>
@@ -2334,7 +2334,7 @@
   <proof prover="4"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="WP_parameter t.45" expl="45. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="1.22"/></proof>
+  <proof prover="1"><result status="valid" time="0.97"/></proof>
   <proof prover="3"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="WP_parameter t.46" expl="46. loop invariant preservation">
diff --git a/examples/queens_bv/why3shapes.gz b/examples/queens_bv/why3shapes.gz
index 60a5277484e794e1d9a87eef34ea483df8aea5e2..85751ab158e7e3a8ed6b0af2cdca2da22be587e6 100644
Binary files a/examples/queens_bv/why3shapes.gz and b/examples/queens_bv/why3shapes.gz differ
diff --git a/src/driver/driver.ml b/src/driver/driver.ml
index f7c1a3b2aacb5045326c91b3266ab3ed278235b9..ff472a7e7e06224c47df994c0631ae3a495953d5 100644
--- a/src/driver/driver.ml
+++ b/src/driver/driver.ml
@@ -154,6 +154,12 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | Rremovepr (q) ->
         let td = remove_prop (find_pr th q) in
         add_meta th td meta
+    | Rremoveall ->
+      let it key _ = match (Mid.find key th.th_known).d_node with
+        | Dprop (_,symb,_) -> add_meta th (remove_prop symb) meta
+        | _ -> ()
+      in
+      Mid.iter it th.th_local
     | Rconverter (q,s,b) ->
         let cs = syntax_converter (find_ls th q) s b in
         add_meta th cs meta
diff --git a/src/driver/driver_ast.ml b/src/driver/driver_ast.ml
index dc3c2fe31011e8354302e4ca6bae1658e37afc87..a02e2e333fb560fcc18390ddc8d2aca85e9d3a06 100644
--- a/src/driver/driver_ast.ml
+++ b/src/driver/driver_ast.ml
@@ -33,6 +33,7 @@ type th_rule =
   | Rsyntaxps  of qualid * string * bool
   | Rconverter of qualid * string * bool
   | Rremovepr  of qualid
+  | Rremoveall
   | Rmeta      of string * metarg list
 
 type theory_rules = {
diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll
index d78521bc65251f7a5ccad0faf6fddcf9f999adb7..0e95e8f8c2ccdc52dd75c16aaf933514f6474041 100644
--- a/src/driver/driver_lexer.mll
+++ b/src/driver/driver_lexer.mll
@@ -47,6 +47,7 @@
         "predicate", PREDICATE;
         "type", TYPE;
         "prop", PROP;
+        "allprops", ALL;
         "filename", FILENAME;
         "transformation", TRANSFORM;
         "plugin", PLUGIN;
diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly
index c722a9fde885cb749544890c2c64bb3a88bf4d00..8af74602c7d43efb79606a441f86dbeb3c9e6489 100644
--- a/src/driver/driver_parser.mly
+++ b/src/driver/driver_parser.mly
@@ -28,7 +28,7 @@
 %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
 %token BLACKLIST
 %token MODULE EXCEPTION VAL CONVERTER
-%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
+%token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
 %token LEFTPAR_STAR_RIGHTPAR COMMA CONSTANT
 %token LEFTSQ RIGHTSQ LARROW
 
@@ -90,6 +90,7 @@ trule:
 | syntax PREDICATE qualid STRING { Rsyntaxps  ($3, $4, $1) }
 | syntax CONVERTER qualid STRING { Rconverter ($3, $4, $1) }
 | REMOVE PROP qualid             { Rremovepr  ($3) }
+| REMOVE ALL                     { Rremoveall }
 | META ident meta_args           { Rmeta      ($2, $3) }
 | META STRING meta_args          { Rmeta      ($2, $3) }
 
diff --git a/src/whyml/mlw_driver.ml b/src/whyml/mlw_driver.ml
index 12ca5f5780df315419b11c7acedc29f00c0f9f72..40077d80572dbbf6e8d1d57cc12ea6aff30836ed 100644
--- a/src/whyml/mlw_driver.ml
+++ b/src/whyml/mlw_driver.ml
@@ -116,7 +116,13 @@ let load_driver env file extra_files =
     | Rconverter _ ->
         Loc.errorm "Syntax converter cannot be used in pure theories"
     | Rremovepr (q) ->
-        ignore (find_pr th q)
+      ignore (find_pr th q)
+    | Rremoveall ->
+      let it key _ = match (Mid.find key th.th_known).Decl.d_node with
+        | Decl.Dprop (_,symb,_) -> ignore symb
+        | _ -> ()
+      in
+      Mid.iter it th.th_local
     | Rmeta (s,al) ->
         let rec ty_of_pty = function
           | PTyvar x ->