diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl
index 8e7efe0cd..7a5e011f2 100644
--- a/Test/test2/Rlimitouts0.bpl
+++ b/Test/test2/Rlimitouts0.bpl
@@ -1,7 +1,7 @@
 // We use boogie here because parallel-boogie doesn't work well with -proverLog
 // RUN: %boogie -rlimit:800000 -proverLog:"%t.smt2" "%s"
 // RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
-// CHECK-L: (set-option :timeout 0)
+// CHECK-L: (set-option :timeout 4000)
 // CHECK-L: (set-option :rlimit 800000)
 // CHECK-L: (set-option :timeout 0)
 // CHECK-L: (set-option :rlimit 900000)
@@ -11,7 +11,7 @@
 // Depends on all output going to a single file, so incompatible with
 // batch mode.
 // UNSUPPORTED: batch_mode
-procedure {:timeLimit 4} /* timeLimit overridden by rlimit */ TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
+procedure {:timeLimit 4} TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
   requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
   requires 0 < len;
   ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);