diff --git a/src/cdomains/preValueDomain.ml b/src/cdomains/preValueDomain.ml
index 44b3d274e7..21523c5bb9 100644
--- a/src/cdomains/preValueDomain.ml
+++ b/src/cdomains/preValueDomain.ml
@@ -4,28 +4,24 @@ module IndexDomain = IntDomain.IntDomWithDefaultIkind (ID) (IntDomain.PtrDiffIki
 module Offs = struct
   include Offset.MakeLattice (IndexDomain)
 
-  (** Add the [additional_offset] to the [base_offset]. In case [additional_offset] starts with an index offset, merge this index with the last index occurring in [base_offset]. *)
+  (** Add the [additional_offset] to the [base_offset]. In case [additional_offset] starts with an index offset, merge this index with the index occurring at the end of [base_offset], if any. *)
   let rec add_offset_merge_index_offset ~(base_offset: t) ~(additional_offset: t): t =
     match additional_offset with
     | `NoOffset -> base_offset
     | `Field (f,o) -> add_offset base_offset additional_offset
     | `Index (i,o) ->
       let rec add_offset_index_merged o = match o with
-        | `NoOffset -> false, additional_offset
+        | `NoOffset -> additional_offset
         | `Field (f1,o1) ->
-          let merged, offs = add_offset_index_merged o1 in
-          merged, `Field (f1, offs)
-        | `Index (i1,o1) ->
-          let merged, offs = add_offset_index_merged o1 in
-          let offs = if merged then
-              `Index (i, offs)
-            else
-              `Index (IndexDomain.add i1 i, o1)
-          in
-          true, offs
+          let offs = add_offset_index_merged o1 in
+          `Field (f1, offs)
+        | `Index (i1, `NoOffset) ->
+          `Index (IndexDomain.add i1 i, `NoOffset)
+        | `Index (i1, o1) ->
+          let offs = add_offset_index_merged o1 in
+          `Index (i, offs)
       in
-      let _, offs = add_offset_index_merged base_offset in
-      offs
+      add_offset_index_merged base_offset
 end
 
 module Mval = Mval.MakeLattice (Offs)