diff --git a/.travis.yml b/.travis.yml index d74ec93f7e3..f3147e89e53 100644 --- a/.travis.yml +++ b/.travis.yml @@ -75,4 +75,8 @@ script: COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" && eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" && + eval ${PRE_COMMAND} ${COMMAND} && + COMMAND="make -C src clean" && + eval ${PRE_COMMAND} ${COMMAND} && + COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" && eval ${PRE_COMMAND} ${COMMAND} diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index 1a4d6090f47..930d0ae69b9 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -224,6 +224,13 @@ void dominators_pretty_print_node(const T &node, std::ostream &out) out << node; } +inline void dominators_pretty_print_node( + const goto_programt::targett& target, + std::ostream& out) +{ + out << target->code.pretty(); +} + /*******************************************************************\ Function: cfg_dominators_templatet::output @@ -241,7 +248,7 @@ void cfg_dominators_templatet::output(std::ostream &out) const { for(const auto &node : cfg.entry_map) { - T n=node.first; + auto n=node.first; dominators_pretty_print_node(n, out); if(post_dom) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 1fe89a7b8f6..189048994b8 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -6,8 +6,6 @@ Author: Peter Schrammel \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp index 16985daa5e9..593fc78006d 100644 --- a/src/analyses/natural_loops.cpp +++ b/src/analyses/natural_loops.cpp @@ -10,8 +10,6 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include "natural_loops.h" -// #define DEBUG - /*******************************************************************\ Function: show_natural_loops diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 327ebbdf112..ff56c687c93 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -81,8 +81,6 @@ Function: natural_loops_templatet::compute \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 2f39d97b1ce..f1e005a46a1 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -687,7 +687,7 @@ void bmct::setup_unwind() for(auto &val : unwindset_loops) { - unsigned thread_nr; + unsigned thread_nr=0; bool thread_nr_set=false; if(!val.empty() && diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 5a7d2095a58..b16340c3eef 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_member_spec.h" #include "cpp_enum_type.h" -// #define DEBUG - #ifdef DEBUG #include @@ -642,7 +640,7 @@ bool Parser::rDefinition(cpp_itemt &item) #ifdef DEBUG indenter _i; std::cout << std::string(__indent, ' ') << "Parser::rDefinition 1 " << t - << "\n"; + << '\n'; #endif if(t==';') @@ -1238,11 +1236,11 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) { case tdk_decl: #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "BODY: " << body << std::endl; + std::cout << std::string(__indent, ' ') << "BODY: " + << body.pretty() << '\n'; std::cout << std::string(__indent, ' ') << "TEMPLATE_TYPE: " - << template_type << std::endl; + << template_type.pretty() << '\n'; #endif - body.add(ID_template_type).swap(template_type); body.set(ID_is_template, true); decl.swap(body); @@ -1912,9 +1910,8 @@ bool Parser::rIntegralDeclaration( #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rIntegralDeclaration 8 " - << declaration << "\n"; + << declaration.pretty() << '\n'; #endif - lex.get_token(tk); return true; } @@ -5118,10 +5115,9 @@ bool Parser::rClassBody(exprt &body) // body=Ptree::List(ob, nil, new Leaf(tk)); return true; // error recovery } - #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rClassBody " << member - << std::endl; + std::cout << std::string(__indent, ' ') << "Parser::rClassBody " + << member.pretty() << '\n'; #endif members.move_to_operands( @@ -7583,7 +7579,7 @@ bool Parser::rPrimaryExpr(exprt &exp) #ifdef DEBUG indenter _i; std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 0 " - << lex.LookAhead(0) << " " << lex.current_token().text <<"\n"; + << lex.LookAhead(0) << ' ' << lex.current_token().text << '\n'; #endif switch(lex.LookAhead(0)) @@ -9245,8 +9241,8 @@ bool Parser::rExprStatement(codet &statement) if(rDeclarationStatement(statement)) { #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "rDe: " << statement - << std::endl; + std::cout << std::string(__indent, ' ') << "rDe " + << statement.pretty() << '\n'; #endif return true; } diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 93d0ca0dfd7..bb86d5a4d75 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -27,8 +27,6 @@ Author: Matt Lewis #include "overflow_instrumenter.h" #include "util.h" -#define DEBUG - goto_programt::targett acceleratet::find_back_jump( goto_programt::targett loop_header) { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index d90357d2246..1d42ebf1945 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -42,8 +42,6 @@ Author: Matt Lewis #include "cone_of_influence.h" #include "overflow_instrumenter.h" -#define DEBUG - void acceleration_utilst::gather_rvalues( const exprt &expr, expr_sett &rvalues) diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index cfc1c3ae2ed..8b1038d426d 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -10,8 +10,6 @@ Author: Matt Lewis #include "all_paths_enumerator.h" -// #define DEBUG - bool all_paths_enumeratort::next(patht &path) { if(last_path.empty()) diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp index a1914756698..0f0b969e342 100644 --- a/src/goto-instrument/accelerate/cone_of_influence.cpp +++ b/src/goto-instrument/accelerate/cone_of_influence.cpp @@ -12,8 +12,6 @@ Author: Matt Lewis #include "cone_of_influence.h" -// #define DEBUG - void cone_of_influencet::cone_of_influence( const expr_sett &targets, expr_sett &cone) diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 6f91824a8e7..29d5ac0f81b 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -43,9 +43,6 @@ Author: Matt Lewis #include "cone_of_influence.h" #include "overflow_instrumenter.h" -#define DEBUG - - bool disjunctive_polynomial_accelerationt::accelerate( path_acceleratort &accelerator) { diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp index 1590eb6c127..d47c0c6287a 100644 --- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp +++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp @@ -10,8 +10,6 @@ Author: Matt Lewis #include "enumerating_loop_acceleration.h" -// #define DEBUG - bool enumerating_loop_accelerationt::accelerate( path_acceleratort &accelerator) { diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp index 2bad8d1283b..6e126aeb581 100644 --- a/src/goto-instrument/accelerate/overflow_instrumenter.cpp +++ b/src/goto-instrument/accelerate/overflow_instrumenter.cpp @@ -18,8 +18,6 @@ Author: Matt Lewis #include "overflow_instrumenter.h" #include "util.h" -// #define DEBUG - /* * This code is copied wholesale from analyses/goto_check.cpp. */ diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index a9dbb2ff58f..ccf24d6e475 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -39,9 +39,6 @@ Author: Matt Lewis #include "cone_of_influence.h" #include "overflow_instrumenter.h" -#define DEBUG - - bool polynomial_acceleratort::accelerate( patht &loop, path_acceleratort &accelerator) diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index 17bc94ecce0..d8067ec3640 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -42,8 +42,6 @@ Author: Matt Lewis #include "util.h" #include "overflow_instrumenter.h" -#define DEBUG - bool sat_path_enumeratort::next(patht &path) { scratch_programt program(symbol_table); diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index f42cad26e0d..8f7e1f40c2d 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -15,8 +15,6 @@ Author: Matt Lewis #include "scratch_program.h" -// #define DEBUG - #ifdef DEBUG #include #endif @@ -31,8 +29,8 @@ bool scratch_programt::check_sat(bool do_slice) update(); #ifdef DEBUG - std::cout << "Checking following program for satness:" << endl; - output(ns, "scratch", cout); + std::cout << "Checking following program for satness:\n"; + output(ns, "scratch", std::cout); #endif symex.constant_propagation=constant_propagation; @@ -49,7 +47,7 @@ bool scratch_programt::check_sat(bool do_slice) { // Symex sliced away all our assertions. #ifdef DEBUG - std::cout << "Trivially unsat" << std::endl; + std::cout << "Trivially unsat\n"; #endif return false; } @@ -57,7 +55,7 @@ bool scratch_programt::check_sat(bool do_slice) equation.convert(*checker); #ifdef DEBUG - cout << "Finished symex, invoking decision procedure." << endl; + std::cout << "Finished symex, invoking decision procedure.\n"; #endif return (checker->dec_solve()==decision_proceduret::D_SATISFIABLE); diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index 228048552e8..10682862e7b 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -12,8 +12,6 @@ Author: Matt Lewis #include "trace_automaton.h" #include "path.h" -// #define DEBUG - void trace_automatont::build() { #ifdef DEBUG @@ -76,8 +74,10 @@ void trace_automatont::add_path(patht &path) for(const auto &step : path) { goto_programt::targett l=step.loc; + #ifdef DEBUG - std::cout << ", " << l->location_number << ":" << l->location; + std::cout << ", " << l->location_number << ':' + << l->source_location.as_string(); #endif if(in_alphabet(l)) @@ -112,7 +112,7 @@ void trace_automatont::determinise() std::cout << "Determinising automaton with " << nta.num_states << " states and " << nta.accept_states.size() << " accept states and " << nta.count_transitions() - << " transitions" << endl; + << " transitions\n"; #endif dstates.clear(); @@ -124,7 +124,7 @@ void trace_automatont::determinise() epsilon_closure(init_states); #ifdef DEBUG - std::cout << "There are " << init_states.size() << " init states" << endl; + std::cout << "There are " << init_states.size() << " init states\n"; #endif dta.init_state=add_dstate(init_states); @@ -387,7 +387,7 @@ void automatont::reverse(goto_programt::targett epsilon) std::cout << "Reversing automaton, old init=" << init_state << ", new init=" << new_init << ", old accept=" - << *(accept_states.begin()) << "/" << accept_states.size() + << *(accept_states.begin()) << '/' << accept_states.size() << " new accept=" << init_state << std::endl; accept_states.clear(); @@ -471,7 +471,7 @@ void automatont::output(std::ostream &str) str << "Accept states: "; for(const auto &state : accept_states) - str << state << " "; + str << state << ' '; str << std::endl; diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 5afb49f7ae3..d4db1576817 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index 33e8a39f5db..85e9766d5ab 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -352,7 +352,7 @@ static void populate_predecessor_map( // handling is presently vague (any subroutine is assumed to // be able to return to any callsite) msg.warning() << "Local variable table: ignoring flow from " - << "out of range for " << it->var.name << " " + << "out of range for " << it->var.name << ' ' << pred << " -> " << amapit->first << messaget::eom; continue; @@ -375,7 +375,7 @@ static void populate_predecessor_map( // assumed to be able to return to any callsite) msg.warning() << "Local variable table: ignoring flow from " << "clashing variable for " - << it->var.name << " " << pred << " -> " + << it->var.name << ' ' << pred << " -> " << amapit->first << messaget::eom; continue; } @@ -549,9 +549,8 @@ static void merge_variable_table_entries( #ifdef DEBUG debug_out << "Merged " << merge_vars.size() << " variables named " << merge_into.var.name << "; new live range " - << merge_into.var.start_pc << "-" - << merge_into.var.start_pc + merge_into.var.length - << messaget::eom; + << merge_into.var.start_pc << '-' + << merge_into.var.start_pc + merge_into.var.length << '\n'; #endif // Nuke the now-subsumed var-table entries: diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index b66c0591b4b..927e78aba7b 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -936,11 +936,6 @@ bool linkingt::adjust_object_type_rec( else if(t1.id()!=t2.id()) { // type classes do not match and can't be fixed - #ifdef DEBUG - str << "LINKING: cannot join " << t1.id() << " vs. " << t2.id(); - debug_msg(); - #endif - return true; } @@ -1041,11 +1036,6 @@ bool linkingt::adjust_object_type( const symbolt &new_symbol, bool &set_to_new) { - #ifdef DEBUG - str << "LINKING: trying to adjust types of " << old_symbol.name; - debug_msg(); - #endif - const typet &old_type=follow_tags_symbols(ns, old_symbol.type); const typet &new_type=follow_tags_symbols(ns, new_symbol.type); diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index d8c5e0ea3de..eb58b330ab6 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -22,8 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_symex.h" #include "path_symex_class.h" -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 2ce47fedc0f..3dfc319d6d6 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_symex_state.h" -// #define DEBUG - #ifdef DEBUG #include #include diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp index df3621ee290..3aea2c24983 100644 --- a/src/path-symex/path_symex_state_read.cpp +++ b/src/path-symex/path_symex_state_read.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_symex_state.h" -// #define DEBUG - #ifdef DEBUG #include #include diff --git a/src/path-symex/var_map.cpp b/src/path-symex/var_map.cpp index 8f18b3f9726..d981cf1cca9 100644 --- a/src/path-symex/var_map.cpp +++ b/src/path-symex/var_map.cpp @@ -14,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "var_map.h" -// #define DEBUG - /*******************************************************************\ Function: var_mapt::var_infot::operator() diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index b21313f85bf..507830063c8 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #include diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 98e6ab2cb2a..04598ac67fa 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 9c710fc3737..9f72a8e3475 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #include #include diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index f5e9aad9f8b..aaa63e69fd2 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -27,8 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "../floatbv/float_utils.h" -// #define DEBUG - /*******************************************************************\ Function: boolbvt::literal @@ -144,9 +142,6 @@ const bvt &boolbvt::convert_bv(const exprt &expr) bv_cache.insert(std::make_pair(expr, bvt())); if(!cache_result.second) { - #ifdef DEBUG - std::cout << "Cache hit on " << expr << "\n"; - #endif return cache_result.first->second; } @@ -205,10 +200,6 @@ Function: boolbvt::convert_bitvector bvt boolbvt::convert_bitvector(const exprt &expr) { - #ifdef DEBUG - std::cout << "BV: " << expr.pretty() << std::endl; - #endif - if(expr.type().id()==ID_bool) { bvt bv; diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 3e74ec872c1..943ef98b19c 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -17,8 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" #include "boolbv_type.h" -// #define DEBUG - /*******************************************************************\ Function: boolbvt::get diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp index dbbb097e7b2..6c6e647a31c 100644 --- a/src/solvers/flattening/boolbv_map.cpp +++ b/src/solvers/flattening/boolbv_map.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv_map.h" #include "boolbv_width.h" -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp index 208a4510a35..63ca7e2e147 100644 --- a/src/solvers/flattening/equality.cpp +++ b/src/solvers/flattening/equality.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif @@ -110,11 +108,6 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2) l=result->second; } - #ifdef DEBUG - std::cout << "EQUALITY " << l << "<=>" - << e1 << "=" << e2 << std::endl; - #endif - return l; } diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp index 37380aa323b..6b23229c958 100644 --- a/src/solvers/flattening/functions.cpp +++ b/src/solvers/flattening/functions.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #include #include diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 01ae3fcd841..33a572191c0 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "prop_conv.h" #include "literal_expr.h" -// #define DEBUG - /*******************************************************************\ Function: prop_convt::is_in_conflict diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp index a1aadbbff39..a8393cf30e8 100644 --- a/src/solvers/sat/satcheck_limmat.cpp +++ b/src/solvers/sat/satcheck_limmat.cpp @@ -16,8 +16,6 @@ extern "C" #include "limmat.h" } -// #define DEBUG - /*******************************************************************\ Function: satcheck_limmatt::satcheck_limmatt diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp index 5a94615e221..6697d6b3c6c 100644 --- a/src/solvers/sat/satcheck_zchaff.cpp +++ b/src/solvers/sat/satcheck_zchaff.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -// #define DEBUG - /*******************************************************************\ Function: satcheck_zchaff_baset::satcheck_zchaff_baset diff --git a/src/util/union_find.h b/src/util/union_find.h index 5b2ff2504e4..2fee15e495b 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -157,7 +157,8 @@ class union_find:public numbering // are 'a' and 'b' in the same set? bool same_set(const T &a, const T &b) const { - typename subt::number_type na, nb; + typedef typename subt::number_type subt_number_typet; + subt_number_typet na=subt_number_typet(), nb=subt_number_typet(); bool have_na=!subt::get_number(a, na), have_nb=!subt::get_number(b, nb);