Hi,
For this formula,
(declare-datatypes ((A 0)) (((b (c A)) (d))))
(declare-fun f () A)
(assert (exists ((e A)) (distinct f (b e))))
(check-sat-using qe-sat)
z3 throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/smt/theory_datatype.cpp
Line: 758
d->m_constructor
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Revision: 5dc8c93
Hi,
For this formula,
z3 throws out an assertion violation:
OS: Ubuntu 18.04
Revision: 5dc8c93