[cfe-dev] [analyzer][z3] Limit Z3 without timeouts

[Nuno Lopes via cfe-dev]

There's a caveat to Z3's resource limit option: it counts operations done across very different algorithms, so an rlimit may be not super correlated with running time for some inputs.
For example, on some input, the rlimit may be triggered during preprocessing, ending the solver early. With another input, it reaches the SAT solver so it has a different meaning and run-time characteristics. I don't know if clang is using quantifiers, but in that case it's even worse (though you can use 'smt.mbqi.max_iterations' instead).

So while it's true that rlimit gives a deterministic running time, it offers poor behavior across queries. A first query may timeout after 10 seconds, and the second only after 1 minute.

BTW, using Z3's memory limit is a no-no. Z3 can't recover from the state where memory limit is hit. The alternative is to use a "soft" limit (deterministic though): memory_high_watermark. This soft limit also helps taming the running time.

Nuno


From: Balázs Benics
Sent: 19 August 2020 18:10
To: cfe-dev <cfe-dev at lists.llvm.org>
Subject: [cfe-dev] [analyzer][z3] Limit Z3 without timeouts

SMT solvers are actively used not only for bugreport refutation but also for substituting the range based constraint manager.
IMO it would be valuable to limit the solver to prevent it from spending too much time on evaluating the given constraint set.

Using timeouts are not really deterministic, so its a no-go.
Using a counter-like limit would be the best approach.

Fortunately, Z3 has an `rlimit` option, which does exactly this.

This `rlimit` option is not really well documented, but here is the information that I have:
 - https://github.com/Z3Prover/z3/blob/73d73e6c953dd0d63d76c1dca7f88bc04ccf4565/src/opt/opt_params.pyg#L11
 - https://stackoverflow.com/a/45458651

Other solvers might not have such parameter, so we have to make a decision here how to integrate into our SMTAPI in a nonintrusive way.

Regards,
Balazs