From d0d633a5243e7fb07693e16ee6449abecf645997 Mon Sep 17 00:00:00 2001
From: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Wed, 7 Apr 2021 12:26:03 -0700
Subject: [PATCH] Reintroduce quarantined CBMC test (#516)

This CBMC test would go over the memory limit of most hosts, causing the
kernel to kill the process. With larger memory capabilities, this can be
re-enabled.
---
 .../CBMC/proofs/Task/TaskResumeAll/Configurations.json   | 9 +++++++++
 1 file changed, 9 insertions(+)

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",