diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h b/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h
index ea247e406..539a22e88 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h
@@ -112,10 +112,10 @@
         @*/                                                                                               \
         {                                                                                                 \
             /*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/                                       \
-            /*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack,                                 \
+            /*@ assert( stack_p(?pxStack, ?ulStackDepth, ?pxTopOfStack,                                 \
                         ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) );                                 \
              @*/                                                                                          \
-            /*@ open stack_p_2(_, _, _, _, _, _); @*/                                                     \
+            /*@ open stack_p(_, _, _, _, _, _); @*/                                                     \
             /* The detour below allows us to skip proving that `ulFreeBytes`                              \
              * is a multiple of `sizeof(StackType_t)`.                                                    \
              */                                                                                           \
@@ -136,7 +136,7 @@
                 /*@ integers__to_chars(pxStack); @*/                                                      \
         	    /*@ chars_join((char*) pxStack); @*/                                                      \
         	    /*@ chars_split((char*) pxStack, ulFreeBytesOnStack); @*/                                 \
-        	    /*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack,                                  \
+        	    /*@ close stack_p(pxStack, ulStackDepth, pxTopOfStack,                                  \
                                     ulFreeBytes, ulUsedCells, ulUnalignedBytes);                          \
                 @*/                                                                                       \
         	    /*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/                                  \
@@ -149,7 +149,7 @@
                 integers__to_chars(pxStack);                                                              \
         	    chars_join((char*) pxStack);                                                              \
         	    chars_split((char*) pxStack, ulFreeBytesOnStack);                                         \
-        	    close stack_p_2(pxStack, ulStackDepth, pxTopOfStack,                                      \
+        	    close stack_p(pxStack, ulStackDepth, pxTopOfStack,                                      \
                                 ulFreeBytes, ulUsedCells, ulUnalignedBytes);                              \
         	    close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack);                                          \
             }                                                                                             \
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/stack_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/stack_predicates.h
index 7bf3e41c9..3941beec8 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/stack_predicates.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/stack_predicates.h
@@ -4,7 +4,7 @@
 
 /*@
 // Represents a stack that grows down (cf. RP2040 stack)
-predicate stack_p_2(StackType_t * pxStack, 
+predicate stack_p(StackType_t * pxStack, 
                     uint32_t ulStackDepth, 
                     StackType_t * pxTopOfStack, 
                     uint32_t ulFreeBytes,
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h
index d412714d4..f34ed7a1d 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h
@@ -15,7 +15,7 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
     malloc_block_tskTaskControlBlock(tcb) &*&
     tcb->pxStack |-> ?stackPtr &*&
     tcb->pxTopOfStack |-> ?topPtr &*&
-    stack_p_2(stackPtr, ?ulStackDepth, topPtr, 
+    stack_p(stackPtr, ?ulStackDepth, topPtr, 
               ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*&
 
     xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*&
@@ -63,7 +63,7 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
 predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) =
     tcb->pxStack |-> ?stackPtr &*&
     tcb->pxTopOfStack |-> ?topPtr &*&
-    stack_p_2(stackPtr, ?ulStackDepth, topPtr, 
+    stack_p(stackPtr, ?ulStackDepth, topPtr, 
               ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes);
 
 // This predicate represents a shared part of a TCB that can be accessed by