From 9e26114ea1737530027a76ba07d6982a29d576d5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 3 Nov 2023 12:33:59 +0200
Subject: [PATCH] Fix var_eq not limiting to queried lval invariants

---
 src/analyses/varEq.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 30b36404af..63cf48860b 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -566,7 +566,15 @@ struct
       r
     | Queries.Invariant context when GobConfig.get_bool "witness.invariant.exact" -> (* only exact equalities here *)
       let scope = Node.find_fundec ctx.node in
-      D.invariant ~scope ctx.local
+      if Lval.Set.is_top context.lvals then
+        D.invariant ~scope ctx.local
+      else (
+        Lval.Set.fold (fun lval acc ->
+            match D.find_class (Lval lval) ctx.local with
+            | None -> acc
+            | Some c -> Invariant.(acc && D.invariant ~scope (D.singleton c))
+          ) context.lvals (Invariant.top ())
+      )
     | _ -> Queries.Result.top x
 
   let event ctx e octx =