diff --git a/creusot/tests/should_succeed/hashmap.rs b/creusot/tests/should_succeed/hashmap.rs
index 1c0dc64b8c..0d3790f851 100644
--- a/creusot/tests/should_succeed/hashmap.rs
+++ b/creusot/tests/should_succeed/hashmap.rs
@@ -46,7 +46,6 @@ impl<K: DeepModel, V> List<(K, V)> {
     }
 }
 
-
 impl<K: DeepModel, V> Resolve for List<(K, V)> {
     #[open(self)]
     #[predicate(prophetic)]
diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml
index 3e6e64ec1d..6237a4e3e4 100644
--- a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml
+++ b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml
@@ -8,6 +8,16 @@
 <prover id="3" name="CVC5" version="1.0.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="04_skip.coma"/>
+<theory name="M_04_skip__qyi11651659076391631465__resolve_coherence__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="0"><result status="valid" time="0.034225" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="M_04_skip__qyi11651659076391631465__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="3"><result status="valid" time="0.027573" steps="236"/></proof>
+ </goal>
+</theory>
 <theory name="M_04_skip__qyi17349041008065389927__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
  <proof prover="0"><result status="valid" time="0.040767" steps="0"/></proof>
diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz b/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz
index b0d3f00169..c6f3097688 100644
Binary files a/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz and b/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/iterators/05_map/why3session.xml b/creusot/tests/should_succeed/iterators/05_map/why3session.xml
index c0e0c6f28a..a0cd157890 100644
--- a/creusot/tests/should_succeed/iterators/05_map/why3session.xml
+++ b/creusot/tests/should_succeed/iterators/05_map/why3session.xml
@@ -8,22 +8,32 @@
 <prover id="3" name="CVC5" version="1.0.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="05_map.coma"/>
-<theory name="M_05_map__qyi14910388998417814812__produces_refl__refines" proved="true">
+<theory name="M_05_map__qyi4717544419812877023__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.044652" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.039510" steps="2"/></proof>
  </goal>
 </theory>
-<theory name="M_05_map__qyi14910388998417814812__produces_refl" proved="true">
+<theory name="M_05_map__qyi4717544419812877023__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="1"><result status="valid" time="0.038536" steps="7"/></proof>
+ </goal>
+</theory>
+<theory name="M_05_map__qyi16807608259409463994__produces_refl__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.027547" steps="1280"/></proof>
+ </goal>
+</theory>
+<theory name="M_05_map__qyi16807608259409463994__produces_refl" proved="true">
  <goal name="vc_produces_refl&#39;0" proved="true">
- <proof prover="3"><result status="valid" time="0.097618" steps="5785"/></proof>
+ <proof prover="3"><result status="valid" time="0.083092" steps="5785"/></proof>
  </goal>
 </theory>
-<theory name="M_05_map__qyi14910388998417814812__produces_trans__refines" proved="true">
+<theory name="M_05_map__qyi16807608259409463994__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.040467" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.045929" steps="1280"/></proof>
  </goal>
 </theory>
-<theory name="M_05_map__qyi14910388998417814812__produces_trans" proved="true">
+<theory name="M_05_map__qyi16807608259409463994__produces_trans" proved="true">
  <goal name="vc_produces_trans&#39;0" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="vc_produces_trans&#39;0.0" proved="true">
@@ -33,17 +43,17 @@
     <goal name="vc_produces_trans&#39;0.0.0.0" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="vc_produces_trans&#39;0.0.0.0.0" proved="true">
-     <proof prover="0"><result status="valid" time="0.016570" steps="35892"/></proof>
+     <proof prover="1"><result status="valid" time="0.043474" steps="44"/></proof>
      </goal>
      <goal name="vc_produces_trans&#39;0.0.0.0.1" proved="true">
      <transf name="exists" proved="true" arg1="(fs++fs1)">
       <goal name="vc_produces_trans&#39;0.0.0.0.1.0" proved="true">
       <transf name="split_vc" proved="true" >
        <goal name="vc_produces_trans&#39;0.0.0.0.1.0.0" proved="true">
-       <proof prover="0"><result status="valid" time="0.019150" steps="37398"/></proof>
+       <proof prover="1"><result status="valid" time="0.057629" steps="33"/></proof>
        </goal>
        <goal name="vc_produces_trans&#39;0.0.0.0.1.0.1" proved="true">
-       <proof prover="0"><result status="valid" time="0.320893" steps="848163"/></proof>
+       <proof prover="0"><result status="valid" time="0.509686" steps="848163"/></proof>
        </goal>
       </transf>
       </goal>
@@ -58,37 +68,30 @@
  </transf>
  </goal>
 </theory>
-<theory name="M_05_map__qyi14910388998417814812__next__refines" proved="true">
+<theory name="M_05_map__qyi16807608259409463994__next__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.143710" steps="490"/></proof>
+ <proof prover="1"><result status="valid" time="0.168132" steps="490"/></proof>
  </goal>
 </theory>
-<theory name="M_05_map__qyi14910388998417814812__next" proved="true">
+<theory name="M_05_map__qyi16807608259409463994__next" proved="true">
  <goal name="vc_next&#39;0" proved="true">
- <proof prover="0"><result status="valid" time="0.049368" steps="75559"/></proof>
+ <proof prover="3"><result status="valid" time="0.234538" steps="13778"/></proof>
  </goal>
 </theory>
-<theory name="M_05_map__qyi9543869049664362474__produces_one_invariant" proved="true">
+<theory name="M_05_map__qyi6570657843506441439__produces_one_invariant" proved="true">
  <goal name="vc_produces_one_invariant&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_one_invariant&#39;0.0" proved="true">
-  <proof prover="2"><result status="valid" time="0.459920" steps="86629"/></proof>
+  <proof prover="2"><result status="valid" time="1.136915" steps="86629"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="M_05_map__qyi9543869049664362474__produces_one" proved="true">
+<theory name="M_05_map__qyi6570657843506441439__produces_one" proved="true">
  <goal name="vc_produces_one&#39;0" proved="true">
- <transf name="split_vc" proved="true" >
+ <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_one&#39;0.0" proved="true">
-  <proof prover="2"><result status="valid" time="0.232149" steps="49982"/></proof>
-  </goal>
-  <goal name="vc_produces_one&#39;0.1" proved="true">
-  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
-   <goal name="vc_produces_one&#39;0.1.0" proved="true">
-   <proof prover="3"><result status="valid" time="0.170794" steps="18454"/></proof>
-   </goal>
-  </transf>
+  <proof prover="3"><result status="valid" time="1.630000" steps="143128"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz b/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz
index 78fe98279d..63ef7065b6 100644
Binary files a/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz and b/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml
index 17247e21c2..da3b93c0c0 100644
--- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml
+++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml
@@ -7,43 +7,49 @@
 <prover id="4" name="CVC5" version="1.0.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="06_map_precond.coma"/>
-<theory name="M_06_map_precond__qyi18374305379273630819__produces_refl__refines" proved="true">
+<theory name="M_06_map_precond__qyi12121551022315030028__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.039759" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.034746" steps="2"/></proof>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi18374305379273630819__produces_refl" proved="true">
+<theory name="M_06_map_precond__qyi12121551022315030028__resolve_coherence" proved="true">
+ <goal name="vc_resolve_coherence&#39;0" proved="true">
+ <proof prover="4"><result status="valid" time="0.038221" steps="1693"/></proof>
+ </goal>
+</theory>
+<theory name="M_06_map_precond__qyi16809708214464407778__produces_refl__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="4"><result status="valid" time="0.030135" steps="1669"/></proof>
+ </goal>
+</theory>
+<theory name="M_06_map_precond__qyi16809708214464407778__produces_refl" proved="true">
  <goal name="vc_produces_refl&#39;0" proved="true">
- <transf name="split_vc" proved="true" >
+ <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_refl&#39;0.0" proved="true">
-  <transf name="inline_goal" proved="true" >
-   <goal name="vc_produces_refl&#39;0.0.0" proved="true">
-   <proof prover="4"><result status="valid" time="0.092212" steps="11052"/></proof>
-   </goal>
-  </transf>
+  <proof prover="4"><result status="valid" time="0.117728" steps="11661"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi18374305379273630819__produces_trans__refines" proved="true">
+<theory name="M_06_map_precond__qyi16809708214464407778__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.038764" steps="0"/></proof>
+ <proof prover="4"><result status="valid" time="0.049164" steps="1669"/></proof>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi18374305379273630819__produces_trans" proved="true">
+<theory name="M_06_map_precond__qyi16809708214464407778__produces_trans" proved="true">
  <goal name="vc_produces_trans&#39;0" proved="true">
  <transf name="unfold" proved="true" arg1="produces&#39;0">
   <goal name="vc_produces_trans&#39;0.0" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
-   <proof prover="3" timelimit="1"><result status="valid" time="0.021772" steps="49"/></proof>
+   <proof prover="3"><result status="valid" time="0.045225" steps="49"/></proof>
    </goal>
    <goal name="vc_produces_trans&#39;0.0.1" proved="true">
    <transf name="exists" proved="true" arg1="(fs++fs1)">
     <goal name="vc_produces_trans&#39;0.0.1.0" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="vc_produces_trans&#39;0.0.1.0.0" proved="true">
-     <proof prover="3"><result status="valid" time="0.029943" steps="39"/></proof>
+     <proof prover="3"><result status="valid" time="0.046498" steps="39"/></proof>
      </goal>
      <goal name="vc_produces_trans&#39;0.0.1.0.1" proved="true">
      <transf name="exists" proved="true" arg1="(s++s1)">
@@ -52,35 +58,35 @@
        <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0" proved="true">
        <transf name="split_vc" proved="true" >
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.0" proved="true">
-        <proof prover="3"><result status="valid" time="0.031077" steps="45"/></proof>
+        <proof prover="3"><result status="valid" time="0.043297" steps="45"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.1" proved="true">
-        <proof prover="4"><result status="valid" time="0.063623" steps="10715"/></proof>
+        <proof prover="3"><result status="valid" time="0.041327" steps="39"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.2" proved="true">
-        <proof prover="3"><result status="valid" time="0.032317" steps="250"/></proof>
+        <proof prover="3"><result status="valid" time="0.067377" steps="250"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.3" proved="true">
-        <proof prover="3"><result status="valid" time="0.091952" steps="392"/></proof>
+        <proof prover="3"><result status="valid" time="0.092722" steps="392"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.4" proved="true">
-        <proof prover="3"><result status="valid" time="0.031623" steps="71"/></proof>
+        <proof prover="3"><result status="valid" time="0.067816" steps="71"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.5" proved="true">
-        <proof prover="3"><result status="valid" time="0.053770" steps="166"/></proof>
+        <proof prover="3"><result status="valid" time="0.058771" steps="166"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.6" proved="true">
-        <proof prover="3"><result status="valid" time="0.058183" steps="204"/></proof>
+        <proof prover="3"><result status="valid" time="0.065260" steps="204"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.7" proved="true">
-        <proof prover="3"><result status="valid" time="0.181325" steps="722"/></proof>
+        <proof prover="3"><result status="valid" time="0.164904" steps="722"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.8" proved="true">
         <transf name="instantiate" proved="true" arg1="H2" arg2="i">
          <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.8.0" proved="true">
          <transf name="instantiate" proved="true" arg1="H10" arg2="(i-length ab)">
           <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.8.0.0" proved="true">
-          <proof prover="3"><result status="valid" time="0.359058" steps="3544"/></proof>
+          <proof prover="3"><result status="valid" time="0.716564" steps="3544"/></proof>
           </goal>
          </transf>
          </goal>
@@ -91,7 +97,7 @@
          <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.9.0" proved="true">
          <transf name="instantiate" proved="true" arg1="H10" arg2="(i-length ab)">
           <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.9.0.0" proved="true">
-          <proof prover="3"><result status="valid" time="0.413791" steps="3587"/></proof>
+          <proof prover="3"><result status="valid" time="0.753284" steps="3587"/></proof>
           </goal>
          </transf>
          </goal>
@@ -112,104 +118,100 @@
  </transf>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi18374305379273630819__next__refines" proved="true">
+<theory name="M_06_map_precond__qyi16809708214464407778__next__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3"><result status="valid" time="0.120409" steps="866"/></proof>
+ <proof prover="3"><result status="valid" time="0.266934" steps="866"/></proof>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi18374305379273630819__next" proved="true">
+<theory name="M_06_map_precond__qyi16809708214464407778__next" proved="true">
  <goal name="vc_next&#39;0" proved="true">
- <proof prover="4"><result status="valid" time="0.210941" steps="19642"/></proof>
+ <proof prover="4"><result status="valid" time="0.354113" steps="19642"/></proof>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi16548623944279504987__preservation_inv" proved="true">
+<theory name="M_06_map_precond__qyi15984651645423927012__preservation_inv" proved="true">
  <goal name="vc_preservation_inv&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_preservation_inv&#39;0.0" proved="true">
-  <proof prover="4" timelimit="1"><result status="valid" time="0.182945" steps="15345"/></proof>
+  <proof prover="4"><result status="valid" time="0.153147" steps="15345"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi16548623944279504987__produces_one_invariant" proved="true">
+<theory name="M_06_map_precond__qyi15984651645423927012__produces_one_invariant" proved="true">
  <goal name="vc_produces_one_invariant&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_one_invariant&#39;0.0" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="vc_produces_one_invariant&#39;0.0.0" proved="true">
-   <proof prover="2"><result status="valid" time="0.045086" steps="97791"/></proof>
+   <proof prover="3" timelimit="1"><result status="valid" time="0.231385" steps="1953"/></proof>
    </goal>
    <goal name="vc_produces_one_invariant&#39;0.0.1" proved="true">
-   <proof prover="3"><result status="valid" time="0.036797" steps="203"/></proof>
+   <proof prover="3" timelimit="1"><result status="valid" time="0.054650" steps="203"/></proof>
    </goal>
    <goal name="vc_produces_one_invariant&#39;0.0.2" proved="true">
-   <proof prover="4"><result status="valid" time="0.188068" steps="30664"/></proof>
+   <proof prover="4" timelimit="1"><result status="valid" time="0.318443" steps="30664"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="M_06_map_precond__qyi16548623944279504987__produces_one" proved="true">
+<theory name="M_06_map_precond__qyi15984651645423927012__produces_one" proved="true">
  <goal name="vc_produces_one&#39;0" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="vc_produces_one&#39;0.0" proved="true">
-  <transf name="split_vc" proved="true" >
+  <transf name="unfold" proved="true" arg1="produces&#39;0">
    <goal name="vc_produces_one&#39;0.0.0" proved="true">
-   <transf name="unfold" proved="true" arg1="produces&#39;0">
+   <transf name="split_vc" proved="true" >
     <goal name="vc_produces_one&#39;0.0.0.0" proved="true">
-    <transf name="split_vc" proved="true" >
-     <goal name="vc_produces_one&#39;0.0.0.0.0" proved="true">
-     <proof prover="3" timelimit="1"><result status="valid" time="0.017247" steps="16"/></proof>
-     </goal>
-     <goal name="vc_produces_one&#39;0.0.0.0.1" proved="true">
-     <transf name="exists" proved="true" arg1="(singleton f)">
-      <goal name="vc_produces_one&#39;0.0.0.0.1.0" proved="true">
-      <transf name="split_vc" proved="true" >
-       <goal name="vc_produces_one&#39;0.0.0.0.1.0.0" proved="true">
-       <proof prover="4" timelimit="1"><result status="valid" time="0.108061" steps="13720"/></proof>
-       </goal>
-       <goal name="vc_produces_one&#39;0.0.0.0.1.0.1" proved="true">
-       <transf name="exists" proved="true" arg1="(singleton e)">
-        <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0" proved="true">
-        <transf name="split_vc" proved="true" >
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.0" proved="true">
-         <proof prover="3"><result status="valid" time="0.016188" steps="19"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.1" proved="true">
-         <proof prover="3"><result status="valid" time="0.015339" steps="12"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.2" proved="true">
-         <proof prover="4"><result status="valid" time="0.172796" steps="16042"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.3" proved="true">
-         <proof prover="3"><result status="valid" time="0.032982" steps="24"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.4" proved="true">
-         <proof prover="3"><result status="valid" time="0.031105" steps="18"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.5" proved="true">
-         <proof prover="3"><result status="valid" time="0.028779" steps="17"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.6" proved="true">
-         <proof prover="3"><result status="valid" time="0.022084" steps="21"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.7" proved="true">
-         <proof prover="3"><result status="valid" time="0.039822" steps="30"/></proof>
-         </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.8" proved="true">
-         <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
-          <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.8.0" proved="true">
-          <proof prover="3"><result status="valid" time="0.079180" steps="349"/></proof>
-          </goal>
-         </transf>
+    <proof prover="3"><result status="valid" time="0.047540" steps="16"/></proof>
+    </goal>
+    <goal name="vc_produces_one&#39;0.0.0.1" proved="true">
+    <transf name="exists" proved="true" arg1="(singleton f)">
+     <goal name="vc_produces_one&#39;0.0.0.1.0" proved="true">
+     <transf name="split_vc" proved="true" >
+      <goal name="vc_produces_one&#39;0.0.0.1.0.0" proved="true">
+      <proof prover="3"><result status="valid" time="0.045785" steps="19"/></proof>
+      </goal>
+      <goal name="vc_produces_one&#39;0.0.0.1.0.1" proved="true">
+      <transf name="exists" proved="true" arg1="(singleton e)">
+       <goal name="vc_produces_one&#39;0.0.0.1.0.1.0" proved="true">
+       <transf name="split_vc" proved="true" >
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.0" proved="true">
+        <proof prover="3"><result status="valid" time="0.045425" steps="19"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.1" proved="true">
+        <proof prover="3"><result status="valid" time="0.043173" steps="12"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.2" proved="true">
+        <proof prover="3"><result status="valid" time="0.105708" steps="247"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.3" proved="true">
+        <proof prover="3"><result status="valid" time="0.058293" steps="24"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.4" proved="true">
+        <proof prover="3"><result status="valid" time="0.044418" steps="18"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.5" proved="true">
+        <proof prover="4"><result status="valid" time="0.104098" steps="11874"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.6" proved="true">
+        <proof prover="3"><result status="valid" time="0.041805" steps="21"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.7" proved="true">
+        <proof prover="3"><result status="valid" time="0.047911" steps="30"/></proof>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.8" proved="true">
+        <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
+         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.8.0" proved="true">
+         <proof prover="3"><result status="valid" time="0.091077" steps="349"/></proof>
          </goal>
-         <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.9" proved="true">
-         <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
-          <goal name="vc_produces_one&#39;0.0.0.0.1.0.1.0.9.0" proved="true">
-          <proof prover="3"><result status="valid" time="0.087548" steps="352"/></proof>
-          </goal>
-         </transf>
+        </transf>
+        </goal>
+        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.9" proved="true">
+        <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
+         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.9.0" proved="true">
+         <proof prover="3"><result status="valid" time="0.087451" steps="352"/></proof>
          </goal>
         </transf>
         </goal>
@@ -228,7 +230,7 @@
   <goal name="vc_produces_one&#39;0.1" proved="true">
   <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
    <goal name="vc_produces_one&#39;0.1.0" proved="true">
-   <proof prover="2"><result status="valid" time="0.184757" steps="256600"/></proof>
+   <proof prover="2"><result status="valid" time="0.184141" steps="256600"/></proof>
    </goal>
   </transf>
   </goal>
@@ -245,7 +247,7 @@
  <proof prover="3"><result status="valid" time="0.011285" steps="2"/></proof>
  </goal>
  <goal name="vc_identity&#39;0" proved="true">
- <proof prover="3" timelimit="1"><result status="valid" time="0.016418" steps="134"/></proof>
+ <proof prover="3"><result status="valid" time="0.016418" steps="134"/></proof>
  </goal>
 </theory>
 <theory name="M_06_map_precond__increment" proved="true">
@@ -255,25 +257,25 @@
  <goal name="vc_increment&#39;0" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="vc_increment&#39;0.0" expl="map &#39;iter&#39; type invariant" proved="true">
-  <proof prover="4"><result status="valid" time="0.095944" steps="10050"/></proof>
+  <proof prover="3"><result status="valid" time="0.059564" steps="2"/></proof>
   </goal>
   <goal name="vc_increment&#39;0.1" expl="map &#39;func&#39; type invariant" proved="true">
-  <proof prover="4" timelimit="1"><result status="valid" time="0.082459" steps="11517"/></proof>
+  <proof prover="4"><result status="valid" time="0.082459" steps="11517"/></proof>
   </goal>
   <goal name="vc_increment&#39;0.2" expl="map requires #0" proved="true">
-  <proof prover="3" timelimit="1"><result status="valid" time="0.029129" steps="30"/></proof>
+  <proof prover="3"><result status="valid" time="0.029129" steps="30"/></proof>
   </goal>
   <goal name="vc_increment&#39;0.3" expl="map requires #1" proved="true">
-  <proof prover="4"><result status="valid" time="0.151673" steps="19265"/></proof>
+  <proof prover="3"><result status="valid" time="0.096658" steps="142"/></proof>
   </goal>
   <goal name="vc_increment&#39;0.4" expl="map requires #2" proved="true">
-  <proof prover="3" timelimit="1"><result status="valid" time="0.011868" steps="82"/></proof>
+  <proof prover="3"><result status="valid" time="0.011868" steps="82"/></proof>
   </goal>
   <goal name="vc_increment&#39;0.5" expl="type invariant" proved="true">
-  <proof prover="3" timelimit="1"><result status="valid" time="0.017114" steps="5"/></proof>
+  <proof prover="2"><result status="valid" time="0.043267" steps="6042"/></proof>
   </goal>
   <goal name="vc_increment&#39;0.6" expl="assertion" proved="true">
-  <proof prover="4"><result status="valid" time="0.156018" steps="20794"/></proof>
+  <proof prover="2"><result status="valid" time="0.128001" steps="110613"/></proof>
   </goal>
  </transf>
  </goal>
@@ -283,7 +285,7 @@
  <proof prover="3"><result status="valid" time="0.018386" steps="77"/></proof>
  </goal>
  <goal name="vc_counter&#39;0" proved="true">
- <proof prover="3" timelimit="1"><result status="valid" time="0.075814" steps="502"/></proof>
+ <proof prover="3"><result status="valid" time="0.075814" steps="502"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz
index e9bbcd3a86..5a21487da5 100644
Binary files a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz and b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz differ