[507] % z3 small.smt2
Failed to verify: a.is_numeral(val, r)
ASSERTION VIOLATION
File: ../src/muz/spacer/spacer_qe_project.cpp
Line: 495
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[508] % z3release small.smt2
Failed to verify: a.is_numeral(val, r)
Segmentation fault
[509] % z3san small.smt2
Failed to verify: a.is_numeral(val, r)
*** stack smashing detected ***: <unknown> terminated
Aborted
[510] % 
[510] % cat small.smt2
(set-logic HORN)
(set-option :fp.spacer.native_mbp false)
(set-option :fp.spacer.reach_dnf false)
(declare-fun a () Bool)
(assert (forall ((b Int) (c Int)) (= b c 0)))
(assert (not a))
(check-sat)
[511] %