diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
index 195361cfd..8c993f068 100644
--- a/Source/VCGeneration/Checker.cs
+++ b/Source/VCGeneration/Checker.cs
@@ -327,10 +327,6 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.
       this.handler = handler;
 
       await thmProver.Reset(gen);
-      if (0 < rlimit)
-      {
-        timeout = 0;
-      }
       SetTimeout(timeout);
       SetRlimit(rlimit);
 
diff --git a/Test/prover/timelimit-and-rlimit.bpl b/Test/prover/timelimit-and-rlimit.bpl
new file mode 100644
index 000000000..a74e21629
--- /dev/null
+++ b/Test/prover/timelimit-and-rlimit.bpl
@@ -0,0 +1,10 @@
+// RUN: %boogie /proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
+// CHECK: (set-option :timeout 1000)
+// CHECK: (set-option :rlimit 10000)
+procedure
+{:timeLimit 1}
+{:rlimit 10000}
+P1(a: int, b: int) {
+  assert (a + b) - (a * b) == (b + a) - (a * b);
+}
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);