On the following formula Z3 throws an assertion violation
(set-logic QF_NIA)
(declare-fun x () Int)
(assert (not (= (div 1 x) (div (div 1 x) x))))
(assert (>= x 0))
(assert (<= x 7))
(check-sat)
ASSERTION VIOLATION
File: ../src/util/parray.h
Line: 587
c->m_size == r_sz
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Revision: ba03d99