From 4cb733bd3ca519b5815e793b3bdae0749055c602 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 19:59:58 +0000 Subject: [PATCH] SMT2: tolerate non-constant array indices when parsing array models smt2_convt::walk_array_tree assumes every (store array index value) term in a solver-returned array model has a constant index, calling to_constant_expr on it unconditionally. Models for unbounded or non-integer-keyed arrays can contain a non-constant index, which trips the to_constant_expr precondition. Skip such store entries during model reconstruction instead of aborting. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e5a7d4ff0f2..2b56ce535e8 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -637,6 +637,10 @@ void smt2_convt::walk_array_tree( // Recurse walk_array_tree(operands_map, src.get_sub()[1], type); const auto index_expr = parse_rec(src.get_sub()[2], type.size().type()); + if(!index_expr.is_constant()) + // Non-constant index (e.g. an unbounded / non-integer-keyed heap array + // from Strata's `Map Ref _`): skip this store in model reconstruction. + return; const constant_exprt index_constant = to_constant_expr(index_expr); mp_integer tempint; bool failure = to_integer(index_constant, tempint);