Merge pull request #1132 from creusot-rs/filter-iter

Simple proof of Filter
creusot-rs · Sep 30, 2024 · 40965a6 · 40965a6
2 parents 99b0b77 + 7b0b80d
commit 40965a6
Show file tree

Hide file tree

Showing 454 changed files with 3,505 additions and 688 deletions.
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
@@ -34,7 +34,7 @@ use rustc_type_ir::{FloatTy, IntTy, UintTy};
 use std::fmt::Debug;
 use why3::{
     coma::{self, Arg, Defn, Expr, Param, Term},
-    declaration::{Attribute, Contract, Decl, Module, Signature},
+    declaration::{Attribute, Contract, Decl, Meta, MetaArg, MetaIdent, Module, Signature},
     exp::{Binder, Constant, Exp, Pattern},
     ty::Type,
     Ident, QName,
@@ -168,6 +168,10 @@ pub(crate) fn translate_function<'tcx, 'sess>(
     let decls = closure_generic_decls(ctx.tcx, def_id)
         .chain(clones)
         .chain(promoteds)
+        .chain([Decl::Meta(Meta {
+            name: MetaIdent::String("compute_max_steps".into()),
+            args: vec![MetaArg::Integer(1_000_000)],
+        })])
         .chain(std::iter::once(body))
         .collect();
 

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma b/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma
@@ -197,6 +197,8 @@ module M_01_resolve_unsoundness__make_vec_of_size
       (! return' {result}) ]
 
 
+  meta "compute_max_steps" 1000000
+
   let rec make_vec_of_size (n:usize) (return'  (ret:Vec'0.t_Vec bool (Global'0.t_Global)))= (! bb0
     [ bb0 = s0
       [ s0 = new'0 {[%#s01_resolve_unsoundness0] ()}

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml
@@ -24,21 +24,21 @@
   <proof prover="5"><result status="valid" time="0.013523" steps="14"/></proof>
   </goal>
   <goal name="vc_make_vec_of_size.4" expl="integer overflow">
-  <proof prover="0"><result status="timeout" time="5.000000" steps="304331"/></proof>
-  <proof prover="4"><result status="timeout" time="5.000000" steps="7355345"/></proof>
-  <proof prover="5"><result status="timeout" time="5.000000" steps="36565"/></proof>
-  <proof prover="6"><result status="timeout" time="5.000000" steps="315553"/></proof>
+  <proof prover="0"><result status="timeout" time="5.000000" steps="487601"/></proof>
+  <proof prover="4"><result status="timeout" time="5.000000" steps="23974168"/></proof>
+  <proof prover="5"><result status="timeout" time="5.000000" steps="82715"/></proof>
+  <proof prover="6"><result status="timeout" time="5.000000" steps="748825"/></proof>
   </goal>
   <goal name="vc_make_vec_of_size.5" expl="loop invariant">
   <transf name="split_vc" >
    <goal name="vc_make_vec_of_size.5.0" expl="loop invariant" proved="true">
    <proof prover="5"><result status="valid" time="0.013986" steps="15"/></proof>
    </goal>
    <goal name="vc_make_vec_of_size.5.1" expl="loop invariant">
-   <proof prover="0"><result status="timeout" time="5.000000" steps="304453"/></proof>
-   <proof prover="4"><result status="timeout" time="5.000000" steps="10257229"/></proof>
-   <proof prover="5"><result status="timeout" time="5.000000" steps="34064"/></proof>
-   <proof prover="6"><result status="timeout" time="5.000000" steps="315896"/></proof>
+   <proof prover="0"><result status="timeout" time="5.000000" steps="487685"/></proof>
+   <proof prover="4"><result status="timeout" time="5.000000" steps="31727244"/></proof>
+   <proof prover="5"><result status="timeout" time="5.000000" steps="81141"/></proof>
+   <proof prover="6"><result status="timeout" time="5.000000" steps="755508"/></proof>
    </goal>
   </transf>
   </goal>

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/222.coma b/creusot/tests/should_fail/bug/222.coma
@@ -127,6 +127,8 @@ module M_222__uses_invariant
       (! return' {result}) ]
 
 
+  meta "compute_max_steps" 1000000
+
   let rec uses_invariant (x:borrowed (Once'0.t_Once t)) (return'  (ret:()))= {[%#s2221] inv'1 x}
     {[%#s2220] invariant'0 x.current}
     (! bb0

diff --git a/creusot/tests/should_fail/bug/222/why3shapes.gz b/creusot/tests/should_fail/bug/222/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/492.coma b/creusot/tests/should_fail/bug/492.coma
@@ -44,6 +44,8 @@ module M_492__reborrow_tuple
 
   use prelude.prelude.Int
 
+  meta "compute_max_steps" 1000000
+
   let rec reborrow_tuple (x:borrowed t) (return'  (ret:(borrowed t, uint32)))= {[%#s4921] inv'1 x}
     (! bb0
     [ bb0 = s0
@@ -110,6 +112,8 @@ module M_492__test
       (! return' {result}) ]
 
 
+  meta "compute_max_steps" 1000000
+
   let rec test (_1:()) (return'  (ret:()))= (! bb0
     [ bb0 = s0
       [ s0 =  [ &x <- [%#s4920] (5 : int32) ] s1

diff --git a/creusot/tests/should_fail/bug/492/why3session.xml b/creusot/tests/should_fail/bug/492/why3session.xml
@@ -21,7 +21,7 @@
   </goal>
   <goal name="vc_test.1" expl="assertion">
   <proof prover="2"><result status="unknown" time="0.035416" steps="3366"/></proof>
-  <proof prover="3"><result status="timeout" time="5.000000" steps="6111302"/></proof>
+  <proof prover="3"><result status="timeout" time="5.000000" steps="9700833"/></proof>
   <proof prover="4"><result status="unknown" time="0.014231" steps="38"/></proof>
   <proof prover="5"><result status="unknown" time="0.011462" steps="1568"/></proof>
   </goal>

diff --git a/creusot/tests/should_fail/bug/492/why3shapes.gz b/creusot/tests/should_fail/bug/492/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/692.coma b/creusot/tests/should_fail/bug/692.coma
@@ -83,6 +83,8 @@ module M_692__incorrect
 
   predicate resolve'0 (_1 : b)
 
+  meta "compute_max_steps" 1000000
+
   let rec incorrect (cond:c) (branch:b) (return'  (ret:()))= {[%#s6922] inv'0 branch}
     {[%#s6921] inv'1 cond}
     {[%#s6920] precondition'0 cond ()
@@ -141,6 +143,8 @@ module M_692__valid_normal__qy123zclosureqy35z1qy125z
 
   use prelude.prelude.Intrinsic
 
+  meta "compute_max_steps" 1000000
+
   let rec m_692__valid_normal__qy123zclosureqy35z1qy125z (_1:Closure'0.m_692__valid_normal__qy123zclosureqy35z1qy125z) (return'  (ret:bool))= (! bb0
     [ bb0 = s0
       [ s0 = Closure'0.m_692__valid_normal__qy123zclosureqy35z1qy125z {_1}
@@ -208,6 +212,8 @@ module M_692__valid_normal__qy123zclosureqy35z2qy125z
   predicate resolve'0 (_1 : borrowed Closure'0.m_692__valid_normal__qy123zclosureqy35z2qy125z) =
     resolve'1 _1
 
+  meta "compute_max_steps" 1000000
+
   let rec m_692__valid_normal__qy123zclosureqy35z2qy125z (_1:borrowed Closure'0.m_692__valid_normal__qy123zclosureqy35z2qy125z) (b:bool) (return'  (ret:()))= (! bb0
     [ bb0 = any [ br0 -> {b = false} (! bb2) | br1 -> {b} (! bb1) ] 
     | bb1 = s0 [ s0 =  [ &_4 <- [%#s6920] (2 : uint32) ] s1 | s1 = bb3 ] 
@@ -296,6 +302,8 @@ module M_692__valid_normal
     /\ (exists b : bool . forall b0 : bool . postcondition'0 cond () b0  -> b0 = b))}
     any [ return' (result:())-> {[%#span6] false} (! return' {result}) ] 
 
+  meta "compute_max_steps" 1000000
+
   let rec valid_normal (n:uint32) (return'  (ret:uint32))= (! bb0
     [ bb0 = s0
       [ s0 =  [ &r <- [%#s6920] (0 : uint32) ] s1

diff --git a/creusot/tests/should_fail/bug/692/why3session.xml b/creusot/tests/should_fail/bug/692/why3session.xml
@@ -19,7 +19,7 @@
   </goal>
   <goal name="vc_incorrect.2">
   <proof prover="0"><result status="unknown" time="0.030652" steps="1893"/></proof>
-  <proof prover="4"><result status="timeout" time="5.000000" steps="6246267"/></proof>
+  <proof prover="4"><result status="timeout" time="5.000000" steps="8831165"/></proof>
   <proof prover="5" timelimit="5"><result status="unknown" time="0.012557" steps="111"/></proof>
   <proof prover="6"><result status="unknown" time="0.008014" steps="1297"/></proof>
   </goal>

diff --git a/creusot/tests/should_fail/bug/692/why3shapes.gz b/creusot/tests/should_fail/bug/692/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/695.coma b/creusot/tests/should_fail/bug/695.coma
@@ -131,6 +131,8 @@ module M_695__inversed_if
       (! return' {result}) ]
 
 
+  meta "compute_max_steps" 1000000
+
   let rec inversed_if (cond:c) (branch:b) (return'  (ret:()))= {[%#s6954] inv'1 branch}
     {[%#s6953] inv'0 cond}
     {[%#s6952] precondition'0 cond () /\ (forall b : bool . precondition'1 branch (b))}
@@ -208,6 +210,8 @@ module M_695__valid__qy123zclosureqy35z1qy125z
 
   use prelude.prelude.Intrinsic
 
+  meta "compute_max_steps" 1000000
+
   let rec m_695__valid__qy123zclosureqy35z1qy125z (_1:Closure'0.m_695__valid__qy123zclosureqy35z1qy125z) (return'  (ret:bool))= (! bb0
     [ bb0 = s0
       [ s0 = Closure'0.m_695__valid__qy123zclosureqy35z1qy125z {_1}
@@ -273,6 +277,8 @@ module M_695__valid__qy123zclosureqy35z2qy125z
   predicate resolve'0 (_1 : borrowed Closure'0.m_695__valid__qy123zclosureqy35z2qy125z) =
     resolve'1 _1
 
+  meta "compute_max_steps" 1000000
+
   let rec m_695__valid__qy123zclosureqy35z2qy125z (_1:borrowed Closure'0.m_695__valid__qy123zclosureqy35z2qy125z) (b:bool) (return'  (ret:()))= (! bb0
     [ bb0 = any [ br0 -> {b = false} (! bb2) | br1 -> {b} (! bb1) ] 
     | bb1 = s0 [ s0 =  [ &_4 <- [%#s6950] (2 : uint32) ] s1 | s1 = bb3 ] 
@@ -372,6 +378,8 @@ module M_695__valid
       (! return' {result}) ]
 
 
+  meta "compute_max_steps" 1000000
+
   let rec valid (n:uint32) (return'  (ret:uint32))= (! bb0
     [ bb0 = s0
       [ s0 =  [ &r <- [%#s6950] (0 : uint32) ] s1

diff --git a/creusot/tests/should_fail/bug/695/why3session.xml b/creusot/tests/should_fail/bug/695/why3session.xml
@@ -37,7 +37,7 @@
   </goal>
   <goal name="vc_valid.3">
   <proof prover="0"><result status="unknown" time="0.039270" steps="3567"/></proof>
-  <proof prover="4"><result status="timeout" time="5.000000" steps="5994809"/></proof>
+  <proof prover="4"><result status="timeout" time="5.000000" steps="7808861"/></proof>
   <proof prover="5"><result status="unknown" time="0.016470" steps="74"/></proof>
   <proof prover="6"><result status="unknown" time="0.022450" steps="2787"/></proof>
   </goal>

diff --git a/creusot/tests/should_fail/bug/695/why3shapes.gz b/creusot/tests/should_fail/bug/695/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/869.coma b/creusot/tests/should_fail/bug/869.coma
@@ -29,6 +29,8 @@ module M_869__unsound
 
   use prelude.prelude.Snapshot
 
+  meta "compute_max_steps" 1000000
+
   let rec unsound (_1:()) (return'  (ret:()))= (! bb0
     [ bb0 = s0 [ s0 =  [ &x <- [%#s8690] Snapshot.new true ] s1 | s1 = bb1 ] 
     | bb1 = s0

diff --git a/creusot/tests/should_fail/bug/869/why3session.xml b/creusot/tests/should_fail/bug/869/why3session.xml
@@ -20,7 +20,7 @@
    <proof prover="2"><result status="valid" time="0.015997" steps="909"/></proof>
    </goal>
    <goal name="vc_unsound.1.1" expl="assertion">
-   <proof prover="0"><result status="timeout" time="5.000000" steps="6177449"/></proof>
+   <proof prover="0"><result status="timeout" time="5.000000" steps="8893567"/></proof>
    <proof prover="1"><result status="unknown" time="0.041238" steps="2533"/></proof>
    <proof prover="2"><result status="unknown" time="0.009270" steps="1502"/></proof>
    <proof prover="4"><result status="unknown" time="0.051148" steps="714"/></proof>

diff --git a/creusot/tests/should_fail/bug/869/why3shapes.gz b/creusot/tests/should_fail/bug/869/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/specialize.coma b/creusot/tests/should_fail/bug/specialize.coma
@@ -118,6 +118,8 @@ module M_specialize__f
     [ return' (result:())-> {[%#span1] true} (! return' {result}) ]
 
 
+  meta "compute_max_steps" 1000000
+
   let rec f (v:Vec'0.t_Vec uint32 (Global'0.t_Global)) (return'  (ret:()))= (! bb0
     [ bb0 = s0 [ s0 = x'0 {v} (fun (_ret':()) ->  [ &_2 <- _ret' ] s1) | s1 = bb1 ] 
     | bb1 = s0 [ s0 = {[@expl:assertion] [%#sspecialize0] false} s1 | s1 = bb2 ] 
@@ -193,6 +195,8 @@ module M_specialize__g
   let rec x'0 (self:Vec'0.t_Vec t (Global'0.t_Global)) (return'  (ret:()))= {[@expl:precondition] [%#span7] inv'0 self}
     any [ return' (result:())-> (! return' {result}) ] 
 
+  meta "compute_max_steps" 1000000
+
   let rec g (v:Vec'0.t_Vec t (Global'0.t_Global)) (return'  (ret:()))= {[%#sspecialize1] inv'0 v}
     (! bb0
     [ bb0 = s0 [ s0 = x'0 {v} (fun (_ret':()) ->  [ &_2 <- _ret' ] s1) | s1 = bb1 ] 
@@ -267,6 +271,8 @@ module M_specialize__h
   let rec x'0 (self:Vec'0.t_Vec int32 (Global'0.t_Global)) (return'  (ret:()))= {[@expl:precondition] [%#span6] inv'0 self}
     any [ return' (result:())-> {[%#span7] false} (! return' {result}) ] 
 
+  meta "compute_max_steps" 1000000
+
   let rec h (v:Vec'0.t_Vec int32 (Global'0.t_Global)) (return'  (ret:()))= (! bb0
     [ bb0 = s0 [ s0 = x'0 {v} (fun (_ret':()) ->  [ &_2 <- _ret' ] s1) | s1 = bb1 ] 
     | bb1 = s0 [ s0 = {[@expl:assertion] [%#sspecialize0] false} s1 | s1 = bb2 ] 

diff --git a/creusot/tests/should_fail/bug/specialize/why3session.xml b/creusot/tests/should_fail/bug/specialize/why3session.xml
@@ -25,9 +25,9 @@
  <transf name="split_vc" >
   <goal name="vc_g.0">
   <proof prover="0"><result status="timeout" time="5.000000" steps="735447"/></proof>
-  <proof prover="5"><result status="timeout" time="5.000000" steps="3694936"/></proof>
-  <proof prover="6"><result status="timeout" time="5.000000" steps="58419"/></proof>
-  <proof prover="7"><result status="timeout" time="5.000000" steps="693885"/></proof>
+  <proof prover="5"><result status="timeout" time="5.000000" steps="3593656"/></proof>
+  <proof prover="6"><result status="timeout" time="5.000000" steps="60246"/></proof>
+  <proof prover="7"><result status="timeout" time="5.000000" steps="1006241"/></proof>
   </goal>
  </transf>
  </goal>

diff --git a/creusot/tests/should_fail/bug/specialize/why3shapes.gz b/creusot/tests/should_fail/bug/specialize/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/subregion.coma b/creusot/tests/should_fail/bug/subregion.coma
@@ -11,6 +11,8 @@ module M_subregion__list_reversal_h
 
   use prelude.prelude.Int
 
+  meta "compute_max_steps" 1000000
+
   let rec list_reversal_h (l:usize) (return'  (ret:usize))= (! bb0
     [ bb0 = s0 [ s0 =  [ &r <- [%#ssubregion0] (0 : usize) ] s1 | s1 = bb1 ] 
     | bb1 = bb1

diff --git a/creusot/tests/should_fail/bug/subregion/why3shapes.gz b/creusot/tests/should_fail/bug/subregion/why3shapes.gz
diff --git a/creusot/tests/should_fail/final_borrows.coma b/creusot/tests/should_fail/final_borrows.coma
@@ -30,6 +30,8 @@ module M_final_borrows__not_final_borrow
   predicate resolve'0 (_1 : borrowed t) =
     resolve'1 _1
 
+  meta "compute_max_steps" 1000000
+
   let rec not_final_borrow (bor:borrowed t) (return'  (ret:()))= {[%#sfinal_borrows1] inv'1 bor}
     (! bb0
     [ bb0 = s0
@@ -83,6 +85,8 @@ module M_final_borrows__store_changes_prophecy
   predicate resolve'0 (_1 : borrowed t) =
     resolve'1 _1
 
+  meta "compute_max_steps" 1000000
+
   let rec store_changes_prophecy (bor:borrowed t) (return'  (ret:()))= {[%#sfinal_borrows1] inv'1 bor}
     (! bb0
     [ bb0 = s0
@@ -134,6 +138,8 @@ module M_final_borrows__store_changes_prophecy_2
   predicate resolve'0 (_1 : borrowed t) =
     resolve'1 _1
 
+  meta "compute_max_steps" 1000000
+
   let rec store_changes_prophecy_2 (bor:borrowed t) (x:t) (return'  (ret:()))= {[%#sfinal_borrows2] inv'0 x}
     {[%#sfinal_borrows1] inv'1 bor}
     (! bb0
@@ -189,6 +195,8 @@ module M_final_borrows__call_changes_prophecy
 
   use prelude.prelude.Snapshot
 
+  meta "compute_max_steps" 1000000
+
   let rec call_changes_prophecy (bor:borrowed int32) (return'  (ret:()))= (! bb0
     [ bb0 = s0 [ s0 =  [ &bor_snap <- [%#sfinal_borrows0] Snapshot.new bor ] s1 | s1 = bb1 ] 
     | bb1 = s0
@@ -245,6 +253,8 @@ module M_final_borrows__unnesting_fails
 
   use prelude.prelude.Int
 
+  meta "compute_max_steps" 1000000
+
   let rec unnesting_fails (_1:()) (return'  (ret:()))= (! bb0
     [ bb0 = s0
       [ s0 =  [ &x <- [%#sfinal_borrows0] (0 : int32) ] s1
@@ -333,6 +343,8 @@ module M_final_borrows__move_place_without_deref
   predicate resolve'0 (_1 : borrowed t) =
     resolve'1 _1
 
+  meta "compute_max_steps" 1000000
+
   let rec move_place_without_deref (bor:borrowed t) (return'  (ret:()))= {[%#sfinal_borrows1] inv'2 bor}
     (! bb0
     [ bb0 = s0

diff --git a/creusot/tests/should_fail/final_borrows/why3session.xml b/creusot/tests/should_fail/final_borrows/why3session.xml
@@ -29,7 +29,7 @@
    <proof prover="0"><result status="valid" time="0.010891" steps="4293"/></proof>
    </goal>
    <goal name="vc_not_final_borrow.3.2" expl="assertion">
-   <proof prover="0"><result status="timeout" time="5.000000" steps="2735052"/></proof>
+   <proof prover="0"><result status="timeout" time="5.000000" steps="7348990"/></proof>
    <proof prover="1"><result status="unknown" time="0.027910" steps="1685"/></proof>
    <proof prover="2"><result status="unknown" time="0.005915" steps="1252"/></proof>
    <proof prover="4"><result status="unknown" time="0.007395" steps="87"/></proof>
@@ -54,7 +54,7 @@
    <proof prover="2"><result status="valid" time="0.011504" steps="756"/></proof>
    </goal>
    <goal name="vc_store_changes_prophecy.2.1" expl="assertion">
-   <proof prover="0"><result status="timeout" time="5.000000" steps="2751175"/></proof>
+   <proof prover="0"><result status="timeout" time="5.000000" steps="7910464"/></proof>
    <proof prover="1"><result status="unknown" time="0.029521" steps="1418"/></proof>
    <proof prover="2"><result status="unknown" time="0.008567" steps="1123"/></proof>
    <proof prover="4"><result status="unknown" time="0.010959" steps="51"/></proof>
@@ -66,7 +66,7 @@
 </theory>
 <theory name="M_final_borrows__store_changes_prophecy_2">
  <goal name="vc_store_changes_prophecy_2">
- <proof prover="0"><result status="timeout" time="5.000000" steps="3185037"/></proof>
+ <proof prover="0"><result status="timeout" time="5.000000" steps="7712784"/></proof>
  <proof prover="1"><result status="unknown" time="0.017817" steps="2905"/></proof>
  <proof prover="2"><result status="unknown" time="0.004995" steps="1567"/></proof>
  <proof prover="4"><result status="unknown" time="0.009799" steps="109"/></proof>
@@ -78,7 +78,7 @@
   <goal name="vc_call_changes_prophecy.0" expl="assertion">
   <transf name="split_vc" >
    <goal name="vc_call_changes_prophecy.0.0" expl="assertion">
-   <proof prover="0"><result status="timeout" time="5.000000" steps="2915024"/></proof>
+   <proof prover="0"><result status="timeout" time="5.000000" steps="6721519"/></proof>
    <proof prover="1"><result status="unknown" time="0.022459" steps="2372"/></proof>
    <proof prover="2"><result status="unknown" time="0.008814" steps="1466"/></proof>
    <proof prover="4"><result status="unknown" time="0.012454" steps="59"/></proof>
@@ -100,7 +100,7 @@
    <proof prover="2"><result status="valid" time="0.023494" steps="843"/></proof>
    </goal>
    <goal name="vc_unnesting_fails.0.2" expl="assertion">
-   <proof prover="0"><result status="timeout" time="5.000000" steps="3522266"/></proof>
+   <proof prover="0"><result status="timeout" time="5.000000" steps="7278249"/></proof>
    <proof prover="1"><result status="unknown" time="0.038009" steps="3058"/></proof>
    <proof prover="2"><result status="unknown" time="0.020797" steps="1639"/></proof>
    <proof prover="4"><result status="unknown" time="0.020193" steps="32"/></proof>
@@ -120,7 +120,7 @@
   <proof prover="4"><result status="valid" time="0.007544" steps="13"/></proof>
   </goal>
   <goal name="vc_move_place_without_deref.2" expl="assertion">
-  <proof prover="0"><result status="timeout" time="5.000000" steps="2706710"/></proof>
+  <proof prover="0"><result status="timeout" time="5.000000" steps="7925399"/></proof>
   <proof prover="1"><result status="unknown" time="0.024991" steps="1457"/></proof>
   <proof prover="2"><result status="unknown" time="0.007906" steps="1247"/></proof>
   <proof prover="4"><result status="unknown" time="0.008239" steps="35"/></proof>

diff --git a/creusot/tests/should_fail/final_borrows/why3shapes.gz b/creusot/tests/should_fail/final_borrows/why3shapes.gz
diff --git a/creusot/tests/should_fail/opaque_unproveable.coma b/creusot/tests/should_fail/opaque_unproveable.coma
@@ -6,6 +6,8 @@ module M_opaque_unproveable__test
 
   predicate opaque'0 [#"../opaque_unproveable.rs" 9 4 9 27] (_1 : ())
 
+  meta "compute_max_steps" 1000000
+
   let rec test (_1:()) (return'  (ret:()))= (! bb0
     [ bb0 = s0 [ s0 = {[@expl:assertion] [%#sopaque_unproveable0] opaque'0 ()} s1 | s1 = return' {_0} ]  ]
     ) [ & _0 : () = any_l () ]  [ return' (result:())-> (! return' {result}) ] 

diff --git a/creusot/tests/should_fail/opaque_unproveable/why3shapes.gz b/creusot/tests/should_fail/opaque_unproveable/why3shapes.gz
diff --git a/creusot/tests/should_fail/traits/17_impl_refinement.coma b/creusot/tests/should_fail/traits/17_impl_refinement.coma
@@ -14,6 +14,8 @@ module M_17_impl_refinement__qyi14398438181735515246__my_function
 
   use prelude.prelude.Int
 
+  meta "compute_max_steps" 1000000
+
   let rec my_function (self:()) (return'  (ret:usize))= {[%#s17_impl_refinement1] true}
     (! bb0 [ bb0 = s0 [ s0 =  [ &_0 <- [%#s17_impl_refinement0] (20 : usize) ] s1 | s1 = return' {_0} ]  ] )
     [ & _0 : usize = any_l () ]

diff --git a/creusot/tests/should_fail/traits/17_impl_refinement/why3shapes.gz b/creusot/tests/should_fail/traits/17_impl_refinement/why3shapes.gz