diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c
index 1d41d327..a71dd5fa 100644
--- a/harmony_model_checker/charm/charm.c
+++ b/harmony_model_checker/charm/charm.c
@@ -1497,7 +1497,9 @@ void path_recompute(struct global *global){
             pid = global->oldpid;
         }
         else {
+            // printf("Search for %p\n", (void *) ctx);
             for (pid = 0; pid < global->nprocesses; pid++) {
+                // printf("%d: %p\n", pid, (void *) global->processes[pid]);
                 if (global->processes[pid] == ctx) {
                     break;
                 }
@@ -1508,6 +1510,9 @@ void path_recompute(struct global *global){
             printf("PID %p %u %u\n", (void *) ctx, pid, global->nprocesses);
             panic("bad pid");
         }
+        else {
+            // printf("Found %d\n", pid);
+        }
         assert(pid < global->nprocesses);
 
         macro->tid = pid;
@@ -1527,6 +1532,8 @@ void path_recompute(struct global *global){
         );
         assert(global->processes[pid] == e->after || e->after == 0);
 
+        // printf("Set %d to %p\n", pid, (void *) e->after);
+
         // Copy thread state
         macro->nprocesses = global->nprocesses;
         macro->processes = copy(global->processes, global->nprocesses * sizeof(hvalue_t));
@@ -3701,6 +3708,8 @@ int exec_model_checker(int argc, char **argv){
 
     printf("* Phase 3: analysis\n");
 
+    bool computed_components = false;
+
     // If no failures were detected (yet), determine strongly connected components
     // and look for non-terminating states.
     if (global->failures == NULL) {
@@ -3710,6 +3719,7 @@ int exec_model_checker(int argc, char **argv){
         }
         double now = gettime();
         tarjan(global);
+        computed_components = true;
 
         // Compute shortest path to initial state for each node.
         shortest_path(global);
@@ -3931,7 +3941,10 @@ int exec_model_checker(int argc, char **argv){
                 struct node *node = global->graph.nodes[i];
                 assert(node->id == i);
                 fprintf(df, "\nNode %d:\n", node->id);
-                fprintf(df, "    component: %d\n", node->u.ph2.component);
+                if (computed_components) {
+                    fprintf(df, "    component: %d\n", node->u.ph2.component);
+                }
+                fprintf(df, "    len to parent: %d\n", node->u.ph2.len);
                 if (node->u.ph2.u.to_parent != NULL) {
                     fprintf(df, "    ancestors:");
                     for (struct node *n = node->u.ph2.u.to_parent->src;; n = n->u.ph2.u.to_parent->src) {
@@ -3942,7 +3955,21 @@ int exec_model_checker(int argc, char **argv){
                     }
                     fprintf(df, "\n");
                 }
-                fprintf(df, "    vars: %s\n", value_string(node_state(node)->vars));
+                struct state *state = node_state(node);
+                fprintf(df, "    vars: %s\n", value_string(state->vars));
+                fprintf(df, "    contexts:\n");
+                for (unsigned int i = 0; i < state->bagsize; i++) {
+                    fprintf(df, "      %"PRI_HVAL": %u\n", state_contexts(state)[i], multiplicities(state)[i]);
+                }
+                if (state->stopbag != VALUE_DICT) {
+                    fprintf(df, "    stopbag:\n");
+                    unsigned int size;
+                    hvalue_t *vals = value_get(state->stopbag, &size);
+                    size /= 2 * sizeof(hvalue_t);
+                    for (unsigned int i = 0; i < size; i++) {
+                        fprintf(df, "      %"PRI_HVAL": %d\n", vals[2*i], (int) VALUE_FROM_INT(vals[2*i+1]));;
+                    }
+                }
                 // fprintf(df, "    len: %u %u\n", node->len, node->steps);
                 if (node->failed) {
                     fprintf(df, "    failed\n");
@@ -4058,7 +4085,9 @@ int exec_model_checker(int argc, char **argv){
                 }
                 fprintf(out, "    {\n");
                 fprintf(out, "      \"idx\": %d,\n", node->id);
-                fprintf(out, "      \"component\": %d,\n", node->u.ph2.component);
+                if (computed_components) {
+                    fprintf(out, "      \"component\": %d,\n", node->u.ph2.component);
+                }
 #ifdef notdef
                 if (node->parent != NULL) {
                     fprintf(out, "      \"parent\": %d,\n", node->parent->id);
diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c
index 704eb394..86cd1f04 100644
--- a/harmony_model_checker/charm/ops.c
+++ b/harmony_model_checker/charm/ops.c
@@ -1375,11 +1375,26 @@ void op_Go(
     ctx_push(copy, result);
     copy->stopped = false;
     // TODO.  Check success of context_add
-    context_add(state, value_put_context(&step->engine, copy));
+    hvalue_t context = value_put_context(&step->engine, copy);
+    context_add(state, context);
 #ifdef HEAP_ALLOC
     free(buffer);
 #endif
     step->ctx->pc++;
+
+    if (step->keep_callstack) {
+        // Find the process
+        unsigned int pid;
+        for (pid = 0; pid < global->nprocesses; pid++) {
+            if (global->processes[pid] == ctx) {
+                global->processes[pid] = context;
+                break;
+            }
+        }
+        if (pid >= global->nprocesses) {
+            panic("op_Go: can't find process");
+        }
+    }
 }
 
 void op_Finally(const void *env, struct state *state, struct step *step, struct global *global){
@@ -2147,6 +2162,7 @@ void op_Spawn(
             global->processes = realloc(global->processes, (global->nprocesses + 1) * sizeof(hvalue_t));
             global->callstacks = realloc(global->callstacks, (global->nprocesses + 1) * sizeof(struct callstack *));
             global->processes[global->nprocesses] = context;
+            // printf("Add %d %p\n", global->nprocesses, (void *) context);
             struct callstack *cs = new_alloc(struct callstack);
             cs->pc = pc;
             cs->arg = arg;
diff --git a/harmony_model_checker/charm/value.c b/harmony_model_checker/charm/value.c
index d9f7dcd2..add28689 100644
--- a/harmony_model_checker/charm/value.c
+++ b/harmony_model_checker/charm/value.c
@@ -1747,9 +1747,11 @@ void context_remove(struct state *state, hvalue_t ctx){
                         (char *) &state_contexts(state)[state->bagsize + 1] + i + 1,
                         state->bagsize - i);
             }
-            break;
+            return;
         }
     }
+    // TODO. this can happen with invariant contexts
+    // panic("context_remove: can't find context");
 }
 
 // Add context 'ctx' to the state's context bag.  May fail if there are too
diff --git a/runall.py b/runall.py
index 7f78ca7a..a576f35a 100644
--- a/runall.py
+++ b/runall.py
@@ -17,7 +17,7 @@
     { "args": "code/naiveTurn.hny", "issue": "Non-terminating state", "nstates": 28 },
     { "args": "code/Peterson.hny", "issue": "No issues", "nstates": 104 },
     { "args": "code/PetersonBroken.hny", "issue": "Safety violation", "nstates": 126 },
-    { "args": "code/PetersonInductive.hny", "issue": "No Issues", "nstates": 4 },
+    { "args": "code/PetersonInductive.hny", "issue": "No issues", "nstates": 104 },
     { "args": "code/csonebit.hny", "issue": "Active busy waiting", "nstates": 73 },
     { "args": "code/PetersonMethod.hny", "issue": "No issues", "nstates": 104 },
     { "args": "code/hanoi.hny", "issue": "Safety violation", "nstates": 28 },
@@ -29,7 +29,7 @@
     { "args": "-msynch=synchS code/UpLock.hny", "issue": "No issues", "nstates": 58 },
     { "args": "code/spinlock.hny", "issue": "No issues", "nstates": 473 },
     { "args": "code/xy.hny", "issue": "Safety violation", "nstates": 19 },
-    { "args": "code/atm.hny", "issue": "Safety violation", "nstates": 128 },
+    { "args": "code/atm.hny", "issue": "Invariant violation", "nstates": 1832 },
     { "args": "code/queuedemo.hny", "issue": "No issues", "nstates": 80 },
     { "args": "code/setobjtest.hny", "issue": "No issues", "nstates": 217 },
     { "args": "-msetobj=linkedlist code/setobjtest.hny", "issue": "No issues", "nstates": 9495 },
@@ -44,7 +44,7 @@
     { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 },
     { "args": "-B queue4.hfa -m queue=queueconc code/qtestpar.hny", "issue": "No issues", "nstates": 66530 },
     { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 },
-    { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 },
+    { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "No issues", "nstates": 99816 },
     { "args": "-mqueue=queuebroken code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 },
     { "args": "code/RWtest.hny", "issue": "No issues", "nstates": 135 },
     { "args": "-mRW=RWsbs code/RWtest.hny", "issue": "No issues", "nstates": 1757 },
@@ -84,7 +84,7 @@
     { "args": "-msynch=synchS code/trap6.hny", "issue": "No issues", "nstates": 554 },
     { "args": "code/hw.hny", "issue": "No issues", "nstates": 23864 },
     { "args": "code/abptest.hny", "issue": "No issues", "nstates": 2778 },
-    { "args": "code/leader.hny", "issue": "Safety violation", "nstates": 117 },
+    { "args": "code/leader.hny", "issue": "No issues", "nstates": 33005 },
     { "args": "-mstack=stack1 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
     { "args": "-mstack=stack2 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
     { "args": "-mstack=stack3 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
@@ -106,8 +106,9 @@
             if t["issue"] != hco["issue"]:
                 print("Different issue (was %s)???  Aborting further tests" % t["issue"])
                 break
-            if min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9:
+            if t["issue"] != "Safety violation" and min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9:
                 print("#states very different (was %d)???  Aborting further tests" % t["nstates"])
+                break
     else:
         print("Error code %d, aborting further tests" % cp.returncode)
         print("Output: ", cp.stdout)