diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 8e959e964..295216ef9 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -211,7 +211,7 @@ namespace euf {
         for (sat::literal lit : r) 
             if (s().lvl(lit) > 0) r[j++] = lit;
         r.shrink(j);
-        TRACE("euf", tout << "eplain " << l << " <- " << r << " " << probing << "\n";);
+        TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";);
         DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
 
         if (!probing)
diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h
index 2107b2172..6cb889ee1 100644
--- a/src/sat/smt/q_clause.h
+++ b/src/sat/smt/q_clause.h
@@ -59,10 +59,12 @@ namespace q {
         unsigned            m_index;
         vector<lit>         m_lits;
         quantifier_ref      m_q;
+        unsigned            m_watch = 0;
         sat::literal        m_literal = sat::null_literal;
         q::quantifier_stat* m_stat = nullptr;
         binding*            m_bindings = nullptr;
 
+
         clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}
 
         std::ostream& display(euf::solver& ctx, std::ostream& out) const;
diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp
index 4d5a37821..1ecc0e4ec 100644
--- a/src/sat/smt/q_eval.cpp
+++ b/src/sat/smt/q_eval.cpp
@@ -39,40 +39,37 @@ namespace q {
         unsigned sz = c.m_lits.size();
         unsigned n = c.num_decls();
         m_indirect_nodes.reset();
-        for (unsigned i = 0; i < sz; ++i) {
+        for (unsigned j = 0; j < sz; ++j) {
+            unsigned i = (j + c.m_watch) % sz;
             unsigned lim = m_indirect_nodes.size();
             lit l = c[i];
             lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence);
+            std::cout << l.sign << ": " << l.lhs << " ~~ " << l.rhs << " " << cmp << "\n";
             switch (cmp) {
             case l_false:
                 m_indirect_nodes.shrink(lim);
                 if (!l.sign)
                     break;
-                if (i > 0)
-                    std::swap(c[0], c[i]);
+                c.m_watch = i;
                 return l_true;
             case l_true:
                 m_indirect_nodes.shrink(lim);
                 if (l.sign)
                     break;
-                if (i > 0)
-                    std::swap(c[0], c[i]);
+                c.m_watch = i;
                 return l_true;
             case l_undef:
                 TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";);
-                if (idx == 0) {
+                if (idx != UINT_MAX) {
                     idx = UINT_MAX;
                     return l_undef;
                 }
-                if (i > 0)
-                    std::swap(c[0], c[i]);
-                idx = 0;
+                idx = i;
                 break;
             }
         }
         if (idx == UINT_MAX)
             return l_false;
-        
         return l_undef;
     }
 
@@ -97,8 +94,9 @@ namespace q {
               tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";);
         
         lbool c;
-        if (sn && sn == tn)
+        if (sn && sn == tn) 
             return l_true;
+        
         if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) {
             evidence.push_back(euf::enode_pair(sn, tn));
             return l_false;