diff --git a/include/list.h b/include/list.h
index 332f3f413..2e4d45823 100644
--- a/include/list.h
+++ b/include/list.h
@@ -56,6 +56,20 @@
 #ifndef LIST_H
 #define LIST_H
 
+
+#ifdef VERIFAST
+    /* Reason for rewrite:
+     * VeriFast bug:
+     * Both `#ifdef INC_FREERTOS_H` and its negation `#ifdef INC_FREERTOS_H`
+     * evaluate to true. See minimal example `define_name`.
+     */
+    #define INC_FREERTOS_H
+    /* Remember that this header is included indirectly `tasks.c` after it
+     * includes `FreeRTOS.h`.
+     */
+    // TODO: Remove this work-around once VF has been fixed.
+#endif /* VERIFAST */
+
 #ifndef INC_FREERTOS_H
     #error "FreeRTOS.h must be included before list.h"
 #endif
diff --git a/include/task.h b/include/task.h
index 65cd86e8d..410f9283b 100644
--- a/include/task.h
+++ b/include/task.h
@@ -28,6 +28,20 @@
 #ifndef INC_TASK_H
 #define INC_TASK_H
 
+#ifdef VERIFAST
+    /* Reason for rewrite:
+     * VeriFast bug:
+     * Both `#ifdef INC_FREERTOS_H` and its negation `#ifdef INC_FREERTOS_H`
+     * evaluate to true. See minimal example `define_name`.
+     */
+    #define INC_FREERTOS_H
+    /* Remember that this header is included by `tasks.c` after it includes
+     * `FreeRTOS.h`.
+     */
+    // TODO: Remove this work-around once VF has been fixed.
+#endif /* VERIFAST */
+
+
 #ifndef INC_FREERTOS_H
     #error "include FreeRTOS.h must appear in source files before include task.h"
 #endif