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

fix trace/debug build for unreferenced variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-04 19:55:38 -07:00
parent cba9a160d3
commit 41803ec1cf
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_str.cpp
View file

@ -5619,7 +5619,7 @@ namespace smt {
} }
void theory_str::print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap) { void theory_str::print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap) {
TRACE("str", tout << mk_pp(node, m) << std::endl;); TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;);
if (groundedMap.find(node) != groundedMap.end()) { if (groundedMap.find(node) != groundedMap.end()) {
std::map<std::vector<expr*>, std::set<expr*> >::iterator itor = groundedMap[node].begin(); std::map<std::vector<expr*>, std::set<expr*> >::iterator itor = groundedMap[node].begin();
for (; itor != groundedMap[node].end(); ++itor) { for (; itor != groundedMap[node].end(); ++itor) {
@ -7515,7 +7515,7 @@ namespace smt {
while (varItor != cut_var_map.end()) { while (varItor != cut_var_map.end()) {
std::stack<T_cut*> & val = cut_var_map[varItor->m_key]; std::stack<T_cut*> & val = cut_var_map[varItor->m_key];
while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) { while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) {
TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout);); // TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout););
// T_cut * aCut = val.top(); // T_cut * aCut = val.top();
val.pop(); val.pop();
// dealloc(aCut); // dealloc(aCut);
@ -8828,7 +8828,7 @@ namespace smt {
// break; // break;
} else { } else {
// debug // debug
TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); // TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;);
} }
} }
} }
@ -9315,8 +9315,8 @@ namespace smt {
<< mk_ismt2_pp(makeupAssert, m) << std::endl;); << mk_ismt2_pp(makeupAssert, m) << std::endl;);
assert_axiom(makeupAssert); assert_axiom(makeupAssert);
} else { } else {
TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) // TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m)
<< " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); // << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;);
} }
} }
@ -10334,7 +10334,7 @@ namespace smt {
} }
if (duplicated && dupVar != NULL) { if (duplicated && dupVar != NULL) {
TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager())
<< " = " << mk_ismt2_pp(dupVar, m) << " (SKIP)" << std::endl;); << " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;);
continue; continue;
} else { } else {
eqcRepSet.insert(freeVar); eqcRepSet.insert(freeVar);