diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/problems/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/problems/README.md
deleted file mode 100644
index 712ec2815..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/problems/README.md
+++ /dev/null
@@ -1,2 +0,0 @@
-This directory contains collection of problems encountered with VeriFast that
-need to be fixed in order to verify the current code base as is.
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/defining_header.h b/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/defining_header.h
deleted file mode 100644
index e63adcfa0..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/defining_header.h
+++ /dev/null
@@ -1,10 +0,0 @@
-#define ABC
-
-
-/*
-#ifdef ABC				// ok: evaluates to true
-    #error "ABC defined"		
-#else					// ok: evaluates to false
-    #error "ABC not defined"
-#endif
-*/
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/main.c b/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/main.c
deleted file mode 100644
index c71f3ef2f..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/main.c
+++ /dev/null
@@ -1,20 +0,0 @@
-/* Bug:
- * The header `defining_header.h` defines the constant `ABC` and
- * the header `testing_header.h` checks whether `ABC` has been defined.
- * In `testing_header.h` both checks `#ifdef ABC` and its negation
- * `#ifndef ABC` evaluate to true.
- */
-
-#include "defining_header.h"
-
-
-/*
-#ifdef ABC			// ok: evaluates to true
-    #error "ABC defined"		
-#else				// ok: evaluates to false
-    #error "ABC not defined"
-#endif
-*/
-
-
-#include "testing_header.h"
\ No newline at end of file
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/testing_header.h b/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/testing_header.h
deleted file mode 100644
index 9add91a69..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/problems/bugs/define_name/testing_header.h
+++ /dev/null
@@ -1,17 +0,0 @@
-// Problem: Both branches branch conditions evaluate to true.
-
-/* `main.c` included this header after including `defining_header.h`.
- * Hence, `#ifdef ABC` should evaluate to true and `#ifndef ABC should
- * evaluate to false.
- */
-
-/*
-#ifdef ABC			// ok: evaluates to true.
-    #error "ABC defined"	
-#endif
-*/
-
-
-#ifndef ABC			// bug: evaluates to true
-    #error "ABC defined"
-#endif
\ No newline at end of file
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--original.sh b/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--original.sh
deleted file mode 100755
index 5e5c9bc2a..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--original.sh
+++ /dev/null
@@ -1,90 +0,0 @@
-
-# This script must be run from the directory in which it resides,
-# i.e., `FreeRTOS-Kernel/verification/verifast`.
-
-
-
-
-VFIDE="$1"
-echo Path to vfide binary : "\'$VFIDE\'"
-
-
-SOURCE_DIR="../.."
-HEADER_DIR="$SOURCE_DIR/include"
-
-TASK_H="$HEADER_DIR/task.h"
-TASKS_C="$SOURCE_DIR/tasks.c"
-
-PROOF_SETUP_DIR="proof_setup"
-GENERATED_HEADERS_DIR="$PROOF_SETUP_DIR/generated"
-
-RP2040_CONFIG_DIR="$SOURCE_DIR/portable/ThirdParty/GCC/RP2040/include"
-
-FREERTOS_SMP_DEMO_DIR="demos/FreeRTOS-SMP-Demos"
-
-PICO_SDK_DIR="sdks/pico-sdk"
-
-
-# We replaced the following include paths:
-# `$FREERTOS_SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/build/generated/pico_base`
-# ->
-# `$GENERATED_HEADERS_DIR/pico_base`
-
-
-
-"$VFIDE" -I "$HEADER_DIR" \
--I $PROOF_SETUP_DIR -D VERIFAST "$TASKS_C" \
--I $RP2040_CONFIG_DIR \
--I $PICO_SDK_DIR/src/common/pico_base/include \
--I $GENERATED_HEADERS_DIR/pico_base \
--I $PICO_SDK_DIR/src/boards/include \
--I $PICO_SDK_DIR/src/rp2_common/cmsis/include \
--I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/OnEitherCore \
--I $PICO_SDK_DIR/src/rp2040/hardware_regs/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_base/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_clocks/include \
--I $PICO_SDK_DIR/src/rp2040/hardware_structs/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_claim/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_sync/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_gpio/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_irq/include \
--I $PICO_SDK_DIR/src/common/pico_sync/include \
--I $PICO_SDK_DIR/src/common/pico_time/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_timer/include \
--I $PICO_SDK_DIR/src/common/pico_util/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_resets/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_pll/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_vreg/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_watchdog/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_xosc/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_exception/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_multicore/include \
--I $PICO_SDK_DIR/src/common/pico_stdlib/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_uart/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_divider/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_runtime/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_printf/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_bootrom/include \
--I $PICO_SDK_DIR/src/common/pico_bit_ops/include \
--I $PICO_SDK_DIR/src/common/pico_divider/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_double/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_int64_ops/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_float/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_malloc/include \
--I $PICO_SDK_DIR/src/rp2_common/boot_stage2/include \
--I $PICO_SDK_DIR/src/common/pico_binary_info/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_stdio/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_stdio_uart/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_stdio_usb/include \
--I $PICO_SDK_DIR/lib/tinyusb/src \
--I $PICO_SDK_DIR/lib/tinyusb/src/common \
--I $PICO_SDK_DIR/lib/tinyusb/hw \
--I $PICO_SDK_DIR/src/rp2_common/pico_fix/rp2040_usb_device_enumeration/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_unique_id/include \
--I $PICO_SDK_DIR/src/rp2_common/hardware_flash/include \
--I $PICO_SDK_DIR/src/common/pico_usb_reset_interface/include \
--I $PICO_SDK_DIR/src/rp2_common/pico_platform/include/
-
-# Defines used during the built of the FreeRTOS SMP Demo that might be relevant
-# in the future:
-# -D CFG_TUSB_DEBUG=0 -D CFG_TUSB_MCU=OPT_MCU_RP2040 -D CFG_TUSB_OS=OPT_OS_PICO -D FREE_RTOS_KERNEL_SMP=1 -D LIB_FREERTOS_KERNEL=1 -D LIB_PICO_BIT_OPS=1 -D LIB_PICO_BIT_OPS_PICO=1 -D LIB_PICO_DIVIDER=1 -D LIB_PICO_DIVIDER_HARDWARE=1 -D LIB_PICO_DOUBLE=1 -D LIB_PICO_DOUBLE_PICO=1 -D LIB_PICO_FIX_RP2040_USB_DEVICE_ENUMERATION=1 -D LIB_PICO_FLOAT=1 -D LIB_PICO_FLOAT_PICO=1 -D LIB_PICO_INT64_OPS=1 -D LIB_PICO_INT64_OPS_PICO=1 -D LIB_PICO_MALLOC=1 -D LIB_PICO_MEM_OPS=1 -D LIB_PICO_MEM_OPS_PICO=1 -D LIB_PICO_MULTICORE=1 -D LIB_PICO_PLATFORM=1 -D LIB_PICO_PRINTF=1 -D LIB_PICO_PRINTF_PICO=1 -D LIB_PICO_RUNTIME=1 -D LIB_PICO_STANDARD_LINK=1 -D LIB_PICO_STDIO=1 -D LIB_PICO_STDIO_UART=1 -D LIB_PICO_STDIO_USB=1 -D LIB_PICO_STDLIB=1 -D LIB_PICO_SYNC=1 -D LIB_PICO_SYNC_CORE=1 -D LIB_PICO_SYNC_CRITICAL_SECTION=1 -D LIB_PICO_SYNC_MUTEX=1 -D LIB_PICO_SYNC_SEM=1 -D LIB_PICO_TIME=1 -D LIB_PICO_UNIQUE_ID=1 -D LIB_PICO_UTIL=1 -D PICO_BOARD=\"pico\" -D PICO_BUILD=1 -D PICO_CMAKE_BUILD_TYPE=\"Release\" -D PICO_COPY_TO_RAM=0 -D PICO_CXX_ENABLE_EXCEPTIONS=0 -D PICO_NO_FLASH=0 -D PICO_NO_HARDWARE=0 -D PICO_ON_DEVICE=1 -D PICO_TARGET_NAME=\"on_core_zero\" -D PICO_USE_BLOCKED_RAM=0 \