goto-symex: support struct-keyed arrays (maps) in value materialisation

src/goto-symex/field_sensitivity.cpp

@@ -350,6 +350,21 @@ exprt field_sensitivityt::get_fields(
       return ssa_expr;
 
     const array_typet &type = to_array_type(ssa_expr.type());
+    // Element enumeration below builds integer indices via from_integer(i,
+    // index_type). If the index type is not an integer/bitvector/enum (e.g. a
+    // map keyed by a struct reference, as in Strata's heap model `Map Ref _`),
+    // we cannot enumerate elements this way; treat the array monolithically.
+    {
+      const typet &idx_t = type.index_type();
+      if(
+        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 && idx_t.id() != ID_bool)
+      {
+        return ssa_expr;
+      }
+    }
     const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
 
     array_exprt::operandst elements;
@@ -628,7 +643,19 @@ bool field_sensitivityt::is_divisible(
     numeric_cast_v<mp_integer>(to_constant_expr(
       to_array_type(expr.type()).size())) <= max_field_sensitivity_array_size)
   {
-    return true;
+    // Only field-decompose arrays whose index type is an integer/bitvector/enum
+    // (element enumeration builds from_integer(i, index_type)). Arrays keyed by
+    // a non-scalar type (e.g. Strata's `Map Ref _` heap, indexed by a struct
+    // reference) must be handled monolithically.
+    const typet &idx_t = to_array_type(expr.type()).index_type();
+    if(
+      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 || idx_t.id() == ID_bool)
+    {
+      return true;
+    }
   }
 #endif
 

src/goto-symex/field_sensitivity.h

@@ -204,6 +204,10 @@ class field_sensitivityt
   [[nodiscard]] bool
   is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
 
+  /// Whether field sensitivity is currently enabled (can be temporarily
+  /// disabled for quantifier bodies to preserve algebraic structure).
+  bool enabled = true;
+
 private:
   const std::size_t max_field_sensitivity_array_size;
 

src/pointer-analysis/value_set.cpp

@@ -1593,8 +1593,11 @@ void value_sett::assign(
     else
     {
       DATA_INVARIANT(
-        rhs.type() == lhs.type(),
-        "value_sett::assign types should match, got: "
+        rhs.type() == lhs.type() ||
+          (rhs.type().id() == ID_array && lhs.type().id() == ID_array &&
+           to_array_type(rhs.type()).element_type() ==
+             to_array_type(lhs.type()).element_type()),
+        "value_sett::assign types should match (modulo array size), got: "
         "rhs.type():\n" +
           rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());