mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #5862
This commit is contained in:
parent
11030fc81d
commit
c2f1bdc099
|
@ -133,9 +133,11 @@ namespace datalog {
|
|||
if (engine.get_fact(pred).is_reachable())
|
||||
should_keep = true;
|
||||
else if (m_context.get_model_converter()) {
|
||||
for (rule* pr : source.get_predicate_rules(pred))
|
||||
for (rule* pr : source.get_predicate_rules(pred))
|
||||
for (unsigned i = 0; i < pr->get_uninterpreted_tail_size(); ++i)
|
||||
should_keep |= pr->get_tail(i)->get_decl() != pred;
|
||||
if (pr->get_tail(i)->get_decl() != pred)
|
||||
// don't try to eliminate across predicates
|
||||
return nullptr;
|
||||
}
|
||||
else
|
||||
continue;
|
||||
|
|
Loading…
Reference in a new issue