Fix smtprc-tid unsoundness

goblint · Oct 26, 2023 · ec49852 · ec49852
1 parent e4bf5ac
commit ec49852
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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! *)