mcmini-gdb: fix "mcmini back"

gdbinit_commands.py

@@ -253,12 +253,10 @@ def invoke(self, args, from_tty):
       print("GDB is in scheduler, not target process:" +
             "  Can't go to previous transition\n")
       return
-    iterationsForward = transitionId - 1
-    gdb.execute("mcmini finishTrace quiet")
     gdb.execute("set rerunCurrentTraceForDebugger = 1")
-    gdb.execute("mcmini nextTrace quiet")
+    iterationsForward = transitionId - 1
+    transitionId = 0
     gdb.execute("mcmini forward " + str(iterationsForward) + " quiet")
-    gdb.execute("set rerunCurrentTraceForDebugger = 0")
     print("DEBUGGING: " + "mcmini forward " + str(iterationsForward) + " quiet")
     print_user_frames_in_stack()
     print_mcmini_stats()

src/mcmini_private.cpp

@@ -291,9 +291,21 @@ mc_do_model_checking()
 {
   mc_prepare_to_model_check_new_program();
 
-  int nextBranchPoint = mc_explore_branch(FIRST_BRANCH);
-  while (nextBranchPoint != FIRST_BRANCH) { // while not backtracked to origin
+  int nextBranchPoint = FIRST_BRANCH;
+  while (true) { // while not backtracked to origin
+    if (rerunCurrentTraceForDebugger && traceId == 0) {
+      // FIXME:  Should we just keep current state,and re-initialize it?
+      mc_prepare_to_model_check_new_program();
+      nextBranchPoint = FIRST_BRANCH;
+      traceId--;
+    } else {
+      mcprintf("WARNING:  rerunCurrentTraceForDebugger set with 'tracedId > 0'."
+               "  Ignored.\n");
+    }
+    rerunCurrentTraceForDebugger = false;
+
     nextBranchPoint = mc_explore_branch(nextBranchPoint);
+    // IFXME:  Do we need this?  It seems that it just returns the same value.
     nextBranchPoint = programState->getDeepestDPORBranchPoint();
   }
 }
@@ -570,6 +582,10 @@ mc_search_dpor_branch_with_thread(const tid_t backtrackThread)
       mc_stop_model_checking(EXIT_FAILURE);
     }
 
+    if (rerunCurrentTraceForDebugger) {
+      break;  // Stop this trace.  We'll rerun to it later.
+    }
+
     depth++;
     transitionId++;