diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h
index ea969d1db..f4b3ecb12 100644
--- a/src/smt/smt_justification.h
+++ b/src/smt/smt_justification.h
@@ -181,6 +181,7 @@ namespace smt {
         enode *         m_node2;
     public:
         eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) {
+            SASSERT(n1 != n2);
         }
 
         virtual void get_antecedents(conflict_resolution & cr);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 832995994..76d8a5a74 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1891,7 +1891,7 @@ bool theory_seq::solve_ne(unsigned idx) {
                     new_ls.push_back(ls);
                     new_rs.push_back(rs);
                 }
-                else {
+                else if (nl != nr) {                
                     literal lit(mk_eq(nl, nr, false));
                     ctx.mark_as_relevant(lit);
                     new_lits.push_back(lit);