[585] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 310
st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[586] % 
[586] % cat small.smt2
(declare-fun a () (Array Int Real))
(assert (distinct a ((as const (Array Int Real)) 0)))
(check-sat)
[587] %