From 8359aff1bf65849f4b07c9d340892e3489957cf7 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 5 Jun 2024 06:57:41 -0700
Subject: [PATCH] array-bounds checks are now fatal

Accessing an array out of bounds is undefined behavior, and hence, the
assertions for this need to be fatal.
---
 src/ansi-c/goto-conversion/goto_check_c.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
index 3b3f702308f..bba18ac8964 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.cpp
+++ b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -1628,7 +1628,7 @@ void goto_check_ct::bounds_check_index(
           inequality,
           name + " lower bound",
           "array bounds",
-          false, // fatal
+          true, // fatal
           expr.find_source_location(),
           expr,
           guard);
@@ -1708,7 +1708,7 @@ void goto_check_ct::bounds_check_index(
       inequality,
       name + " upper bound",
       "array bounds",
-      false, // fatal
+      true, // fatal
       expr.find_source_location(),
       expr,
       guard);
@@ -1722,7 +1722,7 @@ void goto_check_ct::bounds_check_index(
       inequality,
       name + " upper bound",
       "array bounds",
-      false, // fatal
+      true, // fatal
       expr.find_source_location(),
       expr,
       guard);