[602] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/muz/spacer/spacer_util.cpp
Line: 430
!m.is_false(a)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[603] % z3release small.smt2
Unexpected expression: false
ASSERTION VIOLATION
File: ../src/muz/spacer/spacer_util.cpp
Line: 529
UNREACHABLE CODE WAS REACHED.
Z3 4.8.8.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[604] % 
[604] % cat small.smt2
(set-logic HORN)
(set-option :rewriter.elim_ite false)
(assert (forall ((a Int) (b Int)) (= (ite (= b 0) 0 1) (ite (= a 0) 0 2))))
(check-sat)
[605] %