Hi,
For this formula:
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (distinct a b))
(check-sat-using psmt)
Z3 throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 277
e_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Commit: 2882a67
Hi,
For this formula:
Z3 throws out an assertion violation:
OS: Ubuntu 18.04
Commit: 2882a67