Allow both timeLimit and rlimit together (#864)

Sometimes we want to set a resource limit _and_ a time limit, where the
goal of the former is to have deterministic bounds but the goal of the
latter is to ensure timely CI completion. In this case, a good value for
the time limit should be much larger than the time we would expect to be
required to exceed the resource limit. This will ensure that execution
is usually deterministic, but in the rare case where resource count and
time are far from each other it'll still guarantee reasonable
termination.

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);
 

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);
+}

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);