From 4d2b0a73012c2ca73c4a74d082fe3b9ac9c8832c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 20:01:24 +0000 Subject: [PATCH] SMT2: disambiguate element-address functions by index type smt2_convt names the helper function emitted for ID_element_address as "element-address-", keyed on the result (pointer) type only. When two element_address expressions share a result type but have different index types, both the declaration and the application reuse the same function name with different argument sorts, so an SMT solver rejects the second application with an "unknown constant" sort-mismatch error. Include type2id(index_type) in the function name in both the application (convert_expr) and the declaration (find_symbols), and build the element size argument in an integer index type when the index type is not itself an integer/bitvector, so the declared and applied sorts always agree. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 40 ++++++++++++++++++++++++++++------ 1 file changed, 33 insertions(+), 7 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e5a7d4ff0f2..d76c4fb3128 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1923,15 +1923,30 @@ void smt2_convt::convert_expr(const exprt &expr) auto element_size_expr_opt = ::size_of_expr(element_address_expr.element_type(), ns); - CHECK_RETURN(element_size_expr_opt.has_value()); - - out << "(element-address-" << type2id(expr.type()) << ' '; + // The size/offset arithmetic requires an integer index type. Heap arrays + // keyed by a non-integer type (Strata `Map Ref _`) or with mathematical + // element types have neither a sensible byte size nor an integer index; + // fall back to an integer index type and unit size to avoid building a + // constant of a struct type. + const typet &idx_t = element_address_expr.index().type(); + const bool int_index = + idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv || + idx_t.id() == ID_bv || idx_t.id() == ID_integer || + idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag; + const typet size_target = int_index ? idx_t : c_index_type(); + const exprt element_size_expr = + element_size_expr_opt.has_value() + ? *element_size_expr_opt + : static_cast(from_integer(1, size_target)); + + out << "(element-address-" << type2id(expr.type()) << '_' << type2id(idx_t) + << ' '; convert_expr(element_address_expr.base()); out << ' '; convert_expr(element_address_expr.index()); out << ' '; - convert_expr(typecast_exprt::conditional_cast( - *element_size_expr_opt, element_address_expr.index().type())); + convert_expr( + typecast_exprt::conditional_cast(element_size_expr, size_target)); out << ')'; } else if(expr.id() == ID_field_address) @@ -5974,7 +5989,8 @@ void smt2_convt::find_symbols(const exprt &expr) } else if(expr.id() == ID_element_address) { - irep_idt function = "element-address-" + type2id(expr.type()); + irep_idt function = "element-address-" + type2id(expr.type()) + "_" + + type2id(to_element_address_expr(expr).index().type()); if(state_fkt_declared.insert(function).second) { @@ -5983,7 +5999,17 @@ void smt2_convt::find_symbols(const exprt &expr) out << ' '; convert_type(to_element_address_expr(expr).index().type()); out << ' '; // repeat, for the element size - convert_type(to_element_address_expr(expr).index().type()); + // The size argument is built as an integer (see convert_expr for + // ID_element_address); for non-integer (e.g. struct-keyed) index types + // we fall back to c_index_type rather than the index type itself. + { + const typet &idx_t = to_element_address_expr(expr).index().type(); + const bool int_index = + idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv || + idx_t.id() == ID_bv || idx_t.id() == ID_integer || + idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag; + convert_type(int_index ? idx_t : c_index_type()); + } out << ") "; convert_type(expr.type()); // return type out << ")\n"; // declare-fun