From 209d31346b56e58165e77061660f1e432bd12c28 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 18:03:25 -0800 Subject: [PATCH] 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);