diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h
index 8eca0df76..2107b2172 100644
--- a/src/sat/smt/q_clause.h
+++ b/src/sat/smt/q_clause.h
@@ -29,7 +29,9 @@ namespace q {
         expr_ref rhs;
         bool     sign;
         lit(expr_ref const& lhs, expr_ref const& rhs, bool sign):
-            lhs(lhs), rhs(rhs), sign(sign) {}
+            lhs(lhs), rhs(rhs), sign(sign) {
+            SASSERT(!rhs.m().is_false(rhs) || !sign);
+        }
         std::ostream& display(std::ostream& out) const;
     };
 
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 7de922f40..6040c4b4b 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -419,6 +419,16 @@ namespace q {
                 r = sign ? m.mk_false() : m.mk_true();
                 sign = false;
             }
+            if (m.is_true(l) || m.is_false(l))
+                std::swap(l, r);
+            if (sign && m.is_false(r)) {
+                r = m.mk_true();
+                sign = false;
+            }
+            else if (sign && m.is_true(r)) {
+                r = m.mk_false();
+                sign = false;
+            }
             cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
         }
         if (q->get_num_patterns() == 0) {