diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index fc9307792..c80b90304 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -182,7 +182,7 @@ namespace smt {
     }
 
     void eq_propagation_justification::get_antecedents(conflict_resolution & cr) {
-        cr.mark_eq(m_node1, m_node2);
+        if (m_node1 != m_node2) cr.mark_eq(m_node1, m_node2);
     }
 
     proof * eq_propagation_justification::mk_proof(conflict_resolution & cr) {
diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h
index 8354c8860..a7f62ee96 100644
--- a/src/smt/smt_justification.h
+++ b/src/smt/smt_justification.h
@@ -181,7 +181,6 @@ namespace smt {
         enode *         m_node2;
     public:
         eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) {
-            SASSERT(n1 != n2);
         }
 
         void get_antecedents(conflict_resolution & cr) override;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 5d3cc3231..b8d298742 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -5830,27 +5830,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
         expr_ref_vector disj(m);
-        // disabled pending regression on issue 1196
-        if (false && m_seq_rewrite.reduce_contains(e1, e2, disj)) {
-            literal_vector lits;
-            literal lit = mk_literal(e);
-            lits.push_back(~lit);
-            for (expr* d : disj) {
-                lits.push_back(mk_literal(d));
-            }
-            ++m_stats.m_add_axiom;            
-
-            {
-                std::function<expr*(void)> fn = [&]() { return m.mk_implies(e, m.mk_or(disj.size(), disj.c_ptr())); };
-                scoped_trace_stream _sts(*this, fn);                
-                ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-            }
-
-            for (expr* d : disj) {
-                add_axiom(lit, ~mk_literal(d));
-            }
-        }
-        else if (is_true) {
+        if (is_true) {
             expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
             expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
             f = mk_concat(f1, e2, f2);