mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

delay detach

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-15 12:41:34 -07:00
parent 891ab8bac5
commit cafe3acff1
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/q_ematch.cpp
View file

@ -578,11 +578,10 @@ namespace q {
TRACE("q", tout << "add " << mk_pp(_q, m) << "\n"); TRACE("q", tout << "add " << mk_pp(_q, m) << "\n");
scoped_ptr<clause> c = clausify(_q); scoped_ptr<clause> c = clausify(_q);
quantifier* q = c->q(); quantifier* q = c->q();
if (m_q2clauses.contains(q)) { if (m_q2clauses.contains(q))
return; return;
}
ensure_ground_enodes(*c); ensure_ground_enodes(*c);
m_clauses.push_back(c.detach()); m_clauses.push_back(c.get());
m_q2clauses.insert(q, c->index()); m_q2clauses.insert(q, c->index());
ctx.push(pop_clause(*this)); ctx.push(pop_clause(*this));
init_watch(*c); init_watch(*c);
@ -613,6 +612,7 @@ namespace q {
if (!unary) if (!unary)
j++; j++;
} }
c.detach();
} }