diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml
index 047a17ba5d..5841a8d79d 100644
--- a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml
+++ b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml
@@ -2,7 +2,6 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -24,7 +23,7 @@
     <proof prover="1"><result status="valid" time="0.137914" steps="123624"/></proof>
     </goal>
     <goal name="vc_produces_trans.0.0.1" proved="true">
-    <proof prover="0"><result status="valid" time="0.368971" steps="74078"/></proof>
+    <proof prover="1" timelimit="5"><result status="valid" time="0.102708" steps="573625"/></proof>
     </goal>
     <goal name="vc_produces_trans.0.0.2" proved="true">
     <proof prover="1"><result status="valid" time="0.126535" steps="573628"/></proof>