From f77349fea912bcd4541922ac8dba88cc258875a2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 2 Jun 2025 10:50:05 +0000
Subject: [PATCH] Fix statement-expression expansion for Kani-provided
 quantifiers

CBMC side of https://github.com/model-checking/kani/issues/4020:
re-using the same converter instance would confuse finish-gotos (when
really we don't want gotos inside the statement expression to be
considered at all by the main goto-converter instances).
---
 .../Quantifiers-statement-expression1/main.c  | 21 +++++++++++++++++++
 .../test.desc                                 |  8 +++++++
 .../goto-conversion/goto_clean_expr.cpp       |  7 +++++--
 3 files changed, 34 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/Quantifiers-statement-expression1/main.c
 create mode 100644 regression/cbmc/Quantifiers-statement-expression1/test.desc

diff --git a/regression/cbmc/Quantifiers-statement-expression1/main.c b/regression/cbmc/Quantifiers-statement-expression1/main.c
new file mode 100644
index 00000000000..a940665bd59
--- /dev/null
+++ b/regression/cbmc/Quantifiers-statement-expression1/main.c
@@ -0,0 +1,21 @@
+int main()
+{
+  __CPROVER_assert(
+    __CPROVER_forall {
+      int i;
+      ({
+        goto out;
+        i == i;
+      })
+    },
+    "");
+  __CPROVER_assert(
+    __CPROVER_forall {
+      int i;
+      ({ i == i; })
+    },
+    "");
+out:
+
+  return 0;
+}
diff --git a/regression/cbmc/Quantifiers-statement-expression1/test.desc b/regression/cbmc/Quantifiers-statement-expression1/test.desc
new file mode 100644
index 00000000000..9bab40c8f03
--- /dev/null
+++ b/regression/cbmc/Quantifiers-statement-expression1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+goto label 'out' not found
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
index 4a605141902..5e49ce90f98 100644
--- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp
+++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
@@ -61,9 +61,11 @@ static exprt convert_statement_expression(
   const quantifier_exprt &qex,
   const code_expressiont &code,
   const irep_idt &mode,
-  goto_convertt &converter)
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
 {
   goto_programt where;
+  goto_convertt converter{symbol_table, message_handler};
   converter.goto_convert(code, where, mode);
   where.compute_location_numbers();
 
@@ -716,7 +718,8 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
       code.operands()[0].get_named_sub()[ID_statement].id() ==
         ID_statement_expression)
     {
-      auto res = convert_statement_expression(qex, code, mode, *this);
+      auto res = convert_statement_expression(
+        qex, code, mode, symbol_table, get_message_handler());
       qex.where() = res;
       return clean_expr(res, mode, result_is_used);
     }