Merge branch 'master' into itp

Conflicts: examples/dijkstra/why3session.xml examples/dijkstra/why3shapes.gz src/tools/why3prove.ml

Merge branch 'master' into itp
Conflicts: examples/dijkstra/why3session.xml examples/dijkstra/why3shapes.gz src/tools/why3prove.ml
eb43812d · MARCHE Claude · 81bbad2b · eb751c1b · eb43812d · eb43812d
Commit eb43812d authored May 24, 2017 by MARCHE Claude
--- 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>

--- a/examples/cursor/why3shapes.gz
+++ b/examples/cursor/why3shapes.gz
--- 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">

--- a/examples/double_wp/logic/why3shapes.gz
+++ b/examples/double_wp/logic/why3shapes.gz
--- 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>

--- a/examples/double_wp/vm/why3shapes.gz
+++ b/examples/double_wp/vm/why3shapes.gz
--- a/examples/fibonacci.mlw
+++ b/examples/fibonacci.mlw
@@ -271,11 +271,9 @@ 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
+    int.Exponentiation with type t = t, function one = id, function (*) = mult,
+    goal Monoid.Assoc, goal Monoid.Unit_def_l, goal Monoid.Unit_def_r

 end


--- a/examples/fibonacci/why3session.xml
+++ b/examples/fibonacci/why3session.xml
@@ -3,9 +3,10 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
+<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="7" name="Vampire" version="0.6" timelimit="3" steplimit="0" memlimit="0"/>
+<prover id="7" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="10" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="0"/>
@@ -21,7 +22,7 @@
 <goal name="not_isfib_2_2">
 <proof prover="2" memlimit="0"><result status="valid" time="0.00"/></proof>
 <proof prover="4"><result status="valid" time="0.02"/></proof>
- <proof prover="7" timelimit="5"><result status="valid" time="0.03"/></proof>
+ <proof prover="7"><result status="valid" time="0.03"/></proof>
 <proof prover="8" memlimit="0"><result status="valid" time="0.01" steps="4"/></proof>
 <proof prover="10"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -430,21 +431,28 @@
 </transf>
 </goal>
 </theory>
-<theory name="Mat22" sum="d41d8cd98f00b204e9800998ecf8427e">
+<theory name="Mat22" sum="cc41e6488bdd64071b3c815e4f5356d3">
+ <goal name="Monoid.Assoc">
+ <proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
+ </goal>
+ <goal name="Monoid.Unit_def_l">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+ <goal name="Monoid.Unit_def_r">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
 </theory>
-<theory name="FibonacciLogarithmic" sum="b47fef62882561569b783ece5a6bfae1">
+<theory name="FibonacciLogarithmic" sum="1463e67fce33079e4726bf939886c65a">
 <goal name="WP_parameter logfib" expl="VC for logfib">
 <transf name="split_goal_wp">
  <goal name="WP_parameter logfib.1" expl="1. postcondition">
-  <proof prover="2" memlimit="0"><result status="valid" time="0.00"/></proof>
-  <proof prover="7"><result status="valid" time="0.00"/></proof>
-  <proof prover="8" memlimit="0"><result status="valid" time="0.01" steps="5"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
  </goal>
  <goal name="WP_parameter logfib.2" expl="2. variant decrease">
-  <proof prover="8"><result status="valid" time="0.00" steps="4"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
  <goal name="WP_parameter logfib.3" expl="3. precondition">
-  <proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
  </goal>
  <goal name="WP_parameter logfib.4" expl="4. postcondition">
  <proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="0.47"/></proof>
@@ -455,26 +463,25 @@
 <proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="0.40"/></proof>
 </goal>
 <goal name="WP_parameter fibo" expl="VC for fibo">
- <proof prover="2" memlimit="0"><result status="valid" time="0.00"/></proof>
- <proof prover="8" memlimit="0"><result status="valid" time="0.00" steps="5"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
 </goal>
 <goal name="WP_parameter test0" expl="VC for test0">
- <proof prover="8"><result status="valid" time="0.01" steps="2"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
 </goal>
 <goal name="WP_parameter test1" expl="VC for test1">
- <proof prover="8"><result status="valid" time="0.00" steps="2"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
 </goal>
 <goal name="WP_parameter test7" expl="VC for test7">
- <proof prover="8"><result status="valid" time="0.01" steps="2"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
 </goal>
 <goal name="WP_parameter test42" expl="VC for test42">
- <proof prover="8"><result status="valid" time="0.02" steps="2"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
 </goal>
 <goal name="WP_parameter test2014" expl="VC for test2014">
- <proof prover="8" memlimit="4000"><result status="valid" time="0.01" steps="2"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
 </goal>
 <goal name="WP_parameter bench" expl="VC for bench">
- <proof prover="8" memlimit="4000"><result status="valid" time="0.01" steps="2"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/fibonacci/why3shapes.gz
+++ b/examples/fibonacci/why3shapes.gz
--- a/examples/koda_ruskey/why3session.xml
+++ b/examples/koda_ruskey/why3session.xml
@@ -3,12 +3,13 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="36" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Eprover" version="1.8-001" timelimit="36" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
-<file name="../koda_ruskey.mlw">
+<file name="../koda_ruskey.mlw" expanded="true">
 <theory name="KodaRuskey_Spec" sum="8e518d6f01f787c2ba93abeff13d48b2">
 <goal name="size_forest_nonneg">
 <transf name="induction_ty_lex">
@@ -25,7 +26,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="Lemmas" sum="69586628d3c613c629b078044197f281">
+<theory name="Lemmas" sum="3c7358ff49ab0c33420397550d3b9052">
 <goal name="mem_app">
 <transf name="induction_ty_lex">
  <goal name="mem_app.1" expl="1.">
@@ -202,10 +203,10 @@
  <proof prover="7"><result status="valid" time="0.00" steps="11"/></proof>
  </goal>
  <goal name="sub_not_nil.2" expl="2.">
-  <proof prover="0" timelimit="6"><result status="valid" time="0.01"/></proof>
+  <proof prover="1"><result status="valid" time="0.76"/></proof>
  </goal>
  <goal name="sub_not_nil.3" expl="3.">
-  <proof prover="7"><result status="valid" time="0.01" steps="37"/></proof>
+  <proof prover="0" timelimit="6"><result status="valid" time="0.01"/></proof>
  </goal>
 </transf>
 </goal>
@@ -215,10 +216,10 @@
  <proof prover="7" timelimit="5"><result status="valid" time="0.00" steps="12"/></proof>
  </goal>
  <goal name="sub_empty.2" expl="2.">
-  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="32"/></proof>
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="sub_empty.3" expl="3.">
-  <proof prover="0"><result status="valid" time="1.13"/></proof>
+  <proof prover="1"><result status="valid" time="3.23"/></proof>
  </goal>
 </transf>
 </goal>
@@ -228,15 +229,15 @@
  <proof prover="7" timelimit="5"><result status="valid" time="0.00" steps="23"/></proof>
  </goal>
  <goal name="sub_mem.2" expl="2.">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
-  </goal>
-  <goal name="sub_mem.3" expl="3.">
  <transf name="simplify_trivial_quantification">
-   <goal name="sub_mem.3.1" expl="1.">
+   <goal name="sub_mem.2.1" expl="1.">
   <proof prover="0"><result status="valid" time="0.04"/></proof>
   </goal>
  </transf>
  </goal>
+  <goal name="sub_mem.3" expl="3.">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
 </transf>
 </goal>
 <goal name="sub_weaken1">
@@ -245,15 +246,15 @@
  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="sub_weaken1.2" expl="2.">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
-  </goal>
-  <goal name="sub_weaken1.3" expl="3.">
  <transf name="induction_ty_lex">
-   <goal name="sub_weaken1.3.1" expl="1.">
-   <proof prover="7" timelimit="5"><result status="valid" time="0.71" steps="908"/></proof>
+   <goal name="sub_weaken1.2.1" expl="1.">
+   <proof prover="7" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
   </goal>
  </transf>
  </goal>
+  <goal name="sub_weaken1.3" expl="3.">
+  <proof prover="0"><result status="valid" time="1.33"/></proof>
+  </goal>
 </transf>
 </goal>
 <goal name="sub_weaken2">
@@ -262,17 +263,22 @@
  <proof prover="0"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="sub_weaken2.2" expl="2.">
-  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="58"/></proof>
-  </goal>
-  <goal name="sub_weaken2.3" expl="3.">
  <transf name="induction_ty_lex">
-   <goal name="sub_weaken2.3.1" expl="1.">
+   <goal name="sub_weaken2.2.1" expl="1.">
   <transf name="split_goal_wp">
-    <goal name="sub_weaken2.3.1.1" expl="1.">
+    <goal name="sub_weaken2.2.1.1" expl="1.">
    <proof prover="6"><result status="valid" time="0.02"/></proof>
    </goal>
-    <goal name="sub_weaken2.3.1.2" expl="2.">
-    <proof prover="0"><result status="valid" time="0.20"/></proof>
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="sub_weaken2.3" expl="3.">
+  <transf name="simplify_trivial_quantification_in_goal">
+   <goal name="sub_weaken2.3.1" expl="1.">
+   <transf name="introduce_premises">
+    <goal name="sub_weaken2.3.1.1" expl="1.">
+    <proof prover="1" timelimit="30" memlimit="4000"><result status="valid" time="0.88"/></proof>
    </goal>
   </transf>
   </goal>
@@ -286,10 +292,10 @@
  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="13"/></proof>
  </goal>
  <goal name="not_mem_st.2" expl="2.">
-  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="25"/></proof>
+  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="26"/></proof>
  </goal>
  <goal name="not_mem_st.3" expl="3.">
-  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="87"/></proof>
+  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="88"/></proof>
  </goal>
 </transf>
 </goal>
@@ -299,10 +305,10 @@
  <proof prover="7" timelimit="5"><result status="valid" time="0.01" steps="12"/></proof>
  </goal>
  <goal name="sub_frame.2" expl="2.">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="sub_frame.3" expl="3.">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
 </transf>
 </goal>
@@ -312,10 +318,10 @@
  <proof prover="7" timelimit="5" steplimit="-1"><result status="valid" time="0.01" steps="12"/></proof>
  </goal>
  <goal name="sub_no_rep.2" expl="2.">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.13"/></proof>
  </goal>
  <goal name="sub_no_rep.3" expl="3.">
-  <proof prover="0"><result status="valid" time="0.13"/></proof>
+  <proof prover="0"><result status="valid" time="0.16"/></proof>
  </goal>
 </transf>
 </goal>
@@ -331,14 +337,14 @@
  <goal name="sub_no_rep2.2" expl="2.">
  <transf name="split_goal_wp">
   <goal name="sub_no_rep2.2.1" expl="1.">
-   <proof prover="0"><result status="valid" time="0.03"/></proof>
+   <proof prover="0"><result status="valid" time="0.04"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="sub_no_rep2.3" expl="3.">
  <transf name="split_goal_wp">
   <goal name="sub_no_rep2.3.1" expl="1.">
-   <proof prover="0"><result status="valid" time="1.74"/></proof>
+   <proof prover="0"><result status="valid" time="1.09"/></proof>
   </goal>
  </transf>
  </goal>
@@ -422,9 +428,24 @@
  <goal name="sub_valid_coloring.2" expl="2.">
  <transf name="introduce_premises">
   <goal name="sub_valid_coloring.2.1" expl="1.">
-   <transf name="compute_in_goal">
+   <transf name="simplify_trivial_quantification">
    <goal name="sub_valid_coloring.2.1.1" expl="1.">
-    <proof prover="0" timelimit="6"><result status="valid" time="0.10"/></proof>
+    <transf name="compute_in_goal">
+     <goal name="sub_valid_coloring.2.1.1.1" expl="1.">
+     <transf name="split_goal_wp">
+      <goal name="sub_valid_coloring.2.1.1.1.1" expl="1.">
+      <proof prover="7" timelimit="5"><result status="valid" time="0.04" steps="98"/></proof>
+      </goal>
+      <goal name="sub_valid_coloring.2.1.1.1.2" expl="2.">
+      <proof prover="0" timelimit="6"><result status="valid" time="0.18"/></proof>
+      </goal>
+      <goal name="sub_valid_coloring.2.1.1.1.3" expl="3.">
+      <proof prover="0"><result status="valid" time="0.20"/></proof>
+      <proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
+      </goal>
+     </transf>
+     </goal>
+    </transf>
    </goal>
   </transf>
   </goal>
@@ -433,23 +454,22 @@
  <goal name="sub_valid_coloring.3" expl="3.">
  <transf name="introduce_premises">
   <goal name="sub_valid_coloring.3.1" expl="1.">
-   <transf name="simplify_trivial_quantification">
+   <transf name="compute_in_goal">
    <goal name="sub_valid_coloring.3.1.1" expl="1.">
-    <transf name="compute_in_goal">
+    <transf name="split_goal_wp">
     <goal name="sub_valid_coloring.3.1.1.1" expl="1.">
-     <transf name="split_goal_wp">
+     <transf name="introduce_premises">
      <goal name="sub_valid_coloring.3.1.1.1.1" expl="1.">
-      <proof prover="4" edited="koda_ruskey_Lemmas_sub_valid_coloring_1.v"><result status="valid" time="4.50"/></proof>
-      </goal>
-      <goal name="sub_valid_coloring.3.1.1.1.2" expl="2.">
-      <proof prover="0" timelimit="6"><result status="valid" time="0.04"/></proof>
-      <proof prover="7"><result status="valid" time="0.01" steps="57"/></proof>
-      </goal>
-      <goal name="sub_valid_coloring.3.1.1.1.3" expl="3.">
-      <proof prover="7"><result status="valid" time="0.28" steps="537"/></proof>
+      <proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="12.19"/></proof>
      </goal>
     </transf>
     </goal>
+     <goal name="sub_valid_coloring.3.1.1.2" expl="2.">
+     <proof prover="1" timelimit="1"><result status="valid" time="0.03"/></proof>
+     </goal>
+     <goal name="sub_valid_coloring.3.1.1.3" expl="3.">
+     <proof prover="7" timelimit="1"><result status="valid" time="0.18" steps="326"/></proof>
+     </goal>
    </transf>
    </goal>
   </transf>
@@ -464,10 +484,10 @@
  <proof prover="7" timelimit="26"><result status="valid" time="0.01" steps="14"/></proof>
  </goal>
  <goal name="sub_Cons_N.2" expl="2.">
-  <proof prover="0" timelimit="26"><result status="valid" time="0.08"/></proof>
+  <proof prover="0" timelimit="26"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="sub_Cons_N.3" expl="3.">
-  <proof prover="0" timelimit="26"><result status="valid" time="0.02"/></proof>
+  <proof prover="0" timelimit="26"><result status="valid" time="0.08"/></proof>
  </goal>
 </transf>
 </goal>
@@ -792,7 +812,6 @@
     </goal>
     <goal name="WP_parameter enum.49.1.1.2" expl="2. VC for enum">
     <proof prover="0" timelimit="16"><result status="valid" time="10.18"/></proof>
-     <proof prover="7" timelimit="16"><result status="timeout" time="17.66"/></proof>
     </goal>
     <goal name="WP_parameter enum.49.1.1.3" expl="3. VC for enum">
     <proof prover="0" timelimit="16"><result status="valid" time="0.35"/></proof>

--- a/examples/koda_ruskey/why3shapes.gz
+++ b/examples/koda_ruskey/why3shapes.gz
--- a/examples/schorr_waite_via_recursion/why3session.xml
+++ b/examples/schorr_waite_via_recursion/why3session.xml
@@ -8,7 +8,7 @@
 </theory>
 <theory name="GraphShape" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="SchorrWaite" sum="fff0d08f435a9cc7f0ce6b34b7547c29" expanded="true">
+<theory name="SchorrWaite" sum="60eff84723b352455c04d10ba2696679" expanded="true">
 <goal name="WP_parameter black" expl="VC for black">
 <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
 </goal>
@@ -408,7 +408,7 @@
  <proof prover="0"><result status="valid" time="0.05" steps="97"/></proof>
  </goal>
  <goal name="WP_parameter schorr_waite.132" expl="132. postcondition">
-  <proof prover="0"><result status="valid" time="0.79" steps="503"/></proof>
+  <proof prover="0"><result status="valid" time="0.61" steps="503"/></proof>
  </goal>
  <goal name="WP_parameter schorr_waite.133" expl="133. postcondition">
  <proof prover="0"><result status="valid" time="0.57" steps="416"/></proof>
@@ -519,7 +519,7 @@
  <proof prover="0"><result status="valid" time="0.47" steps="396"/></proof>
  </goal>
  <goal name="WP_parameter schorr_waite.169" expl="169. postcondition">
-  <proof prover="0" timelimit="20"><result status="valid" time="3.75" steps="2160"/></proof>
+  <proof prover="0" timelimit="20"><result status="valid" time="3.75" steps="2305"/></proof>
  </goal>
  <goal name="WP_parameter schorr_waite.170" expl="170. postcondition">
  <proof prover="0"><result status="valid" time="0.10" steps="103"/></proof>
@@ -562,23 +562,23 @@
  </goal>
  <goal name="WP_parameter schorr_waite.183" expl="183. assertion">
  <transf name="induction_pr">
-   <goal name="WP_parameter schorr_waite.183.1" expl="1. VC for schorr_waite">
+   <goal name="WP_parameter schorr_waite.183.1" expl="1. assertion">
   <transf name="simplify_trivial_quantification_in_goal">
    <goal name="WP_parameter schorr_waite.183.1.1" expl="1. VC for schorr_waite">
    <transf name="simplify_trivial_quantification_in_goal">
     <goal name="WP_parameter schorr_waite.183.1.1.1" expl="1. VC for schorr_waite">
-     <proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
+     <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
-   <goal name="WP_parameter schorr_waite.183.2" expl="2. VC for schorr_waite">
+   <goal name="WP_parameter schorr_waite.183.2" expl="2. assertion">
   <transf name="simplify_trivial_quantification_in_goal">
    <goal name="WP_parameter schorr_waite.183.2.1" expl="1. VC for schorr_waite">
    <transf name="simplify_trivial_quantification_in_goal">
     <goal name="WP_parameter schorr_waite.183.2.1.1" expl="1. VC for schorr_waite">
-     <proof prover="0"><result status="valid" time="0.02" steps="64"/></proof>
+     <proof prover="0"><result status="valid" time="0.01" steps="64"/></proof>
     </goal>
    </transf>
    </goal>

--- a/examples/schorr_waite_via_recursion/why3shapes.gz
+++ b/examples/schorr_waite_via_recursion/why3shapes.gz
--- a/examples/stdlib/array/why3session.xml
+++ b/examples/stdlib/array/why3session.xml
@@ -4,11 +4,12 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.4.0" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Coq" version="8.6" timelimit="6" steplimit="0" memlimit="1000"/>
-<file name="../../../modules/array.mlw">
-<theory name="Array" sum="324e125dff69cfce0eefc07a77b17b42">
+<file name="../../../modules/array.mlw" expanded="true">
+<theory name="Array" sum="285c467dea3cde7aa3a3c699222d37ee">
 <goal name="WP_parameter defensive_get" expl="VC for defensive_get">
 <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
 <proof prover="4"><result status="valid" time="0.01"/></proof>
@@ -21,6 +22,9 @@
 <proof prover="0"><result status="valid" time="0.02" steps="58"/></proof>
 <proof prover="4"><result status="valid" time="0.06"/></proof>
 </goal>
+ <goal name="WP_parameter self_blit" expl="VC for self_blit">
+ <proof prover="2"><result status="valid" time="0.10" steps="148"/></proof>
+ </goal>
 </theory>
 <theory name="IntArraySorted" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
@@ -53,7 +57,10 @@
 </theory>
 <theory name="NumOfEq" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="ToList" sum="d41d8cd98f00b204e9800998ecf8427e">
+<theory name="ToList" sum="b7bcfe4954496ee8ce9bf8d36ab68113">
+ <goal name="WP_parameter to_list_append" expl="VC for to_list_append">
+ <proof prover="2"><result status="valid" time="0.01" steps="34"/></proof>
+ </goal>
 </theory>
 <theory name="ToSeq" sum="972d3973679c1b19bf79339fb847c382">
 <goal name="WP_parameter to_seq_length" expl="VC for to_seq_length">

--- a/examples/stdlib/array/why3shapes.gz
+++ b/examples/stdlib/array/why3shapes.gz
--- a/examples/tests-provers/bv/why3session.xml
+++ b/examples/tests-provers/bv/why3session.xml
@@ -9,7 +9,7 @@
 <prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../bv.why" expanded="true">
-<theory name="CheckBV64" sum="855747e71f46058c96f9a701bed1fff5" expanded="true">
+<theory name="CheckBV64" sum="e1d447629924850ec87d19e840f58819" expanded="true">
 <goal name="ok_zero">
 <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
 <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -197,7 +197,7 @@
 </goal>
 <goal name="smoke4">
 <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="unknown" time="0.56"/></proof>
+ <proof prover="1"><result status="unknown" time="3.04"/></proof>
 <proof prover="2"><result status="unknown" time="0.01"/></proof>
 <proof prover="3"><result status="timeout" time="0.95"/></proof>
 <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
@@ -260,12 +260,12 @@
 <proof prover="4"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="g3a">
- <proof prover="1"><result status="valid" time="2.12"/></proof>
+ <proof prover="1"><result status="valid" time="0.81"/></proof>
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 <proof prover="4"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="g3b">
- <proof prover="1"><result status="valid" time="0.99"/></proof>
+ <proof prover="1"><result status="valid" time="0.24"/></proof>
 <transf name="compute_in_goal">
  <goal name="g3b.1" expl="1.">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
@@ -275,7 +275,7 @@
 </goal>
 <goal name="f3">
 <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="unknown" time="3.36"/></proof>
+ <proof prover="1"><result status="unknown" time="4.01"/></proof>
 <proof prover="2"><result status="unknown" time="0.00"/></proof>
 <proof prover="3"><result status="timeout" time="0.89"/></proof>
 <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
@@ -301,7 +301,7 @@
 <proof prover="4"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="g7">
- <proof prover="0"><result status="valid" time="0.04" steps="74"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
 <proof prover="1"><result status="valid" time="0.02"/></proof>
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 <proof prover="3" timelimit="5"><result status="valid" time="0.12"/></proof>
@@ -385,7 +385,7 @@
 <proof prover="4"><result status="valid" time="0.02"/></proof>
 </goal>
 </theory>
-<theory name="CheckBV32" sum="b1a27c5773887143af0b808502b49f11">
+<theory name="CheckBV32" sum="379a581bc41c1769af82fa1e277addf0">
 <goal name="ok_zero">
 <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
 <proof prover="1"><result status="valid" time="0.03"/></proof>
@@ -482,7 +482,7 @@
 <proof prover="4"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="ok13">
- <proof prover="1"><result status="valid" time="1.08"/></proof>
+ <proof prover="1"><result status="valid" time="0.36"/></proof>
 <proof prover="2"><result stat