mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 08:45:47 +00:00
Code Activity

correctly reserve entries in theory aware branching queue heap

Browse source
This commit is contained in:
Murphy Berzish 2017-01-10 22:15:46 -05:00
parent bc5af58734
commit 20a8ad9b21
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_case_split_queue.cpp
View file

@ -1130,9 +1130,6 @@ namespace smt {
} }
virtual void activity_increased_eh(bool_var v) { virtual void activity_increased_eh(bool_var v) {
if (m_theory_queue.contains(v)) {
m_theory_queue.decreased(v);
}
m_base_queue->activity_increased_eh(v); m_base_queue->activity_increased_eh(v);
} }
@ -1214,6 +1211,7 @@ namespace smt {
m_theory_vars.insert(v); m_theory_vars.insert(v);
m_theory_var_phase.insert(v, phase); m_theory_var_phase.insert(v, phase);
m_theory_var_priority.insert(v, priority); m_theory_var_priority.insert(v, priority);
m_theory_queue.reserve(v+1);
m_theory_queue.insert(v); m_theory_queue.insert(v);
} }