From d1854ab4d263abde358699839d65ce44285342ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 15:24:40 -0800 Subject: [PATCH 1/2] fix assertion in model converter for incremental mode Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_simplifier.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 05c89fba7..fac4cface 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -46,7 +46,7 @@ namespace sat { UNREACHABLE(); throw solver_exception("flipping assumption"); } - if (m_solver && m_solver->is_external(v)) { + if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) { std::cout << "flipping external v" << v << "\n"; UNREACHABLE(); throw solver_exception("flipping external"); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 6d578b4f9..c101e3a29 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -970,11 +970,12 @@ namespace sat { } void insert(literal l) { + VERIFY(process_var(l.var())); m_queue.insert(l); } bool process_var(bool_var v) { - return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); + return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); } void operator()() { From 209d31346b56e58165e77061660f1e432bd12c28 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 18:03:25 -0800 Subject: [PATCH 2/2] fix crash regression Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 4 ++-- src/sat/sat_elim_eqs.cpp | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index cd7f23576..edf1c82a2 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2294,8 +2294,8 @@ namespace sat { // literal is no longer watched. return l_undef; } - SASSERT(index <= bound); - SASSERT(c[index] == alit); + VERIFY(index <= bound); + VERIFY(c[index] == alit); // find a literal to swap with: for (unsigned i = bound + 1; i < sz; ++i) { diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 6b8d4cba7..a8eb09278 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -181,8 +181,9 @@ namespace sat { for (bool_var v : to_elim) { literal l(v, false); literal r = roots[v]; - SASSERT(v != r.var()); - if (m_solver.is_external(v) || !m_solver.set_root(l, r)) { + SASSERT(v != r.var()); + if (m_solver.is_external(v)) { + m_solver.set_root(l, r); // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false);