mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix incorrect assertion when checking signs of literals, exposed by mitls regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-24 13:09:27 -07:00
parent 33e7dccd42
commit c68c56b0e7
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_context.cpp
View file

@ -3773,15 +3773,16 @@ namespace smt {
#ifdef Z3DEBUG #ifdef Z3DEBUG
for (unsigned i = 0; i < num_lits; i++) { for (unsigned i = 0; i < num_lits; i++) {
literal l = 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 // 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(real_atom == bool_var2expr(l.var()));
SASSERT(expr_signs[i] != l.sign());
} }
else { else {
SASSERT(expr_lits.get(i) == bool_var2expr(l.var())); SASSERT(expr_lits.get(i) == bool_var2expr(l.var()));
SASSERT(expr_signs[i] == l.sign());
} }
} }
#endif #endif

2
src/smt/smt_internalizer.cpp
View file

@ -840,7 +840,7 @@ namespace smt {
} }
#endif #endif
TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << "\n";); 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); set_bool_var(id, v);
m_bdata.reserve(v+1); m_bdata.reserve(v+1);
m_activity.reserve(v+1); m_activity.reserve(v+1);