From 7d693a5f9f3a535317ea22c37a67388a367c1fa7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 20:01:14 -0800 Subject: [PATCH] fix different bug reported on #1366 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fb8f36c59..131d1fd1b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1987,10 +1987,13 @@ bool theory_seq::solve_ne(unsigned idx) { dependency* deps1 = 0; if (explain_eq(n.l(), n.r(), deps1)) { - new_lits.reset(); - new_lits.push_back(~mk_eq(n.l(), n.r(), false)); - new_deps = deps1; - TRACE("seq", tout << "conflict explained\n";); + literal diseq = mk_eq(n.l(), n.r(), false); + if (ctx.get_assignment(diseq) == l_false) { + new_lits.reset(); + new_lits.push_back(~diseq); + new_deps = deps1; + TRACE("seq", tout << "conflict explained\n";); + } } set_conflict(new_deps, new_lits); SASSERT(m_new_propagation);