fix issue #188

the beginner transformation `split_vc` is now using `introduce_premises` followed by `subst_all`, instead of `simplify_trivial_quantification` followed by `introduce_premises`. following Andrei's suggestion, instead of `subst_all` we instead substitute only the symbols that (1) were introduced earlier and (2) do not have any attributes `[@model...]` so as to keep symbols present in the initial code.

fix issue #188
the beginner transformation `split_vc` is now using `introduce_premises` followed by `subst_all`, instead of `simplify_trivial_quantification` followed by `introduce_premises`. following Andrei's suggestion, instead of `subst_all` we instead substitute only the symbols that (1) were introduced earlier and (2) do not have any attributes `[@model...]` so as to keep symbols present in the initial code.
22ab5177 · MARCHE Claude · eb96f1af · 22ab5177 · 22ab5177 · 22ab5177
Commit 22ab5177 authored Oct 02, 2018 by MARCHE Claude
45 changed files
--- a/examples/binary_sort/why3shapes.gz
+++ b/examples/binary_sort/why3shapes.gz
--- a/examples/bitvectors/bitvector/why3shapes.gz
+++ b/examples/bitvectors/bitvector/why3shapes.gz
--- a/examples/euler011/why3session.xml
+++ b/examples/euler011/why3session.xml
--- a/examples/euler011/why3shapes.gz
+++ b/examples/euler011/why3shapes.gz
--- a/examples/fenwick/why3session.xml
+++ b/examples/fenwick/why3session.xml
@@ -15,10 +15,10 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC add.1" expl="index in array bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.06"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC add.2" expl="index in array bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.06"/></proof>
  </goal>
  <goal name="VC add.3" expl="loop invariant init" proved="true">
  <proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -98,7 +98,7 @@
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC query.8" expl="index in array bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC query.9" expl="precondition" proved="true">
  <proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -107,7 +107,7 @@
  <proof prover="2"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="VC query.11" expl="loop variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.06"/></proof>
+  <proof prover="2"><result status="valid" time="0.08"/></proof>
  </goal>
  <goal name="VC query.12" expl="loop invariant preservation" proved="true">
  <proof prover="2"><result status="valid" time="0.09"/></proof>
@@ -137,7 +137,7 @@
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC query.21" expl="index in array bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC query.22" expl="precondition" proved="true">
  <proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -146,7 +146,7 @@
  <proof prover="2"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="VC query.24" expl="loop variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.08"/></proof>
+  <proof prover="2"><result status="valid" time="0.06"/></proof>
  </goal>
  <goal name="VC query.25" expl="loop invariant preservation" proved="true">
  <proof prover="2"><result status="valid" time="0.09"/></proof>

--- a/examples/fenwick/why3shapes.gz
+++ b/examples/fenwick/why3shapes.gz
--- a/examples/hillel_challenge/why3session.xml
+++ b/examples/hillel_challenge/why3session.xml
@@ -3,8 +3,10 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../hillel_challenge.mlw" proved="true">
 <theory name="Leftpad" proved="true">
 <goal name="VC leftpad" expl="VC for leftpad" proved="true">
@@ -48,9 +50,9 @@
  <proof prover="3"><result status="valid" time="0.84"/></proof>
  </goal>
  <goal name="VC unique.11" expl="loop invariant preservation" proved="true">
-  <transf name="case" proved="true" arg1="(x=o)">
+  <transf name="case" proved="true" arg1="x=a[i]">
   <goal name="VC unique.11.0" expl="true case (loop invariant preservation)" proved="true">
-   <proof prover="2"><result status="valid" time="0.01" steps="88"/></proof>
+   <proof prover="1"><result status="valid" time="0.01" steps="75"/></proof>
   </goal>
   <goal name="VC unique.11.1" expl="false case (loop invariant preservation)" proved="true">
   <transf name="assert" proved="true" arg1="(mem x a (i+1) &lt;-&gt; mem x a i)">
@@ -70,12 +72,12 @@
   <proof prover="2"><result status="valid" time="0.01" steps="44"/></proof>
   </goal>
   <goal name="VC unique.12.1" expl="false case (loop invariant preservation)" proved="true">
-   <transf name="assert" proved="true" arg1="(not (mem o a i1))">
+   <transf name="assert" proved="true" arg1="(not (mem a[i1] a i1))">
    <goal name="VC unique.12.1.0" proved="true">
-    <proof prover="0"><result status="valid" time="0.03"/></proof>
+    <proof prover="4"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC unique.12.1.1" expl="false case (loop invariant preservation)" proved="true">
-    <proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
+    <proof prover="1"><result status="valid" time="0.01" steps="92"/></proof>
    </goal>
   </transf>
   </goal>
@@ -88,17 +90,17 @@
  <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC unique.15" expl="loop invariant preservation" proved="true">
-  <transf name="case" proved="true" arg1="(x = o)">
+  <transf name="case" proved="true" arg1="(x=n-1)">
   <goal name="VC unique.15.0" expl="true case (loop invariant preservation)" proved="true">
-   <proof prover="2"><result status="valid" time="0.02" steps="54"/></proof>
+   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC unique.15.1" expl="false case (loop invariant preservation)" proved="true">
   <transf name="assert" proved="true" arg1="(mem x a (i+1) &lt;-&gt; mem x a i)">
    <goal name="VC unique.15.1.0" proved="true">
-    <proof prover="0"><result status="valid" time="0.06"/></proof>
+    <proof prover="0"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC unique.15.1.1" expl="false case (loop invariant preservation)" proved="true">
-    <proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
+    <proof prover="2"><result status="valid" time="0.00" steps="25"/></proof>
    </goal>
   </transf>
   </goal>
@@ -126,7 +128,7 @@
 <goal name="VC fulcrum" expl="VC for fulcrum" proved="true">
 <transf name="split_vc" proved="true" >
  <goal name="VC fulcrum.0" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC fulcrum.1" expl="index in array bounds" proved="true">
  <proof prover="0"><result status="valid" time="0.01"/></proof>
@@ -135,7 +137,7 @@
  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC fulcrum.3" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC fulcrum.4" expl="loop invariant init" proved="true">
  <proof prover="0"><result status="valid" time="0.01"/></proof>
@@ -219,7 +221,7 @@
  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC add_big.3" expl="integer overflow" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC add_big.4" expl="type invariant" proved="true">
  <proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -253,7 +255,7 @@
  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC add_big.9" expl="integer overflow" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC add_big.10" expl="integer overflow" proved="true">
  <proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -284,7 +286,7 @@
 <goal name="VC delta" expl="VC for delta" proved="true">
 <transf name="split_vc" proved="true" >
  <goal name="VC delta.0" expl="integer overflow" proved="true">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC delta.1" expl="integer overflow" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -302,7 +304,7 @@
  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC delta.6" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.06"/></proof>
+  <proof prover="0"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC delta.7" expl="integer overflow" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -311,7 +313,7 @@
  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC delta.9" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05"/></proof>
+  <proof prover="0"><result status="valid" time="0.06"/></proof>
  </goal>
  <goal name="VC delta.10" expl="integer overflow" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -329,7 +331,7 @@
  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC delta.15" expl="integer overflow" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC delta.16" expl="integer overflow" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -338,7 +340,7 @@
  <proof prover="0"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC delta.18" expl="integer overflow" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC delta.19" expl="precondition" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -441,7 +443,7 @@
  <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC fulcrum.28" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.01" steps="38"/></proof>
+  <proof prover="2"><result status="valid" time="0.01" steps="61"/></proof>
  </goal>
  <goal name="VC fulcrum.29" expl="loop invariant preservation" proved="true">
  <proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -456,10 +458,10 @@
  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC fulcrum.33" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
+  <proof prover="2"><result status="valid" time="0.02" steps="51"/></proof>
  </goal>
  <goal name="VC fulcrum.34" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.01" steps="31"/></proof>
+  <proof prover="2"><result status="valid" time="0.01" steps="55"/></proof>
  </goal>
  <goal name="VC fulcrum.35" expl="postcondition" proved="true">
  <proof prover="0"><result status="valid" time="0.02"/></proof>

--- a/examples/hillel_challenge/why3shapes.gz
+++ b/examples/hillel_challenge/why3shapes.gz
--- a/examples/max_matrix/why3shapes.gz
+++ b/examples/max_matrix/why3shapes.gz
--- a/examples/maximum_subarray/why3shapes.gz
+++ b/examples/maximum_subarray/why3shapes.gz
--- a/examples/mccarthy/why3session.xml
+++ b/examples/mccarthy/why3session.xml
@@ -43,19 +43,19 @@
  <proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
  </goal>
  <goal name="VC f91_nonrec.2" expl="loop variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
+  <proof prover="3"><result status="valid" time="0.00" steps="15"/></proof>
  </goal>
  <goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.03" steps="217"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="85"/></proof>
  </goal>
  <goal name="VC f91_nonrec.4" expl="integer overflow" proved="true">
  <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
  </goal>
  <goal name="VC f91_nonrec.5" expl="loop variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
+  <proof prover="3"><result status="valid" time="0.00" steps="15"/></proof>
  </goal>
  <goal name="VC f91_nonrec.6" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="3.56" steps="4952"/></proof>
+  <proof prover="3"><result status="valid" time="3.34" steps="4574"/></proof>
  </goal>
  <goal name="VC f91_nonrec.7" expl="postcondition" proved="true">
  <proof prover="3"><result status="valid" time="0.00" steps="30"/></proof>

--- a/examples/mccarthy/why3shapes.gz
+++ b/examples/mccarthy/why3shapes.gz
--- a/examples/mex/why3shapes.gz
+++ b/examples/mex/why3shapes.gz
--- a/examples/pancake_sorting/why3shapes.gz
+++ b/examples/pancake_sorting/why3shapes.gz
--- a/examples/power/why3shapes.gz
+++ b/examples/power/why3shapes.gz
--- a/examples/power_vc_sp/why3shapes.gz
+++ b/examples/power_vc_sp/why3shapes.gz
--- a/examples/prover/Firstorder_formula_impl/why3session.xml
+++ b/examples/prover/Firstorder_formula_impl/why3session.xml
@@ -1343,7 +1343,7 @@
  <proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="14"/></proof>
  </goal>
  <goal name="VC subst_base_symbol_in_fo_formula.20" expl="variant decrease" proved="true">
-  <proof prover="0" timelimit="5"><result status="valid" time="0.19" steps="93"/></proof>
+  <proof prover="0" timelimit="5"><result status="valid" time="0.07" steps="93"/></proof>
  </goal>
  <goal name="VC subst_base_symbol_in_fo_formula.21" expl="precondition" proved="true">
  <proof prover="0" timelimit="5"><result status="valid" time="0.13" steps="47"/></proof>
@@ -1716,7 +1716,7 @@
   <proof prover="2"><result status="valid" time="1.03"/></proof>
   </goal>
   <goal name="VC construct_fo_formula.4.2" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.12" steps="244"/></proof>
+   <proof prover="0"><result status="valid" time="0.12" steps="245"/></proof>
   </goal>
   <goal name="VC construct_fo_formula.4.3" expl="assertion" proved="true">
   <proof prover="2"><result status="valid" time="0.23"/></proof>
@@ -1786,7 +1786,7 @@
   <proof prover="0"><result status="valid" time="0.06" steps="77"/></proof>
   </goal>
   <goal name="VC construct_fo_formula.20.2" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.13" steps="244"/></proof>
+   <proof prover="0"><result status="valid" time="0.13" steps="245"/></proof>
   </goal>
   <goal name="VC construct_fo_formula.20.3" expl="assertion" proved="true">
   <proof prover="2"><result status="valid" time="0.26"/></proof>
@@ -2348,7 +2348,7 @@
  <proof prover="0" timelimit="5"><result status="valid" time="0.12" steps="25"/></proof>
  </goal>
  <goal name="VC destruct_fo_formula.26" expl="unreachable point" proved="true">
-  <proof prover="0"><result status="valid" time="0.17" steps="25"/></proof>
+  <proof prover="0"><result status="valid" time="0.05" steps="25"/></proof>
  </goal>
  <goal name="VC destruct_fo_formula.27" expl="unreachable point" proved="true">
  <proof prover="0"><result status="valid" time="0.16" steps="23"/></proof>
@@ -2616,7 +2616,7 @@
  <proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="21"/></proof>
  </goal>
  <goal name="VC destruct_fo_formula.100" expl="unreachable point" proved="true">
-  <proof prover="0"><result status="valid" time="0.17" steps="21"/></proof>
+  <proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
  </goal>
  <goal name="VC destruct_fo_formula.101" expl="unreachable point" proved="true">
  <proof prover="0"><result status="valid" time="0.05" steps="23"/></proof>
@@ -3081,7 +3081,7 @@
   <proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="67"/></proof>
   </goal>
   <goal name="VC nlsubst_symbol_in_fo_formula.9.3" expl="assertion" proved="true">
-   <proof prover="2"><result status="valid" time="0.42"/></proof>
+   <proof prover="2"><result status="valid" time="0.27"/></proof>
   </goal>
   <goal name="VC nlsubst_symbol_in_fo_formula.9.4" expl="assertion" proved="true">
   <proof prover="2"><result status="valid" time="0.64"/></proof>

--- a/examples/prover/Firstorder_formula_impl/why3shapes.gz
+++ b/examples/prover/Firstorder_formula_impl/why3shapes.gz
--- a/examples/prover/Firstorder_formula_spec/why3session.xml
+++ b/examples/prover/Firstorder_formula_spec/why3session.xml
@@ -48,25 +48,25 @@
 <goal name="VC subst_then_rename_composition_lemma_fo_formula" expl="VC for subst_then_rename_composition_lemma_fo_formula" proved="true">
 <transf name="split_vc" proved="true" >
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.0" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.20"/></proof>
+  <proof prover="3"><result status="valid" time="0.12"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.1" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.12"/></proof>
+  <proof prover="3"><result status="valid" time="0.20"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.2" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.21"/></proof>
+  <proof prover="3"><result status="valid" time="0.12"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.3" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.24"/></proof>
+  <proof prover="3"><result status="valid" time="0.12"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.4" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.12"/></proof>
+  <proof prover="3"><result status="valid" time="0.16"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.5" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.16"/></proof>
+  <proof prover="3"><result status="valid" time="0.24"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.6" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.12"/></proof>
+  <proof prover="3"><result status="valid" time="0.21"/></proof>
  </goal>
  <goal name="VC subst_then_rename_composition_lemma_fo_formula.7" expl="postcondition" proved="true">
  <transf name="destruct_alg_subst" proved="true" arg1="t">
@@ -113,25 +113,25 @@
 <goal name="VC subst_composition_lemma_fo_formula" expl="VC for subst_composition_lemma_fo_formula" proved="true">
 <transf name="split_vc" proved="true" >
  <goal name="VC subst_composition_lemma_fo_formula.0" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.18"/></proof>
+  <proof prover="3"><result status="valid" time="0.12"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.1" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.12"/></proof>
+  <proof prover="3"><result status="valid" time="0.18"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.2" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.17"/></proof>
+  <proof prover="3"><result status="valid" time="0.20"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.3" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.20"/></proof>
+  <proof prover="3"><result status="valid" time="0.22"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.4" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.20"/></proof>
+  <proof prover="3"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.5" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.17"/></proof>
+  <proof prover="3"><result status="valid" time="0.20"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.6" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.22"/></proof>
+  <proof prover="3"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="VC subst_composition_lemma_fo_formula.7" expl="postcondition" proved="true">
  <transf name="destruct_alg_subst" proved="true" arg1="t">
@@ -192,16 +192,16 @@
   <proof prover="3"><result status="valid" time="0.28"/></proof>
   </goal>
   <goal name="VC subst_identity_lemma_fo_formula.7.1" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.40"/></proof>
+   <proof prover="3"><result status="valid" time="0.24"/></proof>
   </goal>
   <goal name="VC subst_identity_lemma_fo_formula.7.2" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.26"/></proof>
+   <proof prover="3"><result status="valid" time="0.25"/></proof>
   </goal>
   <goal name="VC subst_identity_lemma_fo_formula.7.3" expl="postcondition" proved="true">
   <proof prover="3"><result status="valid" time="0.23"/></proof>
   </goal>
   <goal name="VC subst_identity_lemma_fo_formula.7.4" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.24"/></proof>
+   <proof prover="3"><result status="valid" time="0.40"/></proof>
   </goal>
   <goal name="VC subst_identity_lemma_fo_formula.7.5" expl="postcondition" proved="true">
   <proof prover="3"><result status="valid" time="0.21"/></proof>
@@ -210,7 +210,7 @@
   <proof prover="3"><result status="valid" time="0.20"/></proof>
   </goal>
   <goal name="VC subst_identity_lemma_fo_formula.7.7" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.25"/></proof>
+   <proof prover="3"><result status="valid" time="0.26"/></proof>
   </goal>
  </transf>
  </goal>
@@ -219,22 +219,22 @@
 <goal name="VC renaming_preserve_size_fo_formula" expl="VC for renaming_preserve_size_fo_formula" proved="true">
 <transf name="split_vc" proved="true" >
  <goal name="VC renaming_preserve_size_fo_formula.0" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.18"/></proof>
+  <proof prover="3"><result status="valid" time="0.15"/></proof>
  </goal>
  <goal name="VC renaming_preserve_size_fo_formula.1" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.15"/></proof>
+  <proof prover="3"><result status="valid" time="0.18"/></proof>
  </goal>
  <goal name="VC renaming_preserve_size_fo_formula.2" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.14"/></proof>
+  <proof prover="3"><result status="valid" time="0.15"/></proof>
  </goal>
  <goal name="VC renaming_preserve_size_fo_formula.3" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.21"/></proof>
+  <proof prover="3"><result status="valid" time="0.14"/></proof>
  </goal>
  <goal name="VC renaming_preserve_size_fo_formula.4" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.15"/></proof>
+  <proof prover="3"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="VC renaming_preserve_size_fo_formula.5" expl="variant decrease" proved="true">
-  <proof prover="3"><result status="valid" time="0.17"/></proof>
+  <proof prover="3"><result status="valid" time="0.21"/></proof>
  </goal>
  <goal name="VC renaming_preserve_size_fo_formula.6" expl="variant decrease" proved="true">
  <proof prover="3"><result status="valid" time="0.14"/></proof>

--- a/examples/prover/Firstorder_formula_spec/why3shapes.gz
+++ b/examples/prover/Firstorder_formula_spec/why3shapes.gz
--- a/examples/prover/ISet/why3shapes.gz
+++ b/examples/prover/ISet/why3shapes.gz
--- a/examples/prover/Prover/why3session.xml
+++ b/examples/prover/Prover/why3session.xml
--- a/examples/prover/Prover/why3shapes.gz
+++ b/examples/prover/Prover/why3shapes.gz
--- a/examples/prover/Unification/why3session.xml
+++ b/examples/prover/Unification/why3session.xml
@@ -5,6 +5,7 @@
 <prover id="0" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Eprover" version="1.8-001" timelimit="30" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -762,11 +763,7 @@
  <proof prover="12"><result status="valid" time="0.12" steps="163"/></proof>
  </goal>
  <goal name="VC unification_term.17" expl="precondition" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="VC unification_term.17.0" expl="precondition" proved="true">
-   <proof prover="11"><result status="valid" time="0.16"/></proof>
-   </goal>
-  </transf>
+  <proof prover="3"><result status="valid" time="0.07" steps="273"/></proof>
  </goal>
  <goal name="VC unification_term.18" expl="precondition" proved="true">
  <proof prover="12"><result status="valid" time="0.07" steps="27"/></proof>

--- a/examples/prover/Unification/why3shapes.gz
+++ b/examples/prover/Unification/why3shapes.gz
--- a/examples/random_access_list/why3session.xml
+++ b/examples/random_access_list/why3session.xml
@@ -149,33 +149,33 @@
  <proof prover="3" timelimit="5"><result status="valid" time="0.00" steps="7"/></proof>
  </goal>
  <goal name="VC lookup.1" expl="variant decrease" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="5"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
  <goal name="VC lookup.2" expl="precondition" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="20"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="19"/></proof>
  </goal>
  <goal name="VC lookup.3" expl="precondition" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
  </goal>
  <goal name="VC lookup.4" expl="variant decrease" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="42"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="7"/></proof>
  </goal>
  <goal name="VC lookup.5" expl="precondition" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="38"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="37"/></proof>
  </goal>
  <goal name="VC lookup.6" expl="precondition" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="5"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
  <goal name="VC lookup.7" expl="postcondition" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC lookup.7.0" expl="postcondition" proved="true">
-   <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="11"/></proof>
+   <proof prover="3" timelimit="5"><result status="valid" time="0.06" steps="10"/></proof>
   </goal>
   <goal name="VC lookup.7.1" expl="postcondition" proved="true">
-   <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="27"/></proof>
+   <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="66"/></proof>
   </goal>
   <goal name="VC lookup.7.2" expl="postcondition" proved="true">
-   <proof prover="3" timelimit="5"><result status="valid" time="0.06" steps="96"/></proof>
+   <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="98"/></proof>
   </goal>
  </transf>
  </goal>

--- a/examples/random_access_list/why3shapes.gz
+++ b/examples/random_access_list/why3shapes.gz
--- a/examples/stdlib/pigeon/why3session.xml
+++ b/examples/stdlib/pigeon/why3session.xml
@@ -23,7 +23,6 @@
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC pigeonhole.4" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC pigeonhole.5" expl="precondition" proved="true">
@@ -44,6 +43,7 @@
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC pigeonhole.10" expl="variant decrease" proved="true">
+  <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC pigeonhole.11" expl="precondition" proved="true">

--- a/examples/stdlib/pigeon/why3shapes.gz
+++ b/examples/stdlib/pigeon/why3shapes.gz
--- a/examples/stdlib/witness/why3shapes.gz
+++ b/examples/stdlib/witness/why3shapes.gz
--- a/examples/tortoise_and_hare/why3session.xml
+++ b/examples/tortoise_and_hare/why3session.xml
@@ -63,16 +63,16 @@
 <goal name="VC equality" expl="VC for equality" proved="true">
 <transf name="split_vc" proved="true" >
  <goal name="VC equality.0" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.02"/></proof>
+  <proof prover="6"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="VC equality.1" expl="precondition" proved="true">
-  <proof prover="6"><result status="valid" time="0.03"/></proof>
+  <proof prover="6" timelimit="5"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC equality.2" expl="postcondition" proved="true">
  <proof prover="6"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC equality.3" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.07"/></proof>
+  <proof prover="6"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC equality.4" expl="precondition" proved="true">
  <proof prover="6"><result status="valid" time="0.05"/></proof>
@@ -100,7 +100,7 @@
  <proof prover="6" timelimit="5"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC equality.10" expl="precondition" proved="true">
-  <proof prover="6" timelimit="5"><result status="valid" time="0.03"/></proof>
+  <proof prover="6"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC equality.11" expl="precondition" proved="true">
  <proof prover="5"><result status="valid" time="0.02"/></proof>
@@ -127,7 +127,7 @@
  <proof prover="5"><result status="valid" time="0.21"/></proof>
  </goal>
  <goal name="VC equality.19" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03" steps="73"/></proof>
+  <proof prover="2"><result status="valid" time="0.03" steps="80"/></proof>
  </goal>
  <goal name="VC equality.20" expl="postcondition" proved="true">
  <transf name="split_vc" proved="true" >

--- a/examples/tortoise_and_hare/why3shapes.gz
+++ b/examples/tortoise_and_hare/why3shapes.gz
--- a/examples/tree_of_array/why3shapes.gz
+++ b/examples/tree_of_array/why3shapes.gz
--- a/examples/tree_of_list/why3shapes.gz
+++ b/examples/tree_of_list/why3shapes.gz
--- a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
+++ b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
@@ -218,7 +218,7 @@
  <proof prover="0" timelimit="5"><result status="valid" time="4.95"/></proof>
  </goal>
  <goal name="VC padding.6" expl="assertion" proved="true">
-  <proof prover="0" timelimit="20"><result status="valid" time="1.67"/></proof>
+  <proof prover="0" timelimit="20"><result status="valid" time="2.96"/></proof>
  </goal>
  <goal name="VC padding.7" expl="assertion" proved="true">
  <proof prover="1" timelimit="5"><result status="valid" time="0.78" steps="919"/></proof>
@@ -261,10 +261,10 @@
  <proof prover="1"><result status="valid" time="0.03" steps="14"/></proof>
  </goal>
  <goal name="VC strassen.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
+  <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
  </goal>
  <goal name="VC strassen.7" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
+  <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
  </goal>
  <goal name="VC strassen.8" expl="postcondition" proved="true">
  <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
@@ -1074,7 +1074,7 @@
  <proof prover="1"><result status="valid" time="0.10" steps="196"/></proof>
  </goal>
  <goal name="VC strassen.186" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.14"/></proof>
+  <proof prover="0"><result status="valid" time="0.28"/></proof>
  </goal>
  <goal name="VC strassen.187" expl="precondition" proved="true">
  <proof prover="1"><result status="valid" time="0.38" steps="1048"/></proof>

--- a/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz
+++ b/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz
--- a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
+++ b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
--- a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz
+++ b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz
--- a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml
+++ b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml
--- a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz
+++ b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz
--- a/examples/verifythis_2018_mind_the_gap_2/why3session.xml
+++ b/examples/verifythis_2018_mind_the_gap_2/why3session.xml
@@ -24,13 +24,13 @@
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC left.4" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="56"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="61"/></proof>
  </goal>
  <goal name="VC left.5" expl="postcondition" proved="true">
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC left.6" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
  </goal>
 </transf>
 </goal>
@@ -49,13 +49,13 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC right.4" expl="postcondition" proved="true">
-  <proof prover="0" memlimit="2000"><result status="valid" time="0.02" steps="52"/></proof>
+  <proof prover="0" memlimit="2000"><result status="valid" time="0.02" steps="61"/></proof>
  </goal>
  <goal name="VC right.5" expl="postcondition" proved="true">
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC right.6" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
  </goal>
 </transf>
 </goal>
@@ -99,10 +99,10 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC insert.2" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC insert.3" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="173"/></proof>
+  <proof prover="0"><result status="valid" time="0.03" steps="188"/></proof>
  </goal>
  <goal name="VC insert.4" expl="index in array bounds" proved="true">
  <proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -111,10 +111,10 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC insert.6" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC insert.7" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03" steps="94"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="115"/></proof>