mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

fix different bug reported on #1366

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-25 20:01:14 -08:00
parent 841c48e04d
commit 7d693a5f9f
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_seq.cpp
View file

@ -1987,11 +1987,14 @@ bool theory_seq::solve_ne(unsigned idx) {
dependency* deps1 = 0; dependency* deps1 = 0;
if (explain_eq(n.l(), n.r(), deps1)) { if (explain_eq(n.l(), n.r(), deps1)) {
literal diseq = mk_eq(n.l(), n.r(), false);
if (ctx.get_assignment(diseq) == l_false) {
new_lits.reset(); new_lits.reset();
new_lits.push_back(~mk_eq(n.l(), n.r(), false)); new_lits.push_back(~diseq);
new_deps = deps1; new_deps = deps1;
TRACE("seq", tout << "conflict explained\n";); TRACE("seq", tout << "conflict explained\n";);
} }
}
set_conflict(new_deps, new_lits); set_conflict(new_deps, new_lits);
SASSERT(m_new_propagation); SASSERT(m_new_propagation);
} }