diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index 0a6117561..857604e79 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -87,7 +87,8 @@ predicate isrLockInv();
 fixpoint int taskISRLockID_f();
 
 predicate taskISRLockInv() = 
-    integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _)
+    integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
+    integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _)
     &*&
     // top ready priority must be in range
         integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&