From 878847179fa20ebfcaf7a87bc89248c212b662bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Apr 2021 15:30:17 -0700 Subject: [PATCH] fix #5144 --- src/smt/seq_ne_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; }