fix for #1015

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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)) {

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)) {

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);