Skip to content

Commit

Permalink
Allow both timeLimit and rlimit together
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
atomb committed Apr 8, 2024
1 parent db550f9 commit df9599b
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 4 deletions.
4 changes: 0 additions & 4 deletions Source/VCGeneration/Checker.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
10 changes: 10 additions & 0 deletions Test/prover/timelimit-and-rlimit.bpl
Original file line number Diff line number Diff line change
@@ -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);
}

0 comments on commit df9599b

Please sign in to comment.