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

Bal√°zs Benics via cfe-dev cfe-dev at lists.llvm.org
Wed Aug 19 10:09:31 PDT 2020


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>


More information about the cfe-dev mailing list