[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:

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

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