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

#5778

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-21 09:40:06 +01:00
parent a1f7676c81
commit 9969809745
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -564,7 +564,7 @@ namespace q {
}; };
void ematch::add(quantifier* _q) { void ematch::add(quantifier* _q) {
TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";); TRACE("q", tout << "add " << mk_pp(_q, m) << "\n");
clause* c = clausify(_q); clause* c = clausify(_q);
quantifier* q = c->q(); quantifier* q = c->q();
if (m_q2clauses.contains(q)) { if (m_q2clauses.contains(q)) {
@ -588,7 +588,7 @@ namespace q {
app * mp = to_app(q->get_pattern(i)); app * mp = to_app(q->get_pattern(i));
SASSERT(m.is_pattern(mp)); SASSERT(m.is_pattern(mp));
bool unary = (mp->get_num_args() == 1); bool unary = (mp->get_num_args() == 1);
TRACE("q", tout << "adding:\n" << expr_ref(mp, m) << "\n";); TRACE("q", tout << "adding:\n" << expr_ref(mp, m) << "\n");
if (!unary && j >= num_eager_multi_patterns) { if (!unary && j >= num_eager_multi_patterns) {
TRACE("q", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";); TRACE("q", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";);
if (!m_lazy_mam) if (!m_lazy_mam)

5
src/sat/smt/q_solver.cpp
View file

@ -286,6 +286,11 @@ namespace q {
idx = i; idx = i;
} }
} }
if (!e1 && updated) {
m_expanded.reset();
m_expanded.push_back(r);
return true;
}
if (!e1) if (!e1)
return false; return false;