From 8385b53a388f4c885bc84d6b4e39811dfbabf29b Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Tue, 31 Dec 2019 14:04:10 -0500 Subject: [PATCH] Adjusting Rlimitouts0 test for more efficient Z3. --- Test/test2/Rlimitouts0.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl index c48fe2c3d..b6934e8fd 100644 --- 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;