diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index 9cd812a9a..850e183e8 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -45,6 +45,7 @@ namespace euf {
         expr*         m_expr = nullptr;
         bool          m_mark1 = false;
         bool          m_mark2 = false;
+        bool          m_mark3 = false;
         bool          m_commutative = false;
         bool          m_interpreted = false;
         bool          m_merge_enabled = true; 
@@ -173,6 +174,9 @@ namespace euf {
         void mark2() { m_mark2 = true; }
         void unmark2() { m_mark2 = false; }
         bool is_marked2() { return m_mark2; }
+        void mark3() { m_mark3 = true; }
+        void unmark3() { m_mark3 = false; }
+        bool is_marked3() { return m_mark3; }
 
         template<bool m> void mark1_targets() {
             enode* n = this;
diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp
index 1cfbe7779..a87c5ec0d 100644
--- a/src/sat/smt/q_eval.cpp
+++ b/src/sat/smt/q_eval.cpp
@@ -230,13 +230,17 @@ namespace q {
                 if (!n)
                     return nullptr;
                 for (unsigned i = args.size(); i-- > 0; ) {
-                    if (args[i] != n->get_arg(i)) {
-                        // roots could be different when using commutativity
-                        // instead of compensating for this, we just bail out
-                        if (args[i]->get_root() != n->get_arg(i)->get_root())
-                            return nullptr;
-                        evidence.push_back(euf::enode_pair(args[i], n->get_arg(i)));
-                    }
+                    euf::enode* a = args[i], *b = n->get_arg(i);
+                    if (a == b)
+                        continue;
+
+                    // roots could be different when using commutativity
+                    // instead of compensating for this, we just bail out
+                    if (a->get_root() != b->get_root())
+                        return nullptr;
+
+                    TRACE("q", tout << "evidence " << ctx.bpp(a) << " " << ctx.bpp(b) << "\n");
+                    evidence.push_back(euf::enode_pair(a, b));
                 }
                 m_indirect_nodes.push_back(n);
                 m_eval.setx(t->get_id(), n, nullptr);
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index edf00615b..b029b0618 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -553,8 +553,8 @@ namespace q {
         void unmark(unsigned head) {
             for (unsigned i = m_candidates.size(); i-- > head; ) {
                 enode* app = m_candidates[i];
-                if (app->is_marked2())
-                    app->unmark2();
+                if (app->is_marked3())
+                    app->unmark3();
             }
         }
 
@@ -2022,9 +2022,9 @@ namespace q {
                 code_tree::scoped_unmark _unmark(t);
                 while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) {
                     TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";);
-                    if (!app->is_marked2() && app->is_cgr()) {
+                    if (!app->is_marked3() && app->is_cgr()) {
                         execute_core(t, app);                       
-                        app->mark2();
+                        app->mark3();
                     }
                 }
             }