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

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-16 21:57:46 -05:00
parent 1dedfe3164
commit 0b3a8522ac
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/q_mam.cpp
View file

@ -3705,9 +3705,12 @@ namespace q {
SASSERT(tmp_tree != 0); SASSERT(tmp_tree != 0);
SASSERT(!m_egraph.enodes_of(lbl).empty()); SASSERT(!m_egraph.enodes_of(lbl).empty());
m_interpreter.init(tmp_tree); m_interpreter.init(tmp_tree);
for (enode * app : m_egraph.enodes_of(lbl)) auto& nodes = m_egraph.enodes_of(lbl);
for (unsigned i = 0; i < nodes.size(); ++i) {
enode* app = nodes[i];
if (ctx.is_relevant(app)) if (ctx.is_relevant(app))
m_interpreter.execute_core(tmp_tree, app); m_interpreter.execute_core(tmp_tree, app);
}
m_tmp_trees[lbl_id] = nullptr; m_tmp_trees[lbl_id] = nullptr;
dealloc(tmp_tree); dealloc(tmp_tree);
} }