From 839d6fd5beb4fec68282b93a853114ec3361b67c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Feb 2020 21:37:56 -1000 Subject: [PATCH] fix #3018 Signed-off-by: Nikolaj Bjorner --- src/math/subpaving/subpaving_t_def.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index f72eacdb7..91ff9833b 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -81,7 +81,8 @@ public: // Return the next variable to branch. var operator()(typename context_t::node * n) override { typename context_t::numeral_manager & nm = this->ctx()->nm(); - SASSERT(this->ctx()->num_vars() > 0); + if (this->ctx()->num_vars() == 0) + return null_var; var x = this->ctx()->splitting_var(n); if (x == null_var) x = 0; @@ -823,7 +824,7 @@ void context_t::add_clause_core(unsigned sz, ineq * const * atoms, bool lemma if (watch) { for (unsigned i = 0; i < sz; i++) { var x = c->m_atoms[i]->x(); - if (i == 0 || x != c->m_atoms[i-1]->x()) + if (x != null_var && (i == 0 || x != c->m_atoms[i-1]->x())) m_wlist[x].push_back(watched(c)); } }