diff -r 4ca1895adad8 -r 6c43ba091546 arch/arm/pistachio/include/tcb.h
--- a/arch/arm/pistachio/include/tcb.h
+++ b/arch/arm/pistachio/include/tcb.h
@@ -262,13 +262,18 @@
 
 INLINE bool tcb_t::in_exception_ipc(void)
 {
+    /*
+     * EXCEPTIONFP indicates the thread is doing a syscall exception ipc, this
+     * function returns true if the thread is either doing a syscall exception
+     * ipc, or a general exception ipc.
+     */
     return (resource_bits & (1UL << EXCEPTIONFP)) || (arch.exc_num != 0);
 }
 
 INLINE void tcb_t::clear_exception_ipc(void)
 {
     arch.exc_num = 0;
-    resource_bits & ~(1UL << EXCEPTIONFP);
+    resources.clear_except_fp(this);
 }
 
 /**
diff -r 4ca1895adad8 -r 6c43ba091546 arch/arm/pistachio/src/exception.cc
--- a/arch/arm/pistachio/src/exception.cc
+++ b/arch/arm/pistachio/src/exception.cc
@@ -533,7 +533,7 @@
     }
     /* XXX we should check if the kernel faulted */
 
-    if (EXPECT_TRUE(current->in_exception_ipc())) {
+    if (EXPECT_TRUE(current->resource_bits & (1UL << (word_t)EXCEPTIONFP))) {
 #ifdef CONFIG_ARM_THUMB_SUPPORT
         TRACEPOINT (EXCEPTION_IPC_SYSCALL,
                 word_t instr;
diff -r 4ca1895adad8 -r 6c43ba091546 arch/arm/pistachio/v5/src/traps.spp
--- a/arch/arm/pistachio/v5/src/traps.spp
+++ b/arch/arm/pistachio/v5/src/traps.spp
@@ -1847,7 +1847,13 @@
 #else
         // put current and sp to correct values
         sub     r9,     sp,     #OFS_TCB_ARCH_CONTEXT
+        /* We have to set EXCEPTIONFP in resource_bits to indicate it is a
+         * exception ipc.
+         */
+        ldr     r1,   [r9, #OFS_TCB_RESOURCE_BITS]       /* SET_RESRC */
         ldr     sp,     stack_top
+        orr     r1,   r1,   #EXCEPTIONFP_RESOURCE_BIT       /* SET_RESRC */
+        str     r1,   [r9, #OFS_TCB_RESOURCE_BITS]       /* SET_RESRC */
 #endif  /* EXCEPTION_FASTPATH */
 
 LABEL(exception_slowpath)
diff -r 4ca1895adad8 -r 6c43ba091546 arch/arm/pistachio/v6/src/traps.spp
--- a/arch/arm/pistachio/v6/src/traps.spp
+++ b/arch/arm/pistachio/v6/src/traps.spp
@@ -1885,7 +1885,14 @@
 #else
         // put current and sp to correct values
         sub     r9,     sp,     #OFS_TCB_ARCH_CONTEXT
+        /* We have to set EXCEPTIONFP in resource_bits to indicate it is a
+         * exception ipc.
+         */
+        ldr     r1,   [r9, #OFS_TCB_RESOURCE_BITS]       /* SET_RESRC */
+
         ldr     sp,     stack_top
+        orr     r1,   r1,   #EXCEPTIONFP_RESOURCE_BIT    /* SET_RESRC */
+        str     r1,   [r9, #OFS_TCB_RESOURCE_BITS]       /* SET_RESRC */
 #endif  /* EXCEPTION_FASTPATH */
 
 LABEL(exception_slowpath)