mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #3018

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-15 21:37:56 -10:00
parent 1d3e9fb76c
commit 839d6fd5be
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/subpaving/subpaving_t_def.h
View file

@ -81,7 +81,8 @@ public:
// Return the next variable to branch. // Return the next variable to branch.
var operator()(typename context_t<C>::node * n) override { var operator()(typename context_t<C>::node * n) override {
typename context_t<C>::numeral_manager & nm = this->ctx()->nm(); typename context_t<C>::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); var x = this->ctx()->splitting_var(n);
if (x == null_var) if (x == null_var)
x = 0; x = 0;
@ -823,7 +824,7 @@ void context_t<C>::add_clause_core(unsigned sz, ineq * const * atoms, bool lemma
if (watch) { if (watch) {
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
var x = c->m_atoms[i]->x(); 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)); m_wlist[x].push_back(watched(c));
} }
} }