Inconsistent effect of setting rlimit

[parno]

In the code below, if we run Boogie with /proverOpt:O:smt.qi.eager_threshold=100 /rlimit:5, the verification of test1 fails with an out-of-resource error. However, if we comment out the test0 procedure, then test1 succeeds.

The underlying issue appears to be that Boogie emits a push operation before setting the (large) rlimit for test1. According to Nikolaj, however, Z3 does enough work in a push that it exhausts the resource limit before it reaches the point of setting the larger rlimit.

I think the fix would be to move the if case here: https://github.com/boogie-org/boogie/blob/1a18c9c956249098f6a6a9fc7830e88ebed1aa0d/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs#L559 two lines earlier (so that it precedes the call SendThisVC("(push 1)");).

Does anyone anticipate issues with this change?

function f(i:int, j:int) returns (int)
{
    if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)
}

procedure test0(x:int)      // Causes test1 to fail when run with /rlimit:5
{
    assert(x - x == 0);
}

procedure {:rlimit 100000000} test1()
{
    assert(f(13,5) == 0);
}

[parno]

FWIW, it looks like F* handles rlimit via something like this:

(set-option :rlimit 16339680)
(check-sat)
(set-option :rlimit 0)

which was apparently in response to a similar issue (see https://github.com/FStarLang/FStar/commit/ad1054a7bc6e8838e3788cd88d0297111c8ac213)

[shazqadeer]

I like the F* solution. It is what the user would expect when she provides a resource bound for a particular procedure, i.e., the bound should apply only to the checking of that procedure.

@parno : If you are satisfied with the F* solution, would you like to take a shot at updating your PR?

[parno]

Sure, I can give it a whirl. Would you suggest doing it immediately after the CheckSat; i.e., after this line https://github.com/boogie-org/boogie/blob/ca31fcb2636de4c1582236a8cdf42a799f0b1cae/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs#L589, or as part of Reset here: https://github.com/boogie-org/boogie/blob/ca31fcb2636de4c1582236a8cdf42a799f0b1cae/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs#L609? The latter seems more semantically appropriate. The former matches F*'s approach.

[parno]

Also, is the test suite known to be in a passing state? On a fresh checkout of bced465a1989df30004, when I run lit, I get:

Failing Tests (11):
    Boogie :: aitest9/TestIntervals.bpl
    Boogie :: floats/issue110.bpl
    Boogie :: livevars/bla1.bpl
    Boogie :: livevars/stack_overflow.bpl
    Boogie :: sequences/intseq.bpl
    Boogie :: sequences/intseq_datatype.bpl
    Boogie :: test15/CaptureInlineUnroll.bpl
    Boogie :: test15/CaptureState.bpl
    Boogie :: test15/IntInModel.bpl
    Boogie :: test15/ModelTest.bpl
    Boogie :: test15/NullInModel.bpl

  Expected Passes    : 482
  Expected Failures  : 3
  Unsupported Tests  : 13
  Unexpected Failures: 11

For example, test15/IntInModel.bpl fails because of differences in the model returned:

--- /Users/parno/git/boogie/Test/test15/IntInModel.bpl.expect   2021-02-04 10:02:24.000000000 -0500
+++ /Users/parno/git/boogie/Test/test15/Output/IntInModel.bpl.tmp   2021-03-31 11:06:40.000000000 -0400
@@ -4,14 +4,11 @@
 *** MODEL
 i -> 0
 ControlFlow -> {
-  0 0 -> 51
   0 25 -> (- 52)
   0 51 -> 25
-  else -> (- 52)
+  else -> 51
 }
 tickleBool -> {
-  false -> true
-  true -> true
   else -> true
 }
 *** END_MODEL

Perhaps this is based on Z3 version? I'm using 4.8.5. The testing documentation (https://raw.githubusercontent.com/boogie-org/boogie/master/Test/README.md) has a "" for the expected Z3 version number.

[parno]

I'd like to make sure I have a good baseline before I start tampering with things.

[bkragl]

The test suite assumes Z3 version 4.8.8.

https://github.com/boogie-org/boogie/blob/ca31fcb2636de4c1582236a8cdf42a799f0b1cae/.github/workflows/test.yml#L14

[parno]

Cool, thanks for the tip. Pointing Boogie at 4.8.8 did the trick. Now all of the expected tests are succeeding.

[parno]

In #367, I went with adjusting the rlimit back to 0 during a prover reset. It seems to address the issue I ran into, and the existing unit tests all seem happy.