diff --git a/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h index e36a82ae54..454291682f 100644 --- a/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h +++ b/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h @@ -43,7 +43,7 @@ *----------------------------------------------------------*/ #define configENABLE_BACKWARD_COMPATIBILITY 1 #define configUSE_PREEMPTION 1 -#define configUSE_PORT_OPTIMISED_TASK_SELECTION 1 +#define configUSE_PORT_OPTIMISED_TASK_SELECTION 0 #define configMAX_PRIORITIES ( 7 ) #define configTICK_RATE_HZ ( 1000 ) /* In this non-real time simulated environment the tick frequency has to be at least a multiple of the Win32 tick frequency, and therefore very slow. */ #define configMINIMAL_STACK_SIZE ( ( unsigned short ) 60 ) /* In this simulated case, the stack only has to hold one small structure as the real stack is part of the Win32 thread. */