#5324

src/ast/euf/euf_enode.h

@@ -41,28 +41,28 @@ namespace euf {
     const theory_id null_theory_id = -1;
 
     class enode {
-        expr* m_expr{ nullptr };
-        bool          m_mark1{ false };
-        bool          m_mark2{ false };
-        bool          m_commutative{ false };
-        bool          m_update_children{ false };
-        bool          m_interpreted{ false };
-        bool          m_merge_enabled{ true }; 
-        bool          m_is_equality{ false };   // Does the expression represent an equality
-        lbool         m_value;                  // Assignment by SAT solver for Boolean node
-        unsigned      m_bool_var { UINT_MAX };  // SAT solver variable associated with Boolean node
-        unsigned      m_class_size{ 1 };        // Size of the equivalence class if the enode is the root.
-        unsigned      m_table_id{ UINT_MAX };       
-        unsigned      m_generation { 0 };       // Tracks how many quantifier instantiation rounds were needed to generate this enode.
+        expr*         m_expr = nullptr;
+        bool          m_mark1 = false;
+        bool          m_mark2 = false;
+        bool          m_commutative = false;
+        bool          m_update_children = false;
+        bool          m_interpreted = false;
+        bool          m_merge_enabled = true; 
+        bool          m_is_equality = false;    // Does the expression represent an equality
+        lbool         m_value = l_undef;        // Assignment by SAT solver for Boolean node
+        unsigned      m_bool_var = UINT_MAX;    // SAT solver variable associated with Boolean node
+        unsigned      m_class_size = 1;         // Size of the equivalence class if the enode is the root.
+        unsigned      m_table_id = UINT_MAX;       
+        unsigned      m_generation = 0;         // Tracks how many quantifier instantiation rounds were needed to generate this enode.
         enode_vector  m_parents;
-        enode* m_next   { nullptr };
-        enode* m_root   { nullptr };
-        enode* m_target { nullptr };
-        enode* m_cg     { nullptr };
+        enode* m_next   = nullptr;
+        enode* m_root   = nullptr;
+        enode* m_target = nullptr;
+        enode* m_cg     = nullptr;
         th_var_list   m_th_vars;
         justification m_justification;
-        unsigned      m_num_args{ 0 };
-        signed char         m_lbl_hash { -1 };  // It is different from -1, if enode is used in a pattern
+        unsigned      m_num_args = 0;
+        signed char         m_lbl_hash = -1;  // It is different from -1, if enode is used in a pattern
         approx_set          m_lbls;
         approx_set          m_plbls;
         enode* m_args[0];

src/sat/smt/q_ematch.cpp

@@ -229,11 +229,12 @@ namespace q {
         TRACE("q", tout << "on-binding " << mk_pp(q, m) << "\n";);
         unsigned idx = m_q2clauses[q];
         clause& c = *m_clauses[idx];
-        if (!propagate(_binding, max_generation, c)) 
+        bool new_propagation = false;
+        if (!propagate(_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 ematch::propagate(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);
@@ -260,6 +261,7 @@ namespace q {
             ++m_stats.m_num_propagations;
             ctx.propagate(instantiate(c, binding, c[idx]), j_idx);
         }
+        propagated = true;
         return true;
     }
 
@@ -479,10 +481,8 @@ namespace q {
                 continue;
 
             do {
-                if (propagate(b->m_nodes, b->m_max_generation, c)) {
+                if (propagate(b->m_nodes, b->m_max_generation, c, propagated)) 
                     to_remove.push_back(b);
-                    propagated = true;
-                }
                 else if (flush) {
                     instantiate(*b, c);
                     to_remove.push_back(b);

src/sat/smt/q_ematch.h

@@ -130,7 +130,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 propagate(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

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