From ac7c276300166664dc2b1f143ebfd8d5ea9c3ccb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 28 Mar 2026 20:13:07 +0000 Subject: [PATCH] SMT2 Incremental: Resolve duplicate and missing declarations Guard send_function_definition against duplicate declare-fun commands by checking identifier_table before sending. Guard define_index_identifiers against duplicate define-fun commands by checking expression_identifiers before defining. Ensure array element dependencies are declared before assertions by calling define_dependent_functions on elements in initialize_array_elements for both array_exprt and array_of_exprt. Remove no-new-smt tag from byte_extract1, Initialization6, and Pointer_byte_extract4 regression tests that now pass with the fix. Fixes: #8072 --- regression/cbmc/Initialization6/test.desc | 2 +- regression/cbmc/Pointer_byte_extract4/program-only.desc | 2 +- regression/cbmc/Pointer_byte_extract4/test.desc | 2 +- regression/cbmc/byte_extract1/test.desc | 2 +- .../smt2_incremental_decision_procedure.cpp | 9 +++++++++ 5 files changed, 13 insertions(+), 4 deletions(-) diff --git a/regression/cbmc/Initialization6/test.desc b/regression/cbmc/Initialization6/test.desc index 028f7170892..33900ad2b78 100644 --- a/regression/cbmc/Initialization6/test.desc +++ b/regression/cbmc/Initialization6/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^EXIT=10$ diff --git a/regression/cbmc/Pointer_byte_extract4/program-only.desc b/regression/cbmc/Pointer_byte_extract4/program-only.desc index c3b3f95041f..7b738a3b40b 100644 --- a/regression/cbmc/Pointer_byte_extract4/program-only.desc +++ b/regression/cbmc/Pointer_byte_extract4/program-only.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract4/test.desc b/regression/cbmc/Pointer_byte_extract4/test.desc index 1c039664a91..9efefbc7362 100644 --- a/regression/cbmc/Pointer_byte_extract4/test.desc +++ b/regression/cbmc/Pointer_byte_extract4/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/byte_extract1/test.desc b/regression/cbmc/byte_extract1/test.desc index ecf6bd304bc..d80821ffede 100644 --- a/regression/cbmc/byte_extract1/test.desc +++ b/regression/cbmc/byte_extract1/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^EXIT=10$ diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0d8a91a6f89..f4ada079d0f 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -111,6 +111,10 @@ void smt2_incremental_decision_proceduret::initialize_array_elements( identifier_table.emplace(array_identifier.identifier(), array_identifier); const std::vector &elements = array.operands(); const typet &index_type = array.type().index_type(); + for(const auto &element : elements) + { + define_dependent_functions(element); + } for(std::size_t i = 0; i < elements.size(); ++i) { const smt_termt index = convert_expr_to_smt(from_integer(i, index_type)); @@ -125,6 +129,7 @@ void smt2_incremental_decision_proceduret::initialize_array_elements( const array_of_exprt &array, const smt_identifier_termt &array_identifier) { + define_dependent_functions(array.what()); const smt_sortt index_type = convert_type_to_smt_sort(array.type().index_type()); const smt_identifier_termt array_index_identifier{ @@ -170,6 +175,8 @@ void send_function_definition( &expression_identifiers, std::unordered_map &identifier_table) { + if(identifier_table.count(symbol_identifier)) + return; const smt_declare_function_commandt function{ smt_identifier_termt( symbol_identifier, convert_type_to_smt_sort(expr.type())), @@ -342,6 +349,8 @@ void smt2_incremental_decision_proceduret::define_index_identifiers( if(const auto with_expr = expr_try_dynamic_cast(expr_node)) { const auto index_expr = with_expr->where(); + if(expression_identifiers.count(index_expr)) + return; const auto index_term = convert_expr_to_smt(index_expr); const auto index_identifier = "index_" + std::to_string(index_sequence());