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);