From 54594e6e7daecf143a18cbb8e1924e36ee5bca73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Dac=C3=ADk?= <xdacik00@stud.fit.vutbr.cz>
Date: Mon, 3 Mar 2025 17:43:37 +0100
Subject: [PATCH] [Translation] Add field introduction to heap encoding axioms

---
 src/translation/heap_encoding/ArrayEncoding.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/translation/heap_encoding/ArrayEncoding.ml b/src/translation/heap_encoding/ArrayEncoding.ml
index fdeb982..8a74e76 100644
--- a/src/translation/heap_encoding/ArrayEncoding.ml
+++ b/src/translation/heap_encoding/ArrayEncoding.ml
@@ -158,13 +158,24 @@ module Make (Locations : LOCATIONS) = struct
 
   (** === Axioms === *)
 
+  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 []
+    |> Boolean.mk_and
+
   (* Axioms enforced by location encoding *)
   let heap_axioms self =
     get_arrays self
     |> List.map (Locations.heap_axioms self.locs)
     |> Boolean.mk_and
 
-  (* Axioms enforced by heap encoding, currently none *)
-  let axioms self = heap_axioms self
+  (* Axioms enforced by heap encoding, currently just field introduction. *)
+  let axioms self =
+    Boolean.mk_and [
+      heap_axioms self;
+      field_intros self
+    ]
 
 end