diff --git a/creusot/tests/should_succeed/hillel/why3session.xml b/creusot/tests/should_succeed/hillel/why3session.xml
index 20b33c6b6b..21babf678c 100644
--- a/creusot/tests/should_succeed/hillel/why3session.xml
+++ b/creusot/tests/should_succeed/hillel/why3session.xml
@@ -126,10 +126,9 @@
   </transf>
   </goal>
   <goal name="insert_unique&#39;vc.31" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.400835" steps="1965011"/></proof>
   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,uint64&#39;maxInt,uint64&#39;minInt,max_uint64,length,radix,to_int,min_unsigned,in_bounds,singleton,cons,(++),id,shallow_model5,mAX&#39;,deep_model3,deep_model2,resolve10,completed,index_logic2,shallow_model1,produces,produces_trans,produces_refl,into_iter_post,into_iter_pre,shallow_model,is_unique,index_logic,subset_push,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,to_int_in_bounds,extensionality,zero_unsigned_is_zero,(==)&#39;spec,(==)&#39;spec&#39;0,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,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,new_spec,slice&#39;invariant,slice_ext,some_0&#39;def,inv_trivial15,inv_trivial14,inv_trivial13,inv_trivial12,shallow_model_spec1,inv_trivial11,inv_trivial10,inv_trivial9,shallow_model_spec,inv_trivial7,inv_trivial6,inv_trivial5,inv_trivial4,to_ref_seq_spec,produces_trans_spec,produces_refl_spec,inv_trivial3,inv_trivial2,inv_trivial1,inv_trivial,subset_push_spec,Requires2,Requires1,Requires,H9,Assume5,H8,Assert2,Assume4,Ensures8,Ensures7,Assert1,Assume3,Ensures6,Ensures5,Ensures4,H7,Assume2,H6,Assert,Assume1,H4,H3,H5,H2,Ensures3,H1,Ensures2,Ensures1,Assume,Ensures">
    <goal name="insert_unique&#39;vc.31.0" expl="postcondition" proved="true">
-   <proof prover="2" timelimit="0.022369"><result status="valid" time="0.022435" steps="85164"/></proof>
+   <proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="0.733887" steps="24210"/></proof>
    </goal>
   </transf>
   </goal>