Slow performance on simple inequality

[r0ayane]

Hi, z3 runs slowly on this instance:

$ cat slow.smt2
(declare-fun i0 () Int)
(assert (<= 1 (- i0 (* 32 32 32 i0 i0 i0 i0))))
(check-sat)
$ timeout -s 9 30 z3 slow.smt2
Killed

while cvc5 can solve it immediately.

$ time cvc5 slow.smt2
unsat

real    0m0.018s
user    0m0.014s
sys     0m0.005s

[NikolajBjorner]

It is a general issue with the qfnia tactic. It uses a SAT solver to check for small models, but this solver may take all resources.
It is not obvious the SAT solver should run first (or at all). I am setting a max-conflict on this to throttle it.
It is generally observed that the SAT tactic can even be removed and the solver then handles more qfnia benchmarks.
Fine tuning and experimentation with how to optimize tactic use or harness the SAT backend is more effort than adding this throttle.