mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix #4117
This commit is contained in:
parent
382bd05d1b
commit
7c226f40df
|
@ -431,8 +431,7 @@ class implicant_picker {
|
|||
|
||||
expr *na = nullptr, *f1 = nullptr, *f2 = nullptr, *f3 = nullptr;
|
||||
|
||||
SASSERT(!m.is_false(a));
|
||||
if (m.is_true(a)) {
|
||||
if (m.is_true(a)|| m.is_false(a)) {
|
||||
// noop
|
||||
} else if (a->get_family_id() != m.get_basic_family_id()) {
|
||||
add_literal(a, out);
|
||||
|
|
Loading…
Reference in a new issue