From ec49852dbc981143f73b81672cd802fc99aca884 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 20 Sep 2023 17:47:35 +0300
Subject: [PATCH] Fix smtprc-tid unsoundness

---
 src/analyses/base.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 7b87d3ff51..84bd7ebe21 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -399,6 +399,8 @@ struct
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
         | IndexPI when AD.to_string p2 = ["all_index"] ->
           addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
+        | IndexPI | PlusPI ->
+          addToAddrOp p1 (AD.to_int p2) (* sometimes index is AD for some reason... *)
         | _ -> VD.top ()
       end
     (* For other values, we just give up! *)