diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 7922895a9..9ab9cfbbe 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -73,10 +73,9 @@ namespace polysat { viable::entry* viable::alloc_entry(pvar var) { if (m_alloc.empty()) - return alloc(entry); + return alloc(entry, var); auto* e = m_alloc.back(); - e->reset(); - e->var = var; + e->reset(var); m_alloc.pop_back(); return e; } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index be1d699ae..243f44cd6 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -57,13 +57,15 @@ namespace polysat { bool valid_for_lemma = true; pvar var = null_var; - void reset() { + entry(pvar v) { reset(v); } + + void reset(pvar v) { // dll_base::init(this); // we never did this in alloc_entry either fi_record::reset(); refined = false; active = true; valid_for_lemma = true; - var = null_var; + var = v; } };