[523] % z3release small.smt2
unsat
[524] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 318
m().get_sort(m_r) == m().get_sort(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[525] % 
[525] % cat small.smt2
(set-option :rewriter.mul_to_power true)
(assert (= (- (- 3 (- 1))) 3))
(check-sat)
[526] %