Retrace show default choice as Retrace*

Author: lks9

src/goto-symex/symex_goto.cpp

@@ -227,7 +227,6 @@ renamedt<exprt, L2> try_evaluate_pointer_comparisons(
   return condition;
 }
 
-
 void goto_symext::symex_goto(statet &state)
 {
   PRECONDITION(state.reachable);
@@ -648,15 +647,18 @@ void goto_symext::symex_goto_retrace(statet &state)
 
   // goto or next depends on input trace from user
   bool choose_goto;
+  bool default_choice;
   static int retrace_index = 0;
   if (retrace_index < static_cast<int>(symex_config.retrace_input.size()))
   {
     choose_goto = symex_config.retrace_input[retrace_index] == '1';
+    default_choice = false;
     retrace_index++;
   }
   else
   {
-    choose_goto = false; // default
+    choose_goto = false;
+    default_choice = true;
   }
 
   // print goto choice
@@ -685,12 +687,13 @@ void goto_symext::symex_goto_retrace(statet &state)
     auto nt_line = nt_dest.get_line();
     if(nt_line.empty()) nt_line = "?";
 
+    std::string mode = default_choice ? "Retrace* " : "Retrace ";
     std::string desc = choose_goto ? "1/GOTO" : "0/NEXT";
 
     std::string padding_1 = std::string(abs(3-cur_line.size()), ' ');
     std::string padding_2 = std::string(abs(3-t_line.size()), ' ');
 
-    log.status() << "Retrace " << desc
+    log.status() << mode << desc
                  << " at " << cur_file << ":" << cur_line << padding_1
                  << " to " << t_file << ":" << t_line << padding_2
                  << " (not " << nt_file << ":" << nt_line << ")"
@@ -782,7 +785,6 @@ void goto_symext::symex_goto_retrace(statet &state)
   return;
 }
 
-
 bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
 {
   // dummy implementation