mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
parent
77e7dcb3c3
commit
db3d6d7c95
|
@ -181,9 +181,10 @@ namespace datalog {
|
|||
|
||||
|
||||
rule_set * mk_elim_term_ite::operator()(rule_set const & source) {
|
||||
if (!m_ctx.elim_term_ite ()) {return nullptr;}
|
||||
if (!m_ctx.elim_term_ite ())
|
||||
return nullptr;
|
||||
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
|
||||
rules->inherit_predicates(source);
|
||||
bool change = false;
|
||||
for (auto *rule : source) {
|
||||
|
@ -194,10 +195,9 @@ namespace datalog {
|
|||
change |= elim(*rule, *rules);
|
||||
}
|
||||
if (!change) {
|
||||
dealloc(rules);
|
||||
rules = nullptr;
|
||||
}
|
||||
return rules;
|
||||
return rules.detach();
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue