<div dir="ltr">SMT solvers are actively used not only for bugreport refutation but also for substituting the range based constraint manager.<br>IMO it would be valuable to limit the solver to prevent it from spending too much time on evaluating the given constraint set.<br><br>Using timeouts are not really deterministic, so its a no-go.<br>Using a counter-like limit would be the best approach.<br><br>Fortunately, Z3 has an `rlimit` option, which does exactly this.<br><br>This `rlimit` option is not really well documented, but here is the information that I have:<br> - <a href="https://github.com/Z3Prover/z3/blob/73d73e6c953dd0d63d76c1dca7f88bc04ccf4565/src/opt/opt_params.pyg#L11">'rlimit', UINT, 0, 'resource limit (0 means no limit)</a><br> - <a href="https://stackoverflow.com/a/45458651">[...] as long as you keep using the same binary, it is deterministic.</a><br><br>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.<br><br>Regards,<br>Balazs</div>