#5778

Z3Prover · Jan 21, 2022 · 9969809 · 9969809
1 parent a1f7676
commit 9969809
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
@@ -564,7 +564,7 @@ namespace 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);
         quantifier* q = c->q();
         if (m_q2clauses.contains(q)) {
@@ -588,7 +588,7 @@ namespace q {
             app * mp = to_app(q->get_pattern(i));
             SASSERT(m.is_pattern(mp));
             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) {
                 TRACE("q", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";);
                 if (!m_lazy_mam)

diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
@@ -286,6 +286,11 @@ namespace q {
                     idx = i;
                 }
             }
+            if (!e1 && updated) {
+                m_expanded.reset();
+                m_expanded.push_back(r);
+                return true;
+            }
             if (!e1)
                 return false;