From 9635ddd8fceb6bdde7dc7725e696e6c123af22f4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Dec 2018 00:54:10 -0800 Subject: [PATCH] fix #2018 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 19ef14c3a..abfb28a49 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -4561,11 +4561,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { IF_VERBOSE(11, verbose_stream() << "intersect " << re << " " << mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";); re = m_util.re.mk_inter(entry.m_re, re); m_rewrite(re); - lits.push_back(entry.m_lit); + lits.push_back(~entry.m_lit); enode* n1 = ensure_enode(entry.m_s); enode* n2 = ensure_enode(s); if (n1 != n2) { - lits.push_back(mk_eq(n1->get_owner(), n2->get_owner(), false)); + lits.push_back(~mk_eq(n1->get_owner(), n2->get_owner(), false)); } } }