diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp index bdfa90923..72cdf2a8f 100644 --- a/src/smt/seq_ne_solver.cpp +++ b/src/smt/seq_ne_solver.cpp @@ -144,7 +144,7 @@ bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) { expr_ref e(m), head(m), tail(m); e = mk_concat(es, es[0]->get_sort()); m_sk.decompose(e, head, tail); - propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), false); + propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), true); return true; }