[619] % z3release small.smt2
sat
[620] % z3release smt.arith.solver=2 small.smt2
sat
[621] % z3release rewriter.flat=false smt.arith.solver=2 small.smt2
unsat
[622] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (< a (- 1)))
(assert (< b 0))
(assert (distinct (* (* a b) b) a))
(check-sat)
[623] %