(declare-fun s () (Set Int))
(declare-fun t () (Set Int))
(assert (= (card (union s t)) 2))
(assert (= (card s) 1))
(check-sat)
[639] % z3 small.smt2
sat
[640] % z3 smt.threads=2 small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 1224
l != true_literal && l != false_literal
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 1224
l != true_literal && l != false_literal
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
s
Segmentation fault
[641] %
[641] % cat small.smt2
(declare-fun s () (Set Int))
(declare-fun t () (Set Int))
(assert (= (card (union s t)) 2))
(assert (= (card s) 1))
(check-sat)
Hi,
For this formula:
Z3 throws out an assertion violation:
OS: Ubuntu 18.04
Commit: f447292