mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

fix alloc_entry

Browse source
This commit is contained in:
Jakob Rath 2023-12-21 14:42:46 +01:00
parent df0cd30754
commit 8605dea8be
2 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/viable.cpp
View file

@ -73,10 +73,9 @@ namespace polysat {
viable::entry* viable::alloc_entry(pvar var) { viable::entry* viable::alloc_entry(pvar var) {
if (m_alloc.empty()) if (m_alloc.empty())
return alloc(entry); return alloc(entry, var);
auto* e = m_alloc.back(); auto* e = m_alloc.back();
e->reset(); e->reset(var);
e->var = var;
m_alloc.pop_back(); m_alloc.pop_back();
return e; return e;
} }

6
src/math/polysat/viable.h
View file

@ -57,13 +57,15 @@ namespace polysat {
bool valid_for_lemma = true; bool valid_for_lemma = true;
pvar var = null_var; pvar var = null_var;
void reset() { entry(pvar v) { reset(v); }
void reset(pvar v) {
// dll_base<entry>::init(this); // we never did this in alloc_entry either // dll_base<entry>::init(this); // we never did this in alloc_entry either
fi_record::reset(); fi_record::reset();
refined = false; refined = false;
active = true; active = true;
valid_for_lemma = true; valid_for_lemma = true;
var = null_var; var = v;
} }
}; };