mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
parent
5942dc24bd
commit
41b1f47d77
|
@ -576,14 +576,13 @@ namespace q {
|
|||
|
||||
void ematch::add(quantifier* _q) {
|
||||
TRACE("q", tout << "add " << mk_pp(_q, m) << "\n");
|
||||
clause* c = clausify(_q);
|
||||
scoped_ptr<clause> c = clausify(_q);
|
||||
quantifier* q = c->q();
|
||||
if (m_q2clauses.contains(q)) {
|
||||
dealloc(c);
|
||||
return;
|
||||
}
|
||||
ensure_ground_enodes(*c);
|
||||
m_clauses.push_back(c);
|
||||
m_clauses.push_back(c.detach());
|
||||
m_q2clauses.insert(q, c->index());
|
||||
ctx.push(pop_clause(*this));
|
||||
init_watch(*c);
|
||||
|
|
|
@ -1648,6 +1648,7 @@ public:
|
|||
break;
|
||||
}
|
||||
|
||||
|
||||
switch (check_nla()) {
|
||||
case FC_DONE:
|
||||
break;
|
||||
|
|
Loading…
Reference in a new issue