#5454

Z3Prover · Aug 10, 2021 · 7ab7b86 · 7ab7b86
1 parent 081cdbd
commit 7ab7b86
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
@@ -490,6 +490,10 @@ namespace q {
         TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";);
         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_q2clauses.insert(q, c->index());

diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
@@ -414,7 +414,7 @@ namespace q {
         enode_vector               m_candidates;
 #ifdef Z3DEBUG
         egraph *                   m_egraph;
-        ptr_vector<app>            m_patterns;
+        svector<std::pair<quantifier*, app*>>            m_patterns;
 #endif
 #ifdef _PROFILE_MAM
         stopwatch                  m_watch;
@@ -568,7 +568,7 @@ namespace q {
             m_egraph = ctx;
         }
 
-        ptr_vector<app> & get_patterns() {
+        svector<std::pair<quantifier*, app*>> & get_patterns() {
             return m_patterns;
         }
 #endif
@@ -578,8 +578,8 @@ namespace q {
             if (m_egraph) {
                 ast_manager & m = m_egraph->get_manager();
                 out << "patterns:\n";
-                for (app* a : m_patterns) 
-                    out << mk_pp(a, m) << "\n";
+                for (auto [q, a] : m_patterns) 
+                    out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
             }
 #endif
             out << "function: " << m_root_lbl->get_name();
@@ -2862,12 +2862,11 @@ namespace q {
                 // The E-matching engine that was built when all + and * applications were binary.
                 // We ignore the pattern if it does not have the expected number of arguments.
                 // This is not the ideal solution, but it avoids possible crashes.
-                if (tree->expected_num_args() == p->get_num_args()) {
+                if (tree->expected_num_args() == p->get_num_args()) 
                     m_compiler.insert(tree, qa, mp, first_idx, false);
-                }
             }
-            DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
-                       ctx.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
+            DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
+                       ctx.push(push_back_trail<std::pair<quantifier*,app*>, false>(m_trees[lbl_id]->get_patterns())););
             TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
         }