diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 4b2d123fd..77b20348b 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -85,12 +85,12 @@ namespace q {
             lit.lhs;
             lit.rhs;
             if (lit.sign) {
-                SASSERT(l_true == compare(n, b.m_nodes, l.lhs, l.rhs));
-                explain_eq(c, b, lit.lhs, lit.rhs);
+                SASSERT(l_true == compare(n, b.m_nodes, lit.lhs, lit.rhs));
+                explain_eq(n, b.m_nodes, lit.lhs, lit.rhs);
             }
             else {
-                SASSERT(l_false == compare(n, b.m_nodes, l.lhs, l.rhs));
-                explain_diseq(c, b, lit.lhs, lit.rhs);
+                SASSERT(l_false == compare(n, b.m_nodes, lit.lhs, lit.rhs));
+                explain_diseq(n, b.m_nodes, lit.lhs, lit.rhs);
             }
         }
         ctx.get_egraph().end_explain();
@@ -125,8 +125,8 @@ namespace q {
             explain_eq(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i));
     }
 
-    void ematch::explain_diseq(clause& c, binding& b, expr* a, expr* b) {
-        if (m.are_diseq(s, t))
+    void ematch::explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t) {
+        if (m.are_distinct(s, t))
             return;
         euf::enode* sn = eval(n, binding, s);
         euf::enode* tn = eval(n, binding, t);
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index 2cd8c1308..b54597553 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -122,8 +122,8 @@ namespace q {
         // extract explanation
         ptr_vector<size_t> m_explain;
         void explain(clause& c, unsigned literal_idx, binding& b);
-        void explain_eq(clause& c, binding& b, expr* a, expr* b);
-        void explain_diseq(clause& c, binding& b, expr* a, expr* b);
+        void explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t);
+        void explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t);
 
         void attach_ground_pattern_terms(expr* pat);
         clause* clausify(quantifier* q);
diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index f8c396a75..fc7941591 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -1205,24 +1205,24 @@ namespace smt {
         }
 
         TRACE("str_fl",
-            tout << "formulas asserted to subsolver:" << std::endl;
-            for (auto e : fixed_length_assumptions) {
-                tout << mk_pp(e, subsolver.m()) << std::endl;
-            }
-            tout << "variable to character mappings:" << std::endl;
-            for (auto &entry : var_to_char_subterm_map) {
-                tout << mk_pp(entry.m_key, get_manager()) << ":";
-                for (auto e : entry.m_value) {
-                    tout << " " << mk_pp(e, subsolver.m());
-                }
-                tout << std::endl;
-            }
-            tout << "reduced boolean formulas:" << std::endl;
-              for (auto e : fixed_length_reduced_boolean_formulas) {
+              tout << "formulas asserted to subsolver:" << std::endl;
+              for (auto e : fixed_length_assumptions) {
+                  tout << mk_pp(e, subsolver.m()) << std::endl;
+              }
+              tout << "variable to character mappings:" << std::endl;
+              for (auto &entry : var_to_char_subterm_map) {
+                  tout << mk_pp(entry.m_key, get_manager()) << ":";
+                  for (auto e : *entry.m_value) {
+                      tout << " " << mk_pp(e, subsolver.m());
+                  }
+                  tout << std::endl;
+              }
+              tout << "reduced boolean formulas:" << std::endl;
+              for (expr* e : fixed_length_reduced_boolean_formulas) {
                   tout << mk_pp(e, m) << std::endl;
               }
-        );
-
+              );
+        
         TRACE("str_fl", tout << "calling subsolver" << std::endl;);
 
         lbool subproblem_status = subsolver.check(fixed_length_assumptions);