diff --git a/tasks.c b/tasks.c
index 5266b0bfa..ff0e1c062 100644
--- a/tasks.c
+++ b/tasks.c
@@ -6680,4 +6680,4 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
         }
     #endif
 
-#endif /* if ( configINCLUDE_FREERTOS_TASK_C_ADDITIONS_H == 1 ) */
+#endif /* if ( configINCLUDE_FREERTOS_TASK_C_ADDITIONS_H == 1 ) */
\ No newline at end of file
diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c
index c61aa3fd7..d8b060f4e 100644
--- a/verification/verifast/preprocessed_files/tasks--pp.c
+++ b/verification/verifast/preprocessed_files/tasks--pp.c
@@ -60,40 +60,40 @@ typedef intptr_t ptrdiff_t;
 typedef intptr_t ssize_t;
 // # 5 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/malloc.h" 2
 
-/*@
-
-// In Standard C, freeing a null pointer is allowed and is a no-op.
-lemma_auto void malloc_block_null();
-    requires emp;
-    ensures malloc_block(0, 0);
-
-lemma void malloc_block_limits(void *array);
-    requires [?f]malloc_block(array, ?size);
-    ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX;
-
+/*@
+
+// In Standard C, freeing a null pointer is allowed and is a no-op.
+lemma_auto void malloc_block_null();
+    requires emp;
+    ensures malloc_block(0, 0);
+
+lemma void malloc_block_limits(void *array);
+    requires [?f]malloc_block(array, ?size);
+    ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX;
+
 @*/
 
 void *malloc(size_t size);
     //@ requires true;
-    /*@
-    ensures
-        result == 0 ?
-            emp
-        :
-            chars_(result, size, _) &*& malloc_block(result, size) &*&
-            (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow
+    /*@
+    ensures
+        result == 0 ?
+            emp
+        :
+            chars_(result, size, _) &*& malloc_block(result, size) &*&
+            (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow
     @*/
     //@ terminates;
 
 void *calloc(size_t nmemb, size_t size);
     //@ requires true;
-    /*@
-    ensures
-        result == 0 ?
-            emp
-        :
-            chars(result, nmemb * size, ?cs) &*& malloc_block(result, nmemb * size) &*& all_eq(cs, 0) == true &*&
-            (char *)0 < result && result + nmemb * size <= (char *)UINTPTR_MAX; // one-past-end does not overflow
+    /*@
+    ensures
+        result == 0 ?
+            emp
+        :
+            chars(result, nmemb * size, ?cs) &*& malloc_block(result, nmemb * size) &*& all_eq(cs, 0) == true &*&
+            (char *)0 < result && result + nmemb * size <= (char *)UINTPTR_MAX; // one-past-end does not overflow
     @*/
     //@ terminates;
 
@@ -104,16 +104,16 @@ void free(void *array);
 
 void *realloc(void *array, size_t newSize);
     //@ requires malloc_block(array, ?size) &*& chars(array, size, ?cs);
-    /*@
-    ensures
-        result == 0 ?
-            malloc_block(array, size) &*& chars(array, size, cs)
-        :
-            malloc_block(result, newSize) &*&
-            newSize <= size ?
-                chars(result, _, take(newSize, cs))
-            :
-                chars(result, _, cs) &*& chars(result + size, newSize - size, _);
+    /*@
+    ensures
+        result == 0 ?
+            malloc_block(array, size) &*& chars(array, size, cs)
+        :
+            malloc_block(result, newSize) &*&
+            newSize <= size ?
+                chars(result, _, take(newSize, cs))
+            :
+                chars(result, _, cs) &*& chars(result + size, newSize - size, _);
     @*/
     //@ terminates;
 // # 6 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/stdlib.h" 2
@@ -158,21 +158,21 @@ void memcpy(void *array, void *array0, size_t count);
     //@ ensures chars(array, count, cs0) &*& [f]chars(array0, count, cs0);
 
 void memmove(void *dest, void *src, size_t count);
-    /*@
-    requires
-        chars(src, count, ?cs) &*&
-        dest <= src ?
-            chars(dest, src - dest, _)
-        :
-            chars(src + count, dest - src, _);
+    /*@
+    requires
+        chars(src, count, ?cs) &*&
+        dest <= src ?
+            chars(dest, src - dest, _)
+        :
+            chars(src + count, dest - src, _);
     @*/
-    /*@
-    ensures
-        chars(dest, count, cs) &*&
-        dest <= src ?
-            chars(dest + count, src - dest, _)
-        :
-            chars(src, dest - src, _);
+    /*@
+    ensures
+        chars(dest, count, cs) &*&
+        dest <= src ?
+            chars(dest + count, src - dest, _)
+        :
+            chars(src, dest - src, _);
     @*/
 
 size_t strlen(char *string);
@@ -193,15 +193,15 @@ char *memchr(char *array, char c, size_t count);
 
 char* strchr(char *str, char c);
     //@ requires [?f]string(str, ?cs);
-    /*@ ensures
-            [f]string(str, cs) &*&
-            c == 0 ? 
-                result == str + length(cs)
-            : 
-                result == 0 ?
-                    mem(c, cs) == false
-                :
-                    mem(c, cs) == true &*& result == str + index_of(c, cs);
+    /*@ ensures
+            [f]string(str, cs) &*&
+            c == 0 ? 
+                result == str + length(cs)
+            : 
+                result == 0 ?
+                    mem(c, cs) == false
+                :
+                    mem(c, cs) == true &*& result == str + index_of(c, cs);
     @*/
 
 void* memset(void *array, char value, size_t size);
@@ -548,33 +548,33 @@ typedef void (* TaskFunction_t)( void * );
  * must be set in the compiler's include path. */
 
 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 1
-/*
- * FreeRTOS SMP Kernel V202110.00
- * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
- * Copyright (c) 2021 Raspberry Pi (Trading) Ltd.
- *
- * SPDX-License-Identifier: MIT AND BSD-3-Clause
- *
- * Permission is hereby granted, free of charge, to any person obtaining a copy of
- * this software and associated documentation files (the "Software"), to deal in
- * the Software without restriction, including without limitation the rights to
- * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
- * the Software, and to permit persons to whom the Software is furnished to do so,
- * subject to the following conditions:
- *
- * The above copyright notice and this permission notice shall be included in all
- * copies or substantial portions of the Software.
- *
- * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
- * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
- * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
- * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
- * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
- * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
- *
- * https://www.FreeRTOS.org
- * https://github.com/FreeRTOS
- *
+/*
+ * FreeRTOS SMP Kernel V202110.00
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (c) 2021 Raspberry Pi (Trading) Ltd.
+ *
+ * SPDX-License-Identifier: MIT AND BSD-3-Clause
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 // # 37 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h"
 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/sdks/pico-sdk/src/common/pico_base/include/pico.h" 1
@@ -4283,14 +4283,14 @@ int spin_lock_claim_unused(bool required);
 bool spin_lock_is_claimed(uint lock_num);
 // # 39 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 2
 
-/*-----------------------------------------------------------
- * Port specific definitions.
- *
- * The settings in this file configure FreeRTOS correctly for the
- * given hardware and compiler.
- *
- * These settings should not be altered.
- *-----------------------------------------------------------
+/*-----------------------------------------------------------
+ * Port specific definitions.
+ *
+ * The settings in this file configure FreeRTOS correctly for the
+ * given hardware and compiler.
+ *
+ * These settings should not be altered.
+ *-----------------------------------------------------------
  */
 
 /* Type definitions. */
@@ -4306,7 +4306,7 @@ bool spin_lock_is_claimed(uint lock_num);
         typedef uint32_t TickType_t;
 
 
-/* 32-bit tick type on a 32-bit architecture, so reads of the tick count do
+/* 32-bit tick type on a 32-bit architecture, so reads of the tick count do
  * not need to be guarded with a critical section. */
 
 
@@ -4317,13 +4317,13 @@ bool spin_lock_is_claimed(uint lock_num);
 
 
 
-        /* Reason for rewrite: VeriFast does not support the attriibute `used`. 
+        /* Reason for rewrite: VeriFast does not support the attriibute `used`. 
          */
 
 
 
 
-    /* We have to use PICO_DIVIDER_DISABLE_INTERRUPTS as the source of truth rathern than our config,
+    /* We have to use PICO_DIVIDER_DISABLE_INTERRUPTS as the source of truth rathern than our config,
      * as our FreeRTOSConfig.h header cannot be included by ASM code - which is what this affects in the SDK */
 
 
@@ -4388,11 +4388,11 @@ bool spin_lock_is_claimed(uint lock_num);
 
 
 
-    /* Note this is a single method with uxAcquire parameter since we have
-     * static vars, the method is always called with a compile time constant for
+    /* Note this is a single method with uxAcquire parameter since we have
+     * static vars, the method is always called with a compile time constant for
      * uxAcquire, and the compiler should dothe right thing! */
 
-        /* Reason for rewrite: VeriFast does not support local static variables.
+        /* Reason for rewrite: VeriFast does not support local static variables.
          */
 // # 226 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h"
 /*-----------------------------------------------------------*/
@@ -9973,9 +9973,12 @@ predicate stack_p_2(StackType_t * pxStack,
     // pxTopOfStack points to the last sizeof(StackType_t) number of bytes.
     (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) &*&
     // Used stack cells
-    integers_(pxTopOfStack + sizeof(StackType_t), sizeof(StackType_t), false, ulUsedCells, _) &*&
+    integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*&
     // Unaligned rest
-    chars((char*) pxTopOfStack + sizeof(StackType_t) * (ulUsedCells + 1), ulUnalignedBytes, _);
+    //unalignedRestOfStack_p((char*) pxStack + freeBytes, ulUsedCells, ulUnalignedBytes);
+    true;
+
+
 @*/
 
 /*@
@@ -10402,7 +10405,6 @@ StackType_t* test_stack_pred(uint32_t depth)
 }
 // -------------------------------------------------
 
-
 /*
  * See header file for description.
  */
@@ -10410,43 +10412,111 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
                                      TaskFunction_t pxCode,
                                      void * pvParameters )
 /*@ requires pxTopOfStack > 0 &*&
-             stack_p(?pxStack, ?ulStackDepth, pxTopOfStack, ulStackDepth) &*&
-             ulStackDepth > 16;
+             stack_p_2(?pxStack, ?ulStackDepth, pxTopOfStack, ?ulFreeBytes, 
+                       ?ulUsedCells, ?ulUnalignedBytes) &*&
+             ulFreeBytes > 17 * sizeof(StackType_t) &*&
+             pxStack > 0;
   @*/
-//@ ensures stack_p(pxStack, ulStackDepth, pxTopOfStack-16, ulStackDepth-16);
+/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes, 
+                       			    ulUsedCells, ulUnalignedBytes);
+@*/
 {
-    //@ StackType_t* oldTop = pxTopOfStack;
-    //@ open stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth);
-    ///@ close stack_p(pxStack, ulStackDepth, pxTopOfStack-1, ulStackDepth-1);
-    ///@ getTopOfStack(pxStack, pxTopOfStack-1);
-    //@ integers__split(pxStack, ulStackDepth-2);
-
+    //@ StackType_t* gOldTop = pxTopOfStack;
+    //@ char* gcStack = (char*) pxStack;
+    //@ open stack_p_2(_, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) );
+    //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // skip stack cell #0
+    //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t));
+    //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop);
     /* Simulate the stack frame as it would be created by a context switch
      * interrupt. */
     pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // make stack cell #1 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2));
+    //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop-1);
     *pxTopOfStack = ( 0x01000000 ); /* xPSR */
+    //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _);
     pxTopOfStack--;
-    //@ close integers_(oldTop-1, sizeof(StackType_t), false, 2, _);
-    //@ integers__join(pxStack);
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // prevent overflow
     //@ ptr_range<void>(pxCode);
-    //@ integers__split(pxStack, ulStackDepth-3);
+    // make stack cell #2 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 3));
+    //@ chars_to_integers_(gOldTop-2, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop-2);
     *pxTopOfStack = ( StackType_t ) pxCode; /* PC */
-    //@ close integers_(oldTop-2, sizeof(StackType_t), false, 3, _);
+    //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _);
     pxTopOfStack--;
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // prevent underflow
     //@ ptr_range<void>(prvTaskExitError);
-    //@ integers__join(pxStack);
-    //@ integers__split(pxStack, ulStackDepth-4);
+    // make stack cell #3 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 4));
+    //@ chars_to_integers_(gOldTop-3, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop-3);
     *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */
-    //@ close integers_(oldTop-3, sizeof(StackType_t), false, 4, _);
-    //@ integers__join(pxStack);
+    //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _);
+    
     pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // prevent overflow
     //@ ptr_range<void>(pvParameters);
-    //@ integers__split(pxStack, ulStackDepth-9);
+    // make stack cell #8 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9));
+    //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 5);
+    //@ integers__join(gOldTop-8);
     *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
-    //@ close integers_(oldTop-8, sizeof(StackType_t), false, 9, _);
-    //@ integers__join(pxStack);
+    //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _);
+    
+    
+    // skip stack cells #9 - #15, leave #16 unused
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 17));
+    //@ chars_to_integers_(gOldTop-16, sizeof(StackType_t), false, 8);
+    //@ integers__join(gOldTop-16);
     pxTopOfStack -= 8; /* R11..R4. */
-    //@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth-16);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    
+    
+    
+    //@close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - (sizeof(StackType_t) * 16),  ulUsedCells, ulUnalignedBytes);
+    
     return pxTopOfStack;
 }
 // # 66 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2
diff --git a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c
index fad6c90bc..6c2789141 100644
--- a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c
+++ b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c
@@ -105,7 +105,6 @@ StackType_t* test_stack_pred(uint32_t depth)
 }
 // -------------------------------------------------
 
-
 /*
  * See header file for description.
  */
@@ -113,42 +112,110 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
                                      TaskFunction_t pxCode,
                                      void * pvParameters )
 /*@ requires pxTopOfStack > 0 &*&
-             stack_p(?pxStack, ?ulStackDepth, pxTopOfStack, ulStackDepth) &*&
-             ulStackDepth > 16;
+             stack_p_2(?pxStack, ?ulStackDepth, pxTopOfStack, ?ulFreeBytes, 
+                       ?ulUsedCells, ?ulUnalignedBytes) &*&
+             ulFreeBytes > 17 * sizeof(StackType_t) &*&
+             pxStack > 0;
   @*/
-//@ ensures stack_p(pxStack, ulStackDepth, pxTopOfStack-16, ulStackDepth-16);
+/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes, 
+                       			    ulUsedCells, ulUnalignedBytes);
+@*/
 {
-    //@ StackType_t* oldTop = pxTopOfStack;
-    //@ open stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth);
-    ///@ close stack_p(pxStack, ulStackDepth, pxTopOfStack-1, ulStackDepth-1);
-    ///@ getTopOfStack(pxStack, pxTopOfStack-1);
-    //@ integers__split(pxStack, ulStackDepth-2);
-
+    //@ StackType_t* gOldTop = pxTopOfStack;
+    //@ char* gcStack = (char*) pxStack;
+    //@ open stack_p_2(_, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) );
+    //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // skip stack cell #0
+    //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t));
+    //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop);
     /* Simulate the stack frame as it would be created by a context switch
      * interrupt. */
-    pxTopOfStack--;                                          /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
-    *pxTopOfStack = portINITIAL_XPSR;                        /* xPSR */
+    pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // make stack cell #1 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2));
+    //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop-1);
+    *pxTopOfStack = ( 0x01000000 ); /* xPSR */
+    //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _);
     pxTopOfStack--;
-    //@ close integers_(oldTop-1, sizeof(StackType_t), false, 2, _);
-    //@ integers__join(pxStack);
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // prevent overflow
     //@ ptr_range<void>(pxCode);
-    //@ integers__split(pxStack, ulStackDepth-3);
-    *pxTopOfStack = ( StackType_t ) pxCode;                  /* PC */
-    //@ close integers_(oldTop-2, sizeof(StackType_t), false, 3, _);
+    // make stack cell #2 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 3));
+    //@ chars_to_integers_(gOldTop-2, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop-2);
+    *pxTopOfStack = ( StackType_t ) pxCode; /* PC */
+    //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _);
     pxTopOfStack--;
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // prevent underflow
     //@ ptr_range<void>(prvTaskExitError);
-    //@ integers__join(pxStack);
-    //@ integers__split(pxStack, ulStackDepth-4);
-    *pxTopOfStack = ( StackType_t ) portTASK_RETURN_ADDRESS; /* LR */
-    //@ close integers_(oldTop-3, sizeof(StackType_t), false, 4, _);
-    //@ integers__join(pxStack);
-    pxTopOfStack -= 5;                                       /* R12, R3, R2 and R1. */
+    // make stack cell #3 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 4));
+    //@ chars_to_integers_(gOldTop-3, sizeof(StackType_t), false, 1);
+    //@ integers__join(gOldTop-3);
+    *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */
+    //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _);
+    
+    pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
+    
+    // Ensure maintining stack invariant
+    //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes);
+    //@ open stack_p_2(pxStack, _, _, _, _, _);
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    // prevent overflow
     //@ ptr_range<void>(pvParameters);
-    //@ integers__split(pxStack, ulStackDepth-9);
-    *pxTopOfStack = ( StackType_t ) pvParameters;            /* R0 */
-    //@ close integers_(oldTop-8, sizeof(StackType_t), false, 9, _);
-    //@ integers__join(pxStack);
-    pxTopOfStack -= 8;                                       /* R11..R4. */
-    //@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth-16);
+    // make stack cell #8 available
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9));
+    //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 5);
+    //@ integers__join(gOldTop-8);
+    *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
+    //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _);
+    
+    
+    // skip stack cells #9 - #15, leave #16 unused
+    //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 17));
+    //@ chars_to_integers_(gOldTop-16, sizeof(StackType_t), false, 8);
+    //@ integers__join(gOldTop-16);
+    pxTopOfStack -= 8; /* R11..R4. */
+    
+    //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) );
+    //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) );
+    
+    
+    
+    
+    //@close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - (sizeof(StackType_t) * 16),  ulUsedCells, ulUnalignedBytes);
+    
     return pxTopOfStack;
 }
\ No newline at end of file
diff --git a/verification/verifast/proof/stack_predicates.h b/verification/verifast/proof/stack_predicates.h
index 41ca97100..b42666477 100644
--- a/verification/verifast/proof/stack_predicates.h
+++ b/verification/verifast/proof/stack_predicates.h
@@ -21,8 +21,14 @@ predicate stack_p_2(StackType_t * pxStack,
     // pxTopOfStack points to the last sizeof(StackType_t) number of bytes.
     (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) &*&
     // Used stack cells
-    integers_(pxTopOfStack + sizeof(StackType_t), sizeof(StackType_t), false, ulUsedCells, _) &*&
+    integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*&
     // Unaligned rest
+    //unalignedRestOfStack_p(pxTopOfStack, ulUsedCells, ulUnalignedBytes);
+    true; // skip unaligned part for now
+
+predicate unalignedRestOfStack_p(StackType_t * pxTopOfStack,
+                                 uint32_t ulUsedCells,
+                                 uint32_t ulUnalignedBytes) =
     chars((char*) pxTopOfStack + sizeof(StackType_t) * (ulUsedCells + 1), ulUnalignedBytes, _);
 @*/