Improve goto-synthesizer debug output

Author: qinheping

src/goto-synthesizer/cegis_verifier.cpp

@@ -600,11 +600,11 @@ optionalt<cext> cegis_verifiert::verify()
   // Annotate assigns
   annotate_assigns(assigns_map, goto_model);
 
-  // Control verbosity.
-  // We allow non-error output message only when verbosity is set to at least 9.
+  // Control verbosity. We allow non-error output message only when verbosity
+  // is set to larger than messaget::M_DEBUG.
   const unsigned original_verbosity = log.get_message_handler().get_verbosity();
-  if(original_verbosity < 9)
-    log.get_message_handler().set_verbosity(1);
+  if(original_verbosity < messaget::M_DEBUG)
+    log.get_message_handler().set_verbosity(messaget::M_ERROR);
 
   // Apply loop contracts we annotated.
   code_contractst cont(goto_model, log);
@@ -630,7 +630,7 @@ optionalt<cext> cegis_verifiert::verify()
   // Run the checker to get the result.
   const resultt result = (*checker)();
 
-  if(original_verbosity >= 9)
+  if(original_verbosity >= messaget::M_DEBUG)
     checker->report();
 
   // Restore the verbosity.
@@ -698,6 +698,8 @@ optionalt<cext> cegis_verifiert::verify()
   // although there can be multiple ones.
 
   log.debug() << "Start to compute cause loop ids." << messaget::eom;
+  log.debug() << "Violation description: " << target_violation_info.description
+              << messaget::eom;
 
   const auto &trace = checker->get_traces()[target_violation];
   // Doing assigns-synthesis or invariant-synthesis

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -120,6 +120,7 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
       }
     }
   }
+  log.debug() << "Finished candidates initialization." << messaget::eom;
 }
 
 void enumerative_loop_contracts_synthesizert::synthesize_assigns(
@@ -303,6 +304,8 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
     // generate candidate and verify
     for(auto strengthening_candidate : start_bool_ph.enumerate(size_bound))
     {
+      log.progress() << "Verifying candidate: "
+                     << format(strengthening_candidate) << messaget::eom;
       seen_terms++;
       invariant_mapt new_in_clauses = invariant_mapt(in_invariant_clause_map);
       new_in_clauses[cause_loop_id] =
@@ -351,6 +354,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
   // Set of symbols we used to enumerate strengthening clauses.
   std::vector<exprt> terminal_symbols;
 
+  log.debug() << "Start the first synthesis iteration." << messaget::eom;
   auto return_cex = verifier.verify();
 
   while(return_cex.has_value())