diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 7aa9329d4..cf46badd6 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1506,6 +1506,7 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
 }
 
 br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
+    TRACE("seq", tout << mk_pp(l, m()) << " = " << mk_pp(r, m()) << "\n";);
     expr_ref_vector lhs(m()), rhs(m()), res(m());
     bool changed = false;
     if (!reduce_eq(l, r, lhs, rhs, changed)) {
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index bf238d8c5..750fe0f9d 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -876,6 +876,36 @@ bool seq_decl_plugin::is_value(app* e) const {
     }
 }
 
+bool seq_decl_plugin::are_equal(app* a, app* b) const {
+    if (a == b) return true;
+    // handle concatenations
+    return false;
+}
+
+bool seq_decl_plugin::are_distinct(app* a, app* b) const {
+    if (a == b) {
+        return false;
+    }
+    if (is_app_of(a, m_family_id, OP_STRING_CONST) &&
+        is_app_of(b, m_family_id, OP_STRING_CONST)) {
+        return true;
+    }
+    if (is_app_of(a, m_family_id, OP_SEQ_UNIT) && 
+        is_app_of(b, m_family_id, OP_SEQ_UNIT)) {
+        return true;
+    }
+    if (is_app_of(a, m_family_id, OP_SEQ_EMPTY) && 
+        is_app_of(b, m_family_id, OP_SEQ_UNIT)) {
+        return true;
+    }
+    if (is_app_of(b, m_family_id, OP_SEQ_EMPTY) && 
+        is_app_of(a, m_family_id, OP_SEQ_UNIT)) {
+        return true;
+    }    
+    return false;
+}
+
+
 expr* seq_decl_plugin::get_some_value(sort* s) {
     seq_util util(*m_manager);
     if (util.is_seq(s)) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 76b5ebe31..e2722aa9a 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -182,7 +182,11 @@ public:
 
     virtual bool is_value(app * e) const;
 
-    virtual bool is_unique_value(app * e) const { return is_value(e); }
+    virtual bool is_unique_value(app * e) const { return false; }
+
+    virtual bool are_equal(app* a, app* b) const;
+
+    virtual bool are_distinct(app* a, app* b) const;
 
     virtual expr * get_some_value(sort * s);