Z3 smt.arith.solver=1 or smt.arith.solver=3 assertion violation in ../src/smt/smt_theory.h line 64 or ../src/smt/smt_internalizer.cpp line 853

[muchang]

Hi,
For this formula:

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () (Set Int))
(assert (= (card c) (- a b)))
(assert (>= a b))
(check-sat)

Z3 smt.arith.solver=1 throws out:

ASSERTION VIOLATION
File: ../src/smt/smt_theory.h
Line: 64
!is_attached_to_var(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Z3 smt.arith.solver=3 throws out:

ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 853
!b_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 7b0327d