From 7365b9a94ebfb665c6f11f538c433ac64a78607e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 17:14:45 +0100 Subject: [PATCH] Fix array_exprt handling in incremental SMT2 procedure The call to `define_dependent_functions` ensures that `array_exprt` expressions are properly handled and their dependent functions are defined before the expression conversion process begins. Fixes: #8080 --- regression/cbmc/array-cell-sensitivity12/test_execution.desc | 2 +- .../smt2_incremental/smt2_incremental_decision_procedure.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/array-cell-sensitivity12/test_execution.desc b/regression/cbmc/array-cell-sensitivity12/test_execution.desc index 70141323480..d33e4045438 100644 --- a/regression/cbmc/array-cell-sensitivity12/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity12/test_execution.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE test.c ^VERIFICATION FAILED$ diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0d8a91a6f89..00cfcf0bab2 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -377,6 +377,7 @@ smt_termt smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr) { define_index_identifiers(expr); + define_dependent_functions(expr); const exprt substituted = substitute_defined_padding( substitute_identifiers(expr, expression_identifiers)); track_expression_objects(substituted, ns, object_map);