[782] % z3release small.smt2
sat
[783] % z3release rewriter.eq2ineq=true small.smt2
unsat
[784] % 
[784] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= (* a b) 4293001441))
(check-sat)
[785] %