[Translation] Fix: add field introduction only for pointer fields

TDacik · Mar 3, 2025 · 3d68c5c · 3d68c5c
1 parent 54594e6
commit 3d68c5c
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/translation/heap_encoding/ArrayEncoding.ml b/src/translation/heap_encoding/ArrayEncoding.ml
@@ -161,8 +161,9 @@ module Make (Locations : LOCATIONS) = struct
   let field_intros self =
     let null = Locations.null self.locs in
     Field.Map.fold (fun field _ acc ->
-      Boolean.mk_eq [null; mk_succ self field null] :: acc
-      ) self.field_map []
+      if Field.is_pointer field then Boolean.mk_eq [null; mk_succ self field null] :: acc
+      else acc
+    ) self.field_map []
     |> Boolean.mk_and
 
   (* Axioms enforced by location encoding *)