mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-16 09:05:44 -07:00
parent b93a04c38f
commit b12a1caa07
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -321,7 +321,7 @@ namespace smt {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo); m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
varInfo->vars[node] = 1; varInfo->vars.insert(node, 1);
cut_var_map.insert(baseNode, std::stack<T_cut*>()); cut_var_map.insert(baseNode, std::stack<T_cut*>());
cut_var_map[baseNode].push(varInfo); cut_var_map[baseNode].push(varInfo);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
@ -330,7 +330,7 @@ namespace smt {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo); m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
varInfo->vars[node] = 1; varInfo->vars.insert(node, 1);
cut_var_map[baseNode].push(varInfo); cut_var_map[baseNode].push(varInfo);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
} else { } else {
@ -339,11 +339,11 @@ namespace smt {
m_cut_allocs.push_back(varInfo); m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
varInfo->vars[node] = 1; varInfo->vars.insert(node, 1);
cut_var_map[baseNode].push(varInfo); cut_var_map[baseNode].push(varInfo);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
} else if (cut_var_map[baseNode].top()->level == slevel) { } else if (cut_var_map[baseNode].top()->level == slevel) {
cut_var_map[baseNode].top()->vars[node] = 1; cut_var_map[baseNode].top()->vars.insert(node, 1);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
} else { } else {
get_manager().raise_exception("entered illegal state during add_cut_info_one_node()"); get_manager().raise_exception("entered illegal state during add_cut_info_one_node()");