Adjusting Rlimitouts0 test for more efficient Z3.

boogie-org · Dec 31, 2019 · 8385b53 · 8385b53
1 parent 262f43b
commit 8385b53
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl
@@ -34,7 +34,7 @@ procedure TestRlimit1(in: [int]int, len: int) returns (out: [int]int);
   requires 0 < len;
   ensures (forall j: int :: 0 <= j && j < len ==> out[j] == in[j]);
 
-implementation {:rlimit 60000} TestRlimit1(in: [int]int, len: int) returns (out: [int]int)
+implementation {:rlimit 6000000} TestRlimit1(in: [int]int, len: int) returns (out: [int]int)
 {
     var i : int;