mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

use reference for case split sets

Browse source
This commit is contained in:
Murphy Berzish 2017-05-01 18:25:54 -04:00
parent b86d472eaf
commit 16a5e944d7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -3045,7 +3045,7 @@ namespace smt {
if (m_all_th_case_split_literals.contains(l.index())) { if (m_all_th_case_split_literals.contains(l.index())) {
TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;); TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
// now find the sets of literals which contain l // now find the sets of literals which contain l
vector<literal_vector> case_split_sets = m_literal2casesplitsets.get(l.index(), vector<literal_vector>()); vector<literal_vector> & case_split_sets = m_literal2casesplitsets.get(l.index(), vector<literal_vector>());
for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) { for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
literal_vector case_split_set = *it; literal_vector case_split_set = *it;
TRACE("theory_case_split", tout << "found case split set { "; TRACE("theory_case_split", tout << "found case split set { ";