Hi,
For this formula,
(declare-fun a (Int) Bool)
(declare-fun b () Int)
(assert (forall ((c Int)) (= (= b 0) (a c))))
(push)
(check-sat)
Z3 smt.arith.solver=1 throws out:
ASSERTION VIOLATION
File: ../src/smt/smt_setup.cpp
Line: 53
!m_context.already_internalized()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Revision: 7b0327d