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

[Balázs Benics via cfe-dev]

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:
 - 'rlimit', UINT, 0, 'resource limit (0 means no limit)
<https://github.com/Z3Prover/z3/blob/73d73e6c953dd0d63d76c1dca7f88bc04ccf4565/src/opt/opt_params.pyg#L11>
 - [...] as long as you keep using the same binary, it is deterministic.
<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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200819/14452e87/attachment.html>