mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fix vector manip bug in theory case split

Browse source
This commit is contained in:
Murphy Berzish 2016-12-20 17:32:51 -05:00
parent ab0fcc42f9
commit df63b62763
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context.cpp
View file

@ -2989,7 +2989,6 @@ namespace smt {
m_literal2casesplitsets.insert(l.index(), vector<literal_vector>()); m_literal2casesplitsets.insert(l.index(), vector<literal_vector>());
} }
m_literal2casesplitsets[l.index()].push_back(new_case_split); m_literal2casesplitsets[l.index()].push_back(new_case_split);
push_trail(push_back_vector<context, vector<literal_vector> >(m_literal2casesplitsets[l.index()]));
} }
TRACE("theory_case_split", tout << "tracking case split literal set { "; TRACE("theory_case_split", tout << "tracking case split literal set { ";
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {
@ -3002,6 +3001,11 @@ namespace smt {
void context::undo_th_case_split(literal l) { void context::undo_th_case_split(literal l) {
m_all_th_case_split_literals.remove(l.index()); m_all_th_case_split_literals.remove(l.index());
if (m_literal2casesplitsets.contains(l.index())) {
if (!m_literal2casesplitsets[l.index()].empty()) {
m_literal2casesplitsets[l.index()].pop_back();
}
}
} }
bool context::propagate_th_case_split() { bool context::propagate_th_case_split() {