From ae1204d608ec8be482cedd40320432f477f5cdde Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Tue, 28 Nov 2023 10:55:33 +0100
Subject: [PATCH] Let meet in UnionDomain.Map throw Uncomparable in case
 different fields are set. Fixes an issue where meet in branch refinement
 yielded bot on unions where different fields were set.

---
 src/cdomains/unionDomain.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
index 92d694756a..2a94592db5 100644
--- a/src/cdomains/unionDomain.ml
+++ b/src/cdomains/unionDomain.ml
@@ -192,6 +192,16 @@ struct
   let join =
     Map.join
 
+  let meet a b =
+    if a == b then
+      a
+    else
+      let merge_pair _ x y = match x, y with
+        | Some x, Some y -> Some (Values.meet x y)
+        | _, _ -> raise Lattice.Uncomparable
+      in
+      Map.merge merge_pair a b
+
   (** Performs join or widen operation using per element merge function *)
   let merge ~merge_values x y =
     if is_top x || is_top y then