Hi,
For this formula:
(set-option :smt.core.minimize true)
(set-option :fp.xform.inline_eager false)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(declare-fun R (Int) Bool)
(assert (and (distinct P Q) (= P R)))
(check-sat-using horn)
Z3 throws out a segmentation fault:
[506] % z3 small.smt2
Segmentation fault
[507] %
[507] % cat small.smt2
(set-option :smt.core.minimize true)
(set-option :fp.xform.inline_eager false)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(declare-fun R (Int) Bool)
(assert (and (distinct P Q) (= P R)))
(check-sat-using horn)
[508] %
OS: Ubuntu 18.04
Commit: 3313590
Hi,
For this formula:
Z3 throws out a segmentation fault:
OS: Ubuntu 18.04
Commit: 3313590