From f588952411561efe6ced9d6aa2b02dd704007681 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 6 Jun 2024 09:17:34 +0000
Subject: [PATCH] Make explicit that stringBuilder CBMC proof is bounded

With CBMC v6, unwinding assertions are enabled by default.
---
 test/cbmc/proofs/stringBuilder/Makefile | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/stringBuilder/Makefile b/test/cbmc/proofs/stringBuilder/Makefile
index 30dc77a99..421657092 100644
--- a/test/cbmc/proofs/stringBuilder/Makefile
+++ b/test/cbmc/proofs/stringBuilder/Makefile
@@ -10,9 +10,11 @@ DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET +=
+UNWINDSET += stringBuilder_harness.0:10
+UNWINDSET += stringBuilder_harness.1:10
+UNWINDSET += stringBuilder.0:10
 
-CBMC_FLAG_UNWINDING_ASSERTIONS =
+CBMC_FLAG_UNWINDING_ASSERTIONS = --no-unwinding-assertions
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c