#5336

src/sat/smt/q_clause.h

@@ -56,8 +56,8 @@ namespace q {
         vector<lit>         m_lits;
         quantifier_ref      m_q;
         sat::literal        m_literal;
-        q::quantifier_stat* m_stat { nullptr };
-        binding*            m_bindings { nullptr };
+        q::quantifier_stat* m_stat = nullptr;
+        binding*            m_bindings = nullptr;
 
         clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}
 

src/sat/smt/q_ematch.cpp

@@ -213,6 +213,14 @@ namespace q {
         unsigned sz = sizeof(binding) + sizeof(euf::enode* const*)*n;
         void* mem = ctx.get_region().allocate(sz);
         return new (mem) binding(pat, max_generation, min_top, max_top);
+    }  
+
+    euf::enode* const* ematch::alloc_binding(clause& c, euf::enode* const* _binding) {
+        unsigned sz = sizeof(euf::enode* const*) * c.num_decls();
+        euf::enode** binding = (euf::enode**)ctx.get_region().allocate(sz);
+        for (unsigned i = 0; i < c.num_decls(); ++i)
+            binding[i] = _binding[i];
+        return binding;
     }
 
     void ematch::add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) {
@@ -230,11 +238,11 @@ namespace q {
         unsigned idx = m_q2clauses[q];
         clause& c = *m_clauses[idx];
         bool new_propagation = false;
-        if (!propagate(_binding, max_generation, c, new_propagation)) 
+        if (!propagate(false, _binding, max_generation, c, new_propagation)) 
             add_binding(c, pat, _binding, max_generation, min_gen, max_gen);
     }
 
-    bool ematch::propagate(euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
+    bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
         TRACE("q", c.display(ctx, tout) << "\n";);
         unsigned idx = UINT_MAX;
         lbool ev = m_eval(binding, c, idx);
@@ -252,6 +260,8 @@ namespace q {
         }
         if (ev == l_undef && max_generation > m_generation_propagation_threshold)
             return false;
+        if (!is_owned) 
+            binding = alloc_binding(c, binding);        
         auto j_idx = mk_justification(idx, c, binding);       
         if (ev == l_false) {
             ++m_stats.m_num_conflicts;
@@ -482,7 +492,7 @@ namespace q {
                 continue;
 
             do {
-                if (propagate(b->m_nodes, b->m_max_generation, c, propagated)) 
+                if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
                     to_remove.push_back(b);
                 else if (flush) {
                     instantiate(*b, c);

src/sat/smt/q_ematch.h

@@ -81,6 +81,7 @@ namespace q {
         unsigned_vector               m_clause_queue;
 
         binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top);
+        euf::enode* const* alloc_binding(clause& c, euf::enode* const* _binding);
         void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
 
         sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b);
@@ -130,7 +131,7 @@ namespace q {
 
         void add_instantiation(clause& c, binding& b, sat::literal lit);
 
-        bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c, bool& new_propagation);
+        bool propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& new_propagation);
 
         std::ostream& display(std::ostream& out) const;
 

src/sat/smt/q_queue.cpp

@@ -146,7 +146,7 @@ namespace q {
 
         unsigned gen = get_new_gen(f, ent.m_cost);
         bool new_propagation = false;
-        if (em.propagate(f.nodes(), gen, *f.c, new_propagation))
+        if (em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
             return;
 
         auto* ebindings = m_subst(q, num_bindings);