From 6a0f30429bf96c3deb0ba82aef0d1b4049e069d6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 19:58:22 +0000 Subject: [PATCH] SMT2: skip element enumeration for non-integer-keyed array literals The array-constructor substitute in find_symbols enumerates element indices via from_integer(i, index_type), which is only valid for integer/bitvector index types. For arrays keyed by a non-scalar type, leave the array unconstrained (a sound over-approximation) rather than constructing an integer constant of a non-integer index type. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e5a7d4ff0f2..bf2f6ae1cee 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -5617,7 +5617,17 @@ void smt2_convt::find_symbols(const exprt &expr) convert_type(array_type); out << ")" << "\n"; - if(!is_zero_width(array_type.element_type(), ns)) + // Per-element constraints enumerate indices via from_integer(i, + // index_type); this is only possible for integer/bitvector index types. + // For arrays keyed by a non-scalar type (e.g. Strata's `Map Ref _`), we + // leave the array unconstrained (sound over-approximation). + const typet &idx_t = array_type.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 || + idx_t.id() == ID_c_bool; + if(!is_zero_width(array_type.element_type(), ns) && int_index) { for(std::size_t i = 0; i < expr.operands().size(); i++) {