#5324

src/sat/smt/q_mam.cpp

@@ -3030,6 +3030,7 @@ namespace q {
         ptr_vector<code_tree>       m_tmp_trees;
         ptr_vector<func_decl>       m_tmp_trees_to_delete;
         ptr_vector<code_tree>       m_to_match;
+        unsigned                    m_to_match_head = 0;
         typedef std::pair<quantifier *, app *> qp_pair;
         svector<qp_pair>            m_new_patterns; // recently added patterns
 
@@ -3059,16 +3060,14 @@ namespace q {
         enode *                     m_other { nullptr }; // temp field
         bool                        m_check_missing_instances { false };
 
-        class reset_to_match : public trail {
+        class pop_to_match : public trail {
             mam_impl& i;
         public:
-            reset_to_match(mam_impl& i):i(i) {}
+            pop_to_match(mam_impl& i):i(i) {}
             void undo() override {
-                if (i.m_to_match.empty())
-                    return;
-                for (code_tree* t : i.m_to_match) 
-                    t->reset_candidates();
-                i.m_to_match.reset();
+                code_tree* t = i.m_to_match.back();
+                t->reset_candidates();
+                i.m_to_match.pop_back();
             }
         };
 
@@ -3092,12 +3091,12 @@ namespace q {
         }
 
         void add_candidate(code_tree * t, enode * app) {
-            if (t != nullptr) {
+            if (t) {
                 TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_expr(), m););
-                if (m_to_match.empty()) 
-                    ctx.push(reset_to_match(*this));
-                if (!t->has_candidates()) 
+                if (!t->has_candidates()) {
+                    ctx.push(pop_to_match(*this));
                     m_to_match.push_back(t);
+                }
                 t->add_candidate(app);
             }
         }
@@ -3755,7 +3754,6 @@ namespace q {
 
         void reset() override {
             m_trees.reset();
-            m_to_match.reset();
             m_new_patterns.reset();
             m_is_plbl.reset();
             m_is_clbl.reset();
@@ -3773,12 +3771,15 @@ namespace q {
 
         void propagate() override {
             TRACE("trigger_bug", tout << "match\n"; display(tout););
-            for (code_tree* t : m_to_match) {
+            if (m_to_match_head >= m_to_match.size())
+                return;
+            ctx.push(value_trail<unsigned>(m_to_match_head));
+            for (; m_to_match_head < m_to_match.size(); ++m_to_match_head) {
+                code_tree* t = m_to_match[m_to_match_head];
                 SASSERT(t->has_candidates());
                 m_interpreter.execute(t);
                 t->reset_candidates();
             }
-            m_to_match.reset();
             if (!m_new_patterns.empty()) {
                 match_new_patterns();
                 m_new_patterns.reset();