From c68c56b0e7190fa220ad7e0741a6c5eec2b7efa6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Oct 2016 13:09:27 -0700 Subject: [PATCH] fix incorrect assertion when checking signs of literals, exposed by mitls regressions Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 9 +++++---- src/smt/smt_internalizer.cpp | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5f258fc61..912bbeb36 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3773,15 +3773,16 @@ namespace smt { #ifdef Z3DEBUG for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; - if (m_manager.is_not(expr_lits.get(i))) { + expr* real_atom; + if (expr_signs[i] != l.sign()) { + + VERIFY(m_manager.is_not(expr_lits.get(i), real_atom)); // the sign must have flipped when internalizing - expr * real_atom = to_app(expr_lits.get(i))->get_arg(0); + CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";); SASSERT(real_atom == bool_var2expr(l.var())); - SASSERT(expr_signs[i] != l.sign()); } else { SASSERT(expr_lits.get(i) == bool_var2expr(l.var())); - SASSERT(expr_signs[i] == l.sign()); } } #endif diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 94ce453b4..8028feae6 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -840,7 +840,7 @@ namespace smt { } #endif TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << "\n";); - TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";); + TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";); set_bool_var(id, v); m_bdata.reserve(v+1); m_activity.reserve(v+1);