Skip to content

Commit 7365b9a

Browse files
committed
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
1 parent 4fe3ade commit 7365b9a

File tree

2 files changed

+2
-1
lines changed

2 files changed

+2
-1
lines changed

regression/cbmc/array-cell-sensitivity12/test_execution.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE no-new-smt
1+
CORE
22
test.c
33

44
^VERIFICATION FAILED$

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -377,6 +377,7 @@ smt_termt
377377
smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
378378
{
379379
define_index_identifiers(expr);
380+
define_dependent_functions(expr);
380381
const exprt substituted = substitute_defined_padding(
381382
substitute_identifiers(expr, expression_identifiers));
382383
track_expression_objects(substituted, ns, object_map);

0 commit comments

Comments
 (0)