diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c
index 0699a2b9..a87773ac 100644
--- a/harmony_model_checker/charm/charm.c
+++ b/harmony_model_checker/charm/charm.c
@@ -415,7 +415,6 @@ unsigned int check_finals(struct global *global, struct state *state, struct ste
 
     // Check each finally predicate
     for (unsigned int i = 0; i < global->nfinals; i++) {
-        assert(step->ctx->sp == 0);
         assert(!step->ctx->failed);
         // step->ctx->terminated = false;
         // ctx_failure(step->ctx) = 0;
diff --git a/harmony_model_checker/charm/graph.h b/harmony_model_checker/charm/graph.h
index a23fa608..2d34002a 100644
--- a/harmony_model_checker/charm/graph.h
+++ b/harmony_model_checker/charm/graph.h
@@ -54,7 +54,7 @@ struct edge {
     struct node *dst;        // destination node
     hvalue_t after;          // resulting context (TODO. index in dst context bag)
     struct access_info *ai;  // to detect data races
-    uint16_t inv;            // pc of invariant
+    int16_t inv;             // pc of invariant (negative if finally clause)
     uint16_t nsteps;         // # microsteps
     uint8_t ctx_index;       // index of context in src state context bag
     bool interrupt : 1;      // set if state change is an interrupt