diff --git a/src/vcegar/abstractor.cpp b/src/vcegar/abstractor.cpp index 2102978c2..8a5597c8e 100644 --- a/src/vcegar/abstractor.cpp +++ b/src/vcegar/abstractor.cpp @@ -572,8 +572,9 @@ void abstractort::calc_abstract_trans_rel( throw "unexpected result from predabs_sat1.solve()"; } - print(9, "Generated "+ - i2string(trans_cube_set.no_insertions())+" cube(s)"); + debug() <<"Generated " + << i2string(trans_cube_set.no_insertions()) << " cube(s)" + << eom; if(show_cubes) std::cout << trans_cube_set; @@ -693,8 +694,9 @@ void abstractort::calc_abstract_initial_states( } // std::cout<<" The abstract transition relation \n"; - print(9, "Generated "+ - i2string(initial.no_insertions())+" cube(s)\n"); + debug() << "Generated " << + << i2string(initial.no_insertions()) <, " cube(s)\n" + << eom; if(show_cubes) std::cout << initial; diff --git a/src/vcegar/modelchecker_smv.cpp b/src/vcegar/modelchecker_smv.cpp index d5ccf95d1..922346208 100644 --- a/src/vcegar/modelchecker_smv.cpp +++ b/src/vcegar/modelchecker_smv.cpp @@ -164,7 +164,7 @@ bool modelchecker_smvt::read_result_cadence_smv( counterexample); - print(9, "Cadence SMV counterexample sucessfully read"); + debug() << "Cadence SMV counterexample sucessfully read" << eom; return false; } diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 03a98c7aa..0228639a1 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2026,6 +2026,9 @@ bool verilog_typecheck( message_handlert &message_handler, const namespacet &ns) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + verilog_typecheck_exprt verilog_typecheck_expr( ns, module_identifier, message_handler); @@ -2048,6 +2051,6 @@ bool verilog_typecheck( { verilog_typecheck_expr.error() << e << messaget::eom; } - - return verilog_typecheck_expr.get_error_found(); + + return message_handler.get_message_count(messaget::M_ERROR)!=errors_before; }