CODEWITHSUNDEEP
z3
stefan
stefan

Reputation: 1145

Z3 Performance with Non-Linear Arithmetic

We are running into performance problems with what I believe is the part of Z3 that treats non-linear arithmetic. Here is a simple concrete Boogie example, that when verified with Z3 (version 4.1) takes a long time (on the order of 3 minutes) to complete.

const D: int;
function f(n: int) returns (int) { n * D }

procedure test() returns ()
{
  var a, b, c: int;
  var M: [int]int;
  var t: int;

  assume 0 < a && 1000 * a < f(1);
  assume 0 < c && 1000 * c < f(1);
  assume f(100) * b == a * c;

  assert M[t] > 0;
}

It seems that the problem is caused by an interaction of functions, range assumption on integer variables as well as multiplications of (unknown) integer values. The assertion in the end should not be provable. Instead of failing quickly, it seems that Z3 has ways to instantiate lots of terms somehow, as its memory consumptions grows fairly quickly to about 300 MB, at which point it gives up.

I'm wondering if this is a bug, or whether it is possible to improve the heuristics on when Z3 should stop the search in the particular direction it is currently trying to solve the problem.

One interesting thing is that inlining the function by using

function {:inline} f(n: int) returns (int) { n * D }

makes the verification terminate very quickly.

Background: This is a minimal test case for a problem that we see in our verifier Chalice. There, the Boogie programs get much longer, potentially with multiple assumptions of a similar kind. Often, the verification does not appear to be terminating at all.

Any ideas?

Upvotes: 5

Views: 1223

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Yes, the non-termination is due to nonlinear integer arithmetic. Z3 has a new nonlinear solver, but it is for "nonlinear real arithmetic", and can only be used in quantifier free problems that only use arithmetic (i.e., no uninterpreted functions like in your example). Thus, the old arithmetic solver is used in your example. This solver has very limited support for integer arithmetic. Your analysis of the problem is correct. Z3 has trouble finding a solution for the block of nonlinear integer constraints. Note that if we replace f(100) * b == a * c with f(100) * b <= a * c, then Z3 returns immediately with an "unknown" answer.

We can avoid the non-termination by limiting the number of nonlinear arithmetic reasoning in Z3. The option NL_ARITH_ROUNDS=100 will use the nonlinear module at most 100 times for each Z3 query. This is not an ideal solution, but at least, we avoid the non-termination.

Upvotes: 3

Related Questions