diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
index 1fdd2a63f0..199ca0ae8c 100644
--- a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
+++ b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
@@ -5,86 +5,26 @@
 <prover id="0" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="list_reversal_lasso.coma"/>
-<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
- <goal name="vc_t_nonnull" proved="true">
- <proof prover="2"><result status="valid" time="0.008053" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="Core_Marker_PhantomData_Type" proved="true">
- <goal name="vc_t_phantomdata" proved="true">
- <proof prover="2"><result status="valid" time="0.008700" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
- <goal name="vc_t_unique" proved="true">
- <proof prover="2"><result status="valid" time="0.007423" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_RawVec_Cap_Type" proved="true">
- <goal name="vc_t_cap" proved="true">
- <proof prover="2"><result status="valid" time="0.000001" steps="189"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_RawVec_RawVec_Type" proved="true">
- <goal name="vc_t_rawvec" proved="true">
- <proof prover="2"><result status="valid" time="0.002921" steps="189"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_Vec_Vec_Type" proved="true">
- <goal name="vc_t_vec" proved="true">
- <proof prover="2"><result status="valid" time="0.004360" steps="189"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_Alloc_Global_Type" proved="true">
- <goal name="vc_t_global" proved="true">
- <proof prover="2"><result status="valid" time="0.000001" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="ListReversalLasso_Memory_Type" proved="true">
- <goal name="vc_t_memory" proved="true">
- <proof prover="2"><result status="valid" time="0.000001" steps="189"/></proof>
- </goal>
-</theory>
 <theory name="ListReversalLasso_Impl1_Index" proved="true">
- <goal name="vc_index&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.010572" steps="4967"/></proof>
- </goal>
  <goal name="vc_index" proved="true">
  <proof prover="2"><result status="valid" time="0.028439" steps="9477"/></proof>
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl2_IndexMut" proved="true">
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.007065" steps="5210"/></proof>
- </goal>
  <goal name="vc_index_mut" proved="true">
  <proof prover="2"><result status="valid" time="0.056447" steps="13839"/></proof>
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalSafe" proved="true">
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.009311" steps="4924"/></proof>
- </goal>
- <goal name="vc_index&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.007023" steps="4924"/></proof>
- </goal>
  <goal name="vc_list_reversal_safe" proved="true">
  <proof prover="2"><result status="valid" time="0.124100" steps="25894"/></proof>
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalList" proved="true">
- <goal name="vc_replace&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.010478" steps="5187"/></proof>
- </goal>
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.017108" steps="5187"/></proof>
- </goal>
  <goal name="vc_list_reversal_list" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="2284627"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="9923"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="178269"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_list_reversal_list.0" expl="loop invariant" proved="true">
   <proof prover="2"><result status="valid" time="0.014781" steps="7045"/></proof>
@@ -132,16 +72,7 @@
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalLoop" proved="true">
- <goal name="vc_replace&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.009838" steps="5187"/></proof>
- </goal>
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.007594" steps="5187"/></proof>
- </goal>
  <goal name="vc_list_reversal_loop" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="2306363"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="11663"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="173651"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_list_reversal_loop.0" expl="loop invariant" proved="true">
   <proof prover="2"><result status="valid" time="0.024544" steps="9418"/></proof>
@@ -162,9 +93,6 @@
   <proof prover="1"><result status="valid" time="0.068348" steps="665"/></proof>
   </goal>
   <goal name="vc_list_reversal_loop.6" expl="postcondition" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="1729074"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="10836"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="133050"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_loop.6.0" expl="postcondition" proved="true">
    <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="4.168868" steps="38855"/></proof>
@@ -208,16 +136,7 @@
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalLasso" proved="true">
- <goal name="vc_replace&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.010438" steps="5187"/></proof>
- </goal>
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.013574" steps="5187"/></proof>
- </goal>
  <goal name="vc_list_reversal_lasso" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="1688325"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="8476"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="216314"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_list_reversal_lasso.0" expl="loop invariant" proved="true">
   <proof prover="2"><result status="valid" time="0.025380" steps="7295"/></proof>
@@ -235,14 +154,8 @@
   <proof prover="2"><result status="valid" time="0.056178" steps="15791"/></proof>
   </goal>
   <goal name="vc_list_reversal_lasso.5" expl="postcondition" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="1639253"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="7532"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="211553"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.5.0" expl="postcondition" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="8943428"/></proof>
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="50619"/></proof>
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="704220"/></proof>
    <transf name="inline_goal" proved="true" >
     <goal name="vc_list_reversal_lasso.5.0.0" expl="postcondition" proved="true">
     <transf name="split_all_full" proved="true" >
@@ -256,9 +169,6 @@
      <proof prover="2"><result status="valid" time="0.796825" steps="185143"/></proof>
      </goal>
      <goal name="vc_list_reversal_lasso.5.0.0.3" expl="postcondition" proved="true">
-     <proof prover="0"><result status="timeout" time="1.000000" steps="2602128"/></proof>
-     <proof prover="1"><result status="timeout" time="1.000000" steps="8692"/></proof>
-     <proof prover="2"><result status="timeout" time="1.000000" steps="169372"/></proof>
      <transf name="split_vc" proved="true" >
       <goal name="vc_list_reversal_lasso.5.0.0.3.0" expl="postcondition" proved="true">
       <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="3.299007" steps="31068"/></proof>
@@ -290,19 +200,17 @@
   <proof prover="2"><result status="valid" time="0.018920" steps="10575"/></proof>
   </goal>
   <goal name="vc_list_reversal_lasso.12" expl="loop invariant" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="2685935"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="10097"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="202665"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.12.0" expl="loop invariant" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="9836895"/></proof>
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="43348"/></proof>
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="680508"/></proof>
    <transf name="inline_goal" proved="true" >
     <goal name="vc_list_reversal_lasso.12.0.0" expl="loop invariant" proved="true">
     <transf name="split_all_full" proved="true" >
      <goal name="vc_list_reversal_lasso.12.0.0.0" proved="true">
-     <proof prover="1"><result status="valid" time="0.781007" steps="8157"/></proof>
+     <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,singleton,cons,snoc,(++),(^_),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;2,index_logic&#39;1,nonnull_ptr&#39;0,resolve&#39;1,resolve&#39;0,mid,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Rounds_toward_zero,create&#39;spec&#39;0,empty&#39;def,set&#39;spec,set&#39;spec&#39;0,set&#39;spec&#39;1,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,singleton&#39;spec&#39;0,cons&#39;spec,cons&#39;spec&#39;0,cons&#39;spec&#39;1,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inner_spec,inv&#39;3,inv&#39;2,inv&#39;1,inv&#39;0,Assert19,Assert13,Assert11,Assert10,Assert9,Assert7,Assert6,Assert5,Assert4,Assert3,Assert2,Assert1,Assert,Assert17,H2,H10,H8,H7,H6,Abs_le2,Abs_le1,Div_bound,Mod_bound1,shallow_model&#39;0_spec1,shallow_model&#39;0_spec,Assert14">
+      <goal name="vc_list_reversal_lasso.12.0.0.0.0" proved="true">
+      <proof prover="1" timelimit="0.02816"><result status="valid" time="0.028186" steps="443"/></proof>
+      </goal>
+     </transf>
      </goal>
      <goal name="vc_list_reversal_lasso.12.0.0.1" proved="true">
      <proof prover="2"><result status="valid" time="0.129765" steps="35671"/></proof>
@@ -318,12 +226,13 @@
    </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.12.1" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="3.640039" steps="29914"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,snoc,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;1,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Mod_sign_neg,Div_1,Mod_1,Div_inf,(==)&#39;spec,create&#39;spec&#39;0,empty&#39;def,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inner_spec,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;0,Assert18,Assert7,Assert4,H10,H4">
+    <goal name="vc_list_reversal_lasso.12.1.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.31527" memlimit="2000"><result status="valid" time="0.316375" steps="5473"/></proof>
+    </goal>
+   </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.12.2" expl="loop invariant" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="9817082"/></proof>
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="52172"/></proof>
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="641962"/></proof>
    <transf name="inline_goal" proved="true" >
     <goal name="vc_list_reversal_lasso.12.2.0" expl="loop invariant" proved="true">
     <transf name="split_all_full" proved="true" >
@@ -334,9 +243,6 @@
      <proof prover="2"><result status="valid" time="0.230872" steps="60151"/></proof>
      </goal>
      <goal name="vc_list_reversal_lasso.12.2.0.2" proved="true">
-     <proof prover="0"><result status="timeout" time="1.000000" steps="2417205"/></proof>
-     <proof prover="1"><result status="timeout" time="1.000000" steps="10762"/></proof>
-     <proof prover="2"><result status="timeout" time="1.000000" steps="214458"/></proof>
      <transf name="split_vc" proved="true" >
       <goal name="vc_list_reversal_lasso.12.2.0.2.0" proved="true">
       <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.046999" steps="9229"/></proof>
@@ -353,34 +259,58 @@
   </transf>
   </goal>
   <goal name="vc_list_reversal_lasso.13" expl="loop invariant" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="2690227"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="8793"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="211519"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.13.0" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.519904" steps="12367"/></proof>
+   <transf name="inline_goal" proved="true" >
+    <goal name="vc_list_reversal_lasso.13.0.0" expl="loop invariant" proved="true">
+    <transf name="split_all_full" proved="true" >
+     <goal name="vc_list_reversal_lasso.13.0.0.0" proved="true">
+     <proof prover="1"><result status="valid" time="0.046121" steps="683"/></proof>
+     </goal>
+     <goal name="vc_list_reversal_lasso.13.0.0.1" proved="true">
+     <proof prover="3"><result status="valid" time="0.420334" steps="83508"/></proof>
+     </goal>
+     <goal name="vc_list_reversal_lasso.13.0.0.2" proved="true">
+     <proof prover="1"><result status="valid" time="0.069163" steps="1173"/></proof>
+     </goal>
+     <goal name="vc_list_reversal_lasso.13.0.0.3" proved="true">
+     <proof prover="2"><result status="valid" time="0.710538" steps="154593"/></proof>
+     </goal>
+    </transf>
+    </goal>
+   </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.13.1" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.229106" steps="10855"/></proof>
+   <proof prover="1"><result status="valid" time="0.610102" steps="10855"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),(++),get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,(==)&#39;spec&#39;0,snoc&#39;spec,snoc&#39;spec&#39;0,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,inner_spec,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;1,inv&#39;0,Assert12,Assert7,Assert15">
+    <goal name="vc_list_reversal_lasso.13.1.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.266202"><result status="valid" time="0.261099" steps="4672"/></proof>
+    </goal>
+   </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.13.2" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.617694" steps="15894"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;2,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,snoc&#39;spec,snoc&#39;spec&#39;0,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;1,inv&#39;0,Assert18,Assert14,Assert12,Assert9,Assert8,Assert7,Assert6,Assert5,Assert4,Assert3,Assert2,Assert1,Assert,Assert16,H6,H4,H15,H11,H3,H2">
+    <goal name="vc_list_reversal_lasso.13.2.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.092563"><result status="valid" time="0.091017" steps="1673"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>
   <goal name="vc_list_reversal_lasso.14" expl="loop invariant" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="2640458"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="9517"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="248681"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.14.0" expl="loop invariant" proved="true">
    <proof prover="1"><result status="valid" time="0.528542" steps="4590"/></proof>
    </goal>
    <goal name="vc_list_reversal_lasso.14.1" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="2.082820" steps="17515"/></proof>
+   <proof prover="3"><result status="valid" time="0.510933" steps="77148"/></proof>
    </goal>
    <goal name="vc_list_reversal_lasso.14.2" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.895103" steps="17720"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,singleton,cons,snoc,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,in_bounds,memory_0,invariant&#39;3,invariant&#39;2,invariant&#39;1,invariant&#39;0,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,(==)&#39;spec,(==)&#39;spec&#39;0,empty&#39;def,set&#39;spec,set&#39;spec&#39;0,set&#39;spec&#39;1,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,singleton&#39;spec&#39;0,cons&#39;spec,cons&#39;spec&#39;0,cons&#39;spec&#39;1,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,inv&#39;3,inv&#39;1,inv&#39;0,Assert21,Assert17,Assert10,Assert7,Assert3,H13,Assert20,Assert19,Assert18,H5,H3,H14,H12,H11,H10,H4,H2,H1,Assert2,Assert1,Assert">
+    <goal name="vc_list_reversal_lasso.14.2.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.187113"><result status="valid" time="0.189428" steps="2659"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>
@@ -390,14 +320,6 @@
  </transf>
  </goal>
 </theory>
-<theory name="Core_Option_Option_Type" proved="true">
- <goal name="vc_none" proved="true">
- <proof prover="2"><result status="valid" time="0.006672" steps="27"/></proof>
- </goal>
- <goal name="vc_some" proved="true">
- <proof prover="2"><result status="valid" time="0.004238" steps="27"/></proof>
- </goal>
-</theory>
 <theory name="ListReversalLasso_Impl4_FindPtrInSeq_Impl" proved="true">
  <goal name="vc_find_ptr_in_seq" proved="true">
  <proof prover="2"><result status="valid" time="0.029070" steps="8450"/></proof>
@@ -410,9 +332,6 @@
 </theory>
 <theory name="ListReversalLasso_Impl4_FindLassoAux_Impl" proved="true">
  <goal name="vc_find_lasso_aux" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="3029666"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="8072"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="130948"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_find_lasso_aux.0" proved="true">
   <proof prover="2"><result status="valid" time="0.032432" steps="10396"/></proof>
diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
index a4565a20d7..87af96d21a 100644
Binary files a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz and b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz differ