From af75445579141d42e722f600e9927638f16f8056 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 20:56:27 +0000 Subject: [PATCH] goto-check: skip array bounds checks for unbounded (non-constant-size) arrays An array whose size is not a constant denotes an unbounded array; emitting an array-bounds check over its (non-constant/nil) size is meaningless and cannot be lowered to SMT. Skip the bounds check in that case. Co-authored-by: Kiro --- src/ansi-c/goto-conversion/goto_check_c.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index ad0419853a9..43e03284d7c 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -1593,6 +1593,12 @@ void goto_check_ct::bounds_check_index( throw "bounds check expected array or vector type, got " + array_type.id_string(); + // Skip bounds checking for unbounded arrays (no constant size). + if( + array_type.id() == ID_array && + !to_array_type(array_type).size().is_constant()) + return; + std::string name = array_name(expr.array()); const exprt &index = expr.index();