mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
6e47499e26
commit
38176256c4
|
@ -322,18 +322,19 @@ namespace datalog {
|
|||
if (!m_ctx.array_blast ()) {
|
||||
return nullptr;
|
||||
}
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
|
||||
rules->inherit_predicates(source);
|
||||
rule_set::iterator it = source.begin(), end = source.end();
|
||||
bool change = false;
|
||||
for (; !m_ctx.canceled() && it != end; ++it) {
|
||||
change = blast(**it, *rules) || change;
|
||||
for (rule* r : source) {
|
||||
if (m_ctx.canceled())
|
||||
return nullptr;
|
||||
change = blast(*r, *rules) || change;
|
||||
}
|
||||
if (!change) {
|
||||
dealloc(rules);
|
||||
rules = nullptr;
|
||||
}
|
||||
return rules;
|
||||
return rules.detach();
|
||||
}
|
||||
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue