Slow performance on simple inequality

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
```