diff --git a/examples/cursor/why3session.xml b/examples/cursor/why3session.xml
index 15113b01be9ab9de4594f2ee0e58106fd14e371c..582bbcaea64daf2b311509ea9f64f55d8e99622b 100644
--- a/examples/cursor/why3session.xml
+++ b/examples/cursor/why3session.xml
@@ -101,7 +101,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="IntArrayCursor" sum="8090cb9a5eb720659015e09ae27d5ddf" expanded="true">
+<theory name="IntArrayCursor" sum="0e0d1427d3bf976c46e43f3795d29aa6" expanded="true">
  <goal name="WP_parameter create" expl="VC for create" expanded="true">
  <proof prover="5"><result status="valid" time="0.05" steps="15"/></proof>
  </goal>
@@ -137,12 +137,12 @@
   <proof prover="1"><result status="unknown" time="0.05"/></proof>
   </goal>
   <goal name="WP_parameter next.4" expl="4. postcondition">
-  <proof prover="2"><result status="valid" time="0.27"/></proof>
+  <proof prover="2"><result status="valid" time="0.41"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="TestArrayCursor" sum="32c64c0426c4c4a9eb75e763071b02bd">
+<theory name="TestArrayCursor" sum="7d18da58ded19d7039316e45244f1693">
  <goal name="WP_parameter array_sum_array_to_list" expl="VC for array_sum_array_to_list">
  <proof prover="1"><result status="valid" time="0.04" steps="46"/></proof>
  </goal>
diff --git a/examples/cursor/why3shapes.gz b/examples/cursor/why3shapes.gz
index f6e2cbc298bc202bef02159c41a1dffef3044a19..315b94fb2003432928ca47ebad2e053450af03ae 100644
Binary files a/examples/cursor/why3shapes.gz and b/examples/cursor/why3shapes.gz differ
diff --git a/examples/dijkstra/why3session.xml b/examples/dijkstra/why3session.xml
index 303ae2839cd017ff319c90910693a06b4664aa3a..6ab3b537f6774efca43c766fa1f10a43dd01e836 100644
--- a/examples/dijkstra/why3session.xml
+++ b/examples/dijkstra/why3session.xml
@@ -9,7 +9,7 @@
 <prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../dijkstra.mlw" expanded="true">
-<theory name="DijkstraShortestPath" sum="927fe939ad868be15f33edef384e9149" expanded="true">
+<theory name="DijkstraShortestPath" sum="56fdafe8906f0c9270722a213f328c54" expanded="true">
  <goal name="WP_parameter relax" expl="VC for relax">
  <transf name="split_goal_wp">
   <goal name="WP_parameter relax.1" expl="1. postcondition">
@@ -134,7 +134,7 @@
     <proof prover="8"><result status="valid" time="0.04" steps="86"/></proof>
     </goal>
     <goal name="WP_parameter shortest_path_code.12.1.2" expl="2. VC for shortest_path_code">
-    <proof prover="2" timelimit="10"><result status="valid" time="0.84"/></proof>
+    <proof prover="2" timelimit="10"><result status="valid" time="1.08"/></proof>
     </goal>
     <goal name="WP_parameter shortest_path_code.12.1.3" expl="3. VC for shortest_path_code">
     <proof prover="8"><result status="valid" time="0.03" steps="25"/></proof>
diff --git a/examples/dijkstra/why3shapes.gz b/examples/dijkstra/why3shapes.gz
index 4037c37db3eb1a247966799f4f1d721104ea5376..88a4678b4bf039ee1a053918f8276a5ad4d4cf80 100644
Binary files a/examples/dijkstra/why3shapes.gz and b/examples/dijkstra/why3shapes.gz differ
diff --git a/examples/double_wp/logic/why3session.xml b/examples/double_wp/logic/why3session.xml
index 924a51b94022f5f1a2c4714c050176484550babc..9fd18c38ca1462a66548d53ca3bc5a9a759fd214 100644
--- a/examples/double_wp/logic/why3session.xml
+++ b/examples/double_wp/logic/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.3" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../logic.mlw">
-<theory name="Compiler_logic" sum="01e7845ed8490da8741a9ca86ba106c9">
+<theory name="Compiler_logic" sum="c12240d535cc2c746aa01470b9422232">
  <goal name="seq_wp_lemma">
  <proof prover="2"><result status="valid" time="0.04" steps="8"/></proof>
  </goal>
@@ -72,7 +72,7 @@
    </goal>
    <goal name="WP_parameter make_loop_hl.1.2" expl="2. assertion">
    <transf name="induction_pr">
-    <goal name="WP_parameter make_loop_hl.1.2.1" expl="1. VC for make_loop_hl">
+    <goal name="WP_parameter make_loop_hl.1.2.1" expl="1. assertion">
     <transf name="simplify_trivial_quantification_in_goal">
      <goal name="WP_parameter make_loop_hl.1.2.1.1" expl="1. VC for make_loop_hl">
      <transf name="compute_specified">
diff --git a/examples/double_wp/logic/why3shapes.gz b/examples/double_wp/logic/why3shapes.gz
index a3348d05ea69ed3c986def7aefd4568d6d5ba571..a5eb0e836c3353e5db19dc8ca75196ad31349dd3 100644
Binary files a/examples/double_wp/logic/why3shapes.gz and b/examples/double_wp/logic/why3shapes.gz differ
diff --git a/examples/double_wp/vm/why3session.xml b/examples/double_wp/vm/why3session.xml
index cd2ee5fde2931b94c2876c415b8969f5dc69c003..d2e9ee79fccc2076cd2334c97fd10573f8e58c2e 100644
--- a/examples/double_wp/vm/why3session.xml
+++ b/examples/double_wp/vm/why3session.xml
@@ -3,19 +3,20 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../vm.mlw" expanded="true">
-<theory name="ReflTransClosure" sum="b95bd9cec6f5b6d4f89525010d16d760">
+<theory name="ReflTransClosure" sum="f262a809b2b34d0ef483b05c11f8827b">
  <goal name="transition_star_one">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="transition_star_transitive">
  <transf name="induction_pr">
   <goal name="transition_star_transitive.1" expl="1.">
-  <proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
   </goal>
   <goal name="transition_star_transitive.2" expl="2.">
-  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/examples/double_wp/vm/why3shapes.gz b/examples/double_wp/vm/why3shapes.gz
index 44458e7506ea62b8a49699c49d0cced8fd2e4494..faca0b49f4caf5d75d3e95dce067a65ad9249109 100644
Binary files a/examples/double_wp/vm/why3shapes.gz and b/examples/double_wp/vm/why3shapes.gz differ
diff --git a/examples/fibonacci.mlw b/examples/fibonacci.mlw
index 93749e8c32b3acb256c4044cf4e8d58f531045a2..bdfb39d0f6f6d8aa3927d1945f96d7f9b916ec10 100644
--- a/examples/fibonacci.mlw
+++ b/examples/fibonacci.mlw
@@ -271,13 +271,10 @@ theory Mat22 "2x2 integer matrices"
     a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22;
     }
 
-  (* holds, but not useful *)
-  (* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *)
-
   clone export
     int.Exponentiation with
       type t = t, function one = id, function (*) = mult,
-      goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r
+      goal Assoc, goal Unit_def_l, goal Unit_def_r
 
 end
 
diff --git a/examples/ieee_float.mlw b/examples/tests-provers/ieee_float.mlw
similarity index 100%
rename from examples/ieee_float.mlw
rename to examples/tests-provers/ieee_float.mlw
diff --git a/examples/ieee_float/why3session.xml b/examples/tests-provers/ieee_float/why3session.xml
similarity index 100%
rename from examples/ieee_float/why3session.xml
rename to examples/tests-provers/ieee_float/why3session.xml
diff --git a/examples/tests-provers/ieee_float/why3shapes.gz b/examples/tests-provers/ieee_float/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..39412e954b3663097aee7e466ff63cb10de9e290
Binary files /dev/null and b/examples/tests-provers/ieee_float/why3shapes.gz differ
diff --git a/theories/int.why b/theories/int.why
index 97874584ce332774edccde96e4c04978ff26a3f6..199a1798a6f24f056a39438cc1609c5070f5b594 100644
--- a/theories/int.why
+++ b/theories/int.why
@@ -245,7 +245,7 @@ theory Exponentiation
   constant one : t
   function (*) t t : t
 
-  clone export algebra.CommutativeMonoid
+  clone export algebra.Monoid
     with type t = t, constant unit = one, function op = (*)
 
   (* TODO: implement with let rec once let cloning is done *)
@@ -293,7 +293,7 @@ theory Power
   clone export Exponentiation with
     type t = int, constant one = one,
     function (*) = (*), function power = power,
-    goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r
+    goal Assoc, goal Unit_def_l, goal Unit_def_r
 
   lemma Power_non_neg:
      forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
diff --git a/theories/real.why b/theories/real.why
index ed1dd45a65167bb9dfc3903aa40d014a812ab3a8..e8b9d6923610262c8b909618f56edd9eac8db8f5 100644
--- a/theories/real.why
+++ b/theories/real.why
@@ -255,7 +255,7 @@ theory PowerInt
 
   clone export int.Exponentiation with
     type t = real, constant one = Real.one, function (*) = Real.(*),
-    goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r
+    goal Assoc, goal Unit_def_l, goal Unit_def_r
 
   lemma Pow_ge_one:
     forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n