diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json index 2788b60ec1..d2d1ab1f39 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json @@ -30,6 +30,15 @@ "ENTRY": "TaskResumeAll", "DEF": [ + { "default": + [ + "FREERTOS_MODULE_TEST", + "PENDED_TICKS=1", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ] + }, { "useTickHook1": [ "FREERTOS_MODULE_TEST",