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

fix issue with dependency m_todo updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-10 02:22:44 -08:00
parent c1d58088be
commit ef320af90b
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/util/dependency.h
View file

@ -106,6 +106,7 @@ private:
void del(dependency * d) { void del(dependency * d) {
SASSERT(d); SASSERT(d);
SASSERT(m_todo.empty());
m_todo.push_back(d); m_todo.push_back(d);
while (!m_todo.empty()) { while (!m_todo.empty()) {
d = m_todo.back(); d = m_todo.back();
@ -218,16 +219,17 @@ public:
void linearize(dependency * d, vector<value, false> & vs) { void linearize(dependency * d, vector<value, false> & vs) {
if (!d) if (!d)
return; return;
m_todo.reset(); SASSERT(m_todo.empty());
d->mark(); d->mark();
m_todo.push_back(d); m_todo.push_back(d);
linearize_todo(m_todo, vs); linearize_todo(m_todo, vs);
m_todo.reset();
} }
void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) { void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) {
if (deps.empty()) if (deps.empty())
return; return;
m_todo.reset(); SASSERT(m_todo.empty());
for (auto* d : deps) { for (auto* d : deps) {
if (d && !d->is_marked()) { if (d && !d->is_marked()) {
d->mark(); d->mark();
@ -235,6 +237,7 @@ public:
} }
} }
linearize_todo(m_todo, vs); linearize_todo(m_todo, vs);
m_todo.reset();
} }
}; };