diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index bc5330726c..e99aefa0e5 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -34,8 +34,8 @@ struct
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
     let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
-    let ls = ctx.ask reach_or_mpt in
-    ctx.emit (Access {exp=e; lvals=ls; kind; reach})
+    let ad = ctx.ask reach_or_mpt in
+    ctx.emit (Access {exp=e; ad; kind; reach})
 
   (** Three access levels:
       + [deref=false], [reach=false] - Access [exp] without dereferencing, used for all normal reads and all function call arguments.
@@ -137,25 +137,20 @@ struct
 
   let event ctx e octx =
     match e with
-    | Events.Access {lvals; kind; _} when !collect_local && !AnalysisState.postsolving ->
-      begin match lvals with
-        | ls when Queries.LS.is_top ls ->
-          let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in
-          ctx.sideg ctx.node (G.singleton access)
-        | ls ->
-          let events = Queries.LS.fold (fun (var, offs) acc ->
-              let coffs = Offset.Exp.to_cil offs in
-              let access: AccessDomain.Event.t =
-                if CilType.Varinfo.equal var dummyFunDec.svar then
-                  {var_opt = None; offs_opt = (Some coffs); kind}
-                else
-                  {var_opt = (Some var); offs_opt = (Some coffs); kind}
-              in
-              G.add access acc
-            ) ls (G.empty ())
-          in
-          ctx.sideg ctx.node events
-      end
+    | Events.Access {ad; kind; _} when !collect_local && !AnalysisState.postsolving ->
+      let events = Queries.AD.fold (fun addr es ->
+          match addr with
+          | Queries.AD.Addr.Addr (var, offs) ->
+            let coffs = ValueDomain.Offs.to_cil offs in
+            let access: AccessDomain.Event.t = {var_opt = (Some var); offs_opt = (Some coffs); kind} in
+            G.add access es
+          | UnknownPtr ->
+            let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in
+            G.add access es
+          | _ -> es
+        ) ad (G.empty ())
+      in
+      ctx.sideg ctx.node events
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index c5ad08ec76..46c620f390 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -11,6 +11,7 @@ open Analyses
 open RelationDomain
 
 module M = Messages
+module VS = SetDomain.Make (CilType.Varinfo)
 
 module SpecFunctor (Priv: RelationPriv.S) (RD: RelationDomain.RD) (PCU: RelationPrecCompareUtil.Util) =
 struct
@@ -157,15 +158,13 @@ struct
         {st' with rel = rel''}
       )
     | (Mem v, NoOffset) ->
-      (let r = ask.f (Queries.MayPointTo v) in
-       match r with
-       | `Top ->
-         st
-       | `Lifted s ->
-         let lvals = Queries.LS.elements r in
-         let ass' = List.map (fun lv -> assign_to_global_wrapper ask getg sideg st (Mval.Exp.to_cil lv) f) lvals in
-         List.fold_right D.join ass' (D.bot ())
-      )
+      begin match ask.f (Queries.MayPointTo v) with
+        | ad when Queries.AD.is_top ad -> st
+        | ad ->
+          let mvals = Queries.AD.to_mval ad in
+          let ass' = List.map (fun mval -> assign_to_global_wrapper ask getg sideg st (ValueDomain.Addr.Mval.to_cil mval) f) mvals in
+          List.fold_right D.join ass' (D.bot ())
+      end
     (* Ignoring all other assigns *)
     | _ ->
       st
@@ -217,12 +216,16 @@ struct
       | CastE (t,e) -> CastE (t, inner e)
       | Lval (Var v, off) -> Lval (Var v, off)
       | Lval (Mem e, NoOffset) ->
-        (match ask (Queries.MayPointTo e) with
-         | a when not (Queries.LS.is_top a || Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && (Queries.LS.cardinal a) = 1 ->
-           Mval.Exp.to_cil_exp (Queries.LS.choose a)
-         (* It would be possible to do better here, exploiting e.g. that the things pointed to are known to be equal *)
-         (* see: https://github.com/goblint/analyzer/pull/742#discussion_r879099745 *)
-         | _ -> Lval (Mem e, NoOffset))
+        begin match ask (Queries.MayPointTo e) with
+          | ad when not (Queries.AD.is_top ad) && (Queries.AD.cardinal ad) = 1 ->
+            begin match Queries.AD.Addr.to_mval (Queries.AD.choose ad) with
+              | Some mval -> ValueDomain.Addr.Mval.to_cil_exp mval
+              | None -> Lval (Mem e, NoOffset)
+            end
+          (* It would be possible to do better here, exploiting e.g. that the things pointed to are known to be equal *)
+          (* see: https://github.com/goblint/analyzer/pull/742#discussion_r879099745 *)
+          | _ -> Lval (Mem e, NoOffset)
+        end
       | e -> e (* TODO: Potentially recurse further? *)
     in
     inner e
@@ -268,7 +271,15 @@ struct
   let any_local_reachable fundec reachable_from_args =
     let locals = fundec.sformals @ fundec.slocals in
     let locals_id = List.map (fun v -> v.vid) locals in
-    Queries.LS.exists (fun (v',_) -> List.mem v'.vid locals_id && RD.Tracked.varinfo_tracked v') reachable_from_args
+    VS.exists (fun v -> List.mem v.vid locals_id && RD.Tracked.varinfo_tracked v) reachable_from_args
+
+  let reachable_from_args ctx args =
+    let to_vs e =
+      ctx.ask (ReachableFrom e)
+      |> Queries.AD.to_var_may
+      |> VS.of_list
+    in
+    List.fold (fun vs e -> VS.join vs (to_vs e)) (VS.empty ()) args
 
   let pass_to_callee fundec any_local_reachable var =
     (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachbale to preserve relationality *)
@@ -288,7 +299,6 @@ struct
       |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x)
       |> List.map (Tuple2.map1 RV.arg)
     in
-    let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
     let arg_vars = List.map fst arg_assigns in
     let new_rel = RD.add_vars st.rel arg_vars in
     (* RD.assign_exp_parallel_with new_rel arg_assigns; (* doesn't need to be parallel since exps aren't arg vars directly *) *)
@@ -304,6 +314,7 @@ struct
               )
           ) new_rel arg_assigns
     in
+    let reachable_from_args = reachable_from_args ctx args in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
@@ -366,16 +377,20 @@ struct
 
   let combine_env ctx r fe f args fc fun_st (f_ask : Queries.ask) =
     let st = ctx.local in
-    let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
+    let reachable_from_args = reachable_from_args ctx args in
     let fundec = Node.find_fundec ctx.node in
     if M.tracing then M.tracel "combine" "relation f: %a\n" CilType.Varinfo.pretty f.svar;
     if M.tracing then M.tracel "combine" "relation formals: %a\n" (d_list "," CilType.Varinfo.pretty) f.sformals;
     if M.tracing then M.tracel "combine" "relation args: %a\n" (d_list "," d_exp) args;
     let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in
     let arg_substitutes =
+      let filter_actuals (x,e) =
+        RD.Tracked.varinfo_tracked x
+        && List.for_all (fun v -> not (VS.mem v reachable_from_args)) (Basetype.CilExp.get_vars e)
+      in
       GobList.combine_short f.sformals args (* TODO: is it right to ignore missing formals/args? *)
       (* Do not do replacement for actuals whose value may be modified after the call *)
-      |> List.filter (fun (x, e) -> RD.Tracked.varinfo_tracked x && List.for_all (fun v -> not (Queries.LS.exists (fun (v',_) -> v'.vid = v.vid) reachable_from_args)) (Basetype.CilExp.get_vars e))
+      |> List.filter filter_actuals
       |> List.map (Tuple2.map1 RV.arg)
     in
     (* RD.substitute_exp_parallel_with new_fun_rel arg_substitutes; (* doesn't need to be parallel since exps aren't arg vars directly *) *)
@@ -438,13 +453,13 @@ struct
       match st with
       | None -> None
       | Some st ->
-        let vs = ask.f (Queries.ReachableFrom e) in
-        if Queries.LS.is_top vs then
+        let ad = ask.f (Queries.ReachableFrom e) in
+        if Queries.AD.is_top ad then
           None
         else
-          Some (Queries.LS.join vs st)
+          Some (Queries.AD.join ad st)
     in
-    List.fold_right reachable es (Some (Queries.LS.empty ()))
+    List.fold_right reachable es (Some (Queries.AD.empty ()))
 
 
   let forget_reachable ctx st es =
@@ -456,9 +471,13 @@ struct
         RD.vars st.rel
         |> List.filter_map RV.to_cil_varinfo
         |> List.map Cil.var
-      | Some rs ->
-        Queries.LS.elements rs
-        |> List.map Mval.Exp.to_cil
+      | Some ad ->
+        let to_cil addr rs =
+          match addr with
+          | Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs
+          | _ -> rs
+        in
+        Queries.AD.fold to_cil ad []
     in
     List.fold_left (fun st lval ->
         invalidate_one ask ctx st lval
@@ -515,10 +534,11 @@ struct
        | None -> st)
     | _, _ ->
       let lvallist e =
-        let s = ask.f (Queries.MayPointTo e) in
-        match s with
-        | `Top -> []
-        | `Lifted _ -> List.map Mval.Exp.to_cil (Queries.LS.elements s)
+        match ask.f (Queries.MayPointTo e) with
+        | ad when Queries.AD.is_top ad -> []
+        | ad ->
+          Queries.AD.to_mval ad
+          |> List.map ValueDomain.Addr.Mval.to_cil
       in
       let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
       let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 6ab4015460..71e2661997 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -108,7 +108,7 @@ struct
         | (info,(value:VD.t))::xs ->
           match value with
           | Address t when hasAttribute "goblint_array_domain" info.vattr ->
-            let possibleVars = List.to_seq (PreValueDomain.AD.to_var_may t) in
+            let possibleVars = List.to_seq (AD.to_var_may t) in
             Seq.fold_left (fun map arr -> VarMap.add arr (info.vattr) map) (pointedArrayMap xs) @@ Seq.filter (fun info -> isArrayType info.vtype) possibleVars
           | _ -> pointedArrayMap xs
       in
@@ -345,7 +345,7 @@ struct
           if AD.is_definite x && AD.is_definite y then
             let ax = AD.choose x in
             let ay = AD.choose y in
-            let handle_address_is_multiple addr = begin match AD.Addr.to_var addr with
+            let handle_address_is_multiple addr = begin match Addr.to_var addr with
               | Some v when a.f (Q.IsMultiple v) ->
                 if M.tracing then M.tracel "addr" "IsMultiple %a\n" CilType.Varinfo.pretty v;
                 None
@@ -353,7 +353,7 @@ struct
                 Some true
             end
             in
-            match AD.Addr.semantic_equal ax ay with
+            match Addr.semantic_equal ax ay with
             | Some true ->
               if M.tracing then M.tracel "addr" "semantic_equal %a %a\n" AD.pretty x AD.pretty y;
               handle_address_is_multiple ax
@@ -593,7 +593,7 @@ struct
         | Struct n    -> Struct (ValueDomain.Structs.map replace_val n)
         | Union (f,v) -> Union (f,replace_val v)
         | Blob (n,s,o)  -> Blob (replace_val n,s,o)
-        | Address x -> Address (ValueDomain.AD.map ValueDomain.Addr.top_indices x)
+        | Address x -> Address (AD.map ValueDomain.Addr.top_indices x)
         | x -> x
       in
       CPA.map replace_val st
@@ -613,16 +613,6 @@ struct
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval" ~removeAttr:"base.no-interval" ~keepAttr:"base.interval" fd) drop_interval
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval_set" ~removeAttr:"base.no-interval_set" ~keepAttr:"base.interval_set" fd) drop_intervalSet
 
-  (* TODO: Use AddressDomain for queries *)
-  let convertToQueryLval = function
-    | ValueDomain.AD.Addr.Addr (v,o) -> [v, Addr.Offs.to_exp o]
-    | _ -> []
-
-  let addrToLvalSet a =
-    let add x y = Q.LS.add y x in
-    try
-      AD.fold (fun e c -> List.fold_left add c (convertToQueryLval e)) a (Q.LS.empty ())
-    with SetDomain.Unsupported _ -> Q.LS.top ()
 
   let reachable_top_pointers_types ctx (ps: AD.t) : Queries.TS.t =
     let module TS = Queries.TS in
@@ -1262,9 +1252,10 @@ struct
         (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *)
         match p with
         | Address a ->
-          let s = addrToLvalSet a in
           (* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
-          if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset) s then
+          if AD.exists (function
+              | Addr (v,o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset
+              | _ -> false) a then
             Queries.Result.bot q
           else (
             let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a  None in
@@ -1277,11 +1268,7 @@ struct
       end
     | Q.MayPointTo e -> begin
         match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
-        | Address a ->
-          let s = addrToLvalSet a in
-          if AD.mem Addr.UnknownPtr a
-          then Q.LS.add (dummyFunDec.svar, `NoOffset) s
-          else s
+        | Address a -> a
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | _ -> Queries.Result.top q
       end
@@ -1298,14 +1285,10 @@ struct
         | Top -> Queries.Result.top q
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | Address a ->
-          let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe *)
-          let xs = List.map addrToLvalSet (reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local) in
-          let addrs = List.fold_left (Q.LS.join) (Q.LS.empty ()) xs in
-          if AD.mem Addr.UnknownPtr a then
-            Q.LS.add (dummyFunDec.svar, `NoOffset) addrs (* add unknown back *)
-          else
-            addrs
-        | _ -> Q.LS.empty ()
+          let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
+          let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
+          List.fold_left (AD.join) (AD.empty ()) addrs
+        | _ -> AD.empty ()
       end
     | Q.ReachableUkTypes e -> begin
         match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
@@ -1332,7 +1315,8 @@ struct
           (* ignore @@ printf "EvalStr Address: %a -> %s (must %i, may %i)\n" d_plainexp e (VD.short 80 (Address a)) (List.length @@ AD.to_var_must a) (List.length @@ AD.to_var_may a); *)
           begin match unrollType (Cilfacade.typeOf e) with
             | TPtr(TInt(IChar, _), _) ->
-              let lval = Mval.Exp.to_cil @@ Q.LS.choose @@ addrToLvalSet a in
+              let mval = List.hd (AD.to_mval a) in
+              let lval = Addr.Mval.to_cil mval in
               (try `Lifted (Bytes.to_string (Hashtbl.find char_array lval))
                with Not_found -> Queries.Result.top q)
             | _ -> (* what about ISChar and IUChar? *)
@@ -2010,14 +1994,21 @@ struct
     invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs
 
   let check_invalid_mem_dealloc ctx special_fn ptr =
+    let has_non_heap_var = AD.exists (function
+        | Addr (v,_) -> not (ctx.ask (Q.IsHeapVar v))
+        | _ -> false)
+    in
+    let has_non_zero_offset = AD.exists (function
+        | Addr (_,o) -> Offs.cmp_zero_offset o <> `MustZero
+        | _ -> false)
+    in
     match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
     | Address a ->
-      let points_to_set = addrToLvalSet a in
-      if Q.LS.is_top points_to_set then
+      if AD.is_top a then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname
-      else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
+      else if has_non_heap_var a then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
-      else if Q.LS.exists (fun (_, o) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then
+      else if has_non_zero_offset a then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr
     | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
 
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 5a2e97139c..04b148dd02 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -64,16 +64,16 @@ struct
   let (>?) = Option.bind
 
   let mayPointTo ctx exp =
-    match ctx.ask (Queries.MayPointTo exp) with
-    | a when not (Queries.LS.is_top a) && Queries.LS.cardinal a > 0 ->
-      let top_elt = (dummyFunDec.svar, `NoOffset) in
-      let a' = if Queries.LS.mem top_elt a then (
-          M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
-          Queries.LS.remove top_elt a
-        ) else a
-      in
-      Queries.LS.elements a'
-    | _ -> []
+    let ad = ctx.ask (Queries.MayPointTo exp) in
+    let a' = if Queries.AD.mem UnknownPtr ad then (
+        M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
+        Queries.AD.remove UnknownPtr ad
+      ) else ad
+    in
+    List.filter_map (function
+        | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
+        | _ -> None
+      ) (Queries.AD.elements a')
 
   let mustPointTo ctx exp = (* this is just to get Mval.Exp *)
     match mayPointTo ctx exp with
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 2041c23e1b..60e389fedf 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -244,7 +244,7 @@ let fun_ctx ctx f =
   f.vname ^ "_" ^ ctx_hash
 
 
-module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (PthreadDomain.D))
+module Tasks = SetDomain.Make (Lattice.Prod (Queries.AD) (PthreadDomain.D))
 module rec Env : sig
   type t
 
@@ -869,8 +869,6 @@ module Spec : Analyses.MCPSpec = struct
   module C = D
 
   (** Set of created tasks to spawn when going multithreaded *)
-  module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (D))
-
   module G = Tasks
 
   let tasks_var =
@@ -879,22 +877,9 @@ module Spec : Analyses.MCPSpec = struct
 
   module ExprEval = struct
     let eval_ptr ctx exp =
-      let mayPointTo ctx exp =
-        let a = ctx.ask (Queries.MayPointTo exp) in
-        if (not (Queries.LS.is_top a)) && Queries.LS.cardinal a > 0 then
-          let top_elt = (dummyFunDec.svar, `NoOffset) in
-          let a' =
-            if Queries.LS.mem top_elt a
-            then (* UNSOUND *)
-              Queries.LS.remove top_elt a
-            else a
-          in
-          Queries.LS.elements a'
-        else
-          []
-      in
-      List.map fst @@ mayPointTo ctx exp
-
+      ctx.ask (Queries.MayPointTo exp)
+      |> Queries.AD.remove UnknownPtr (* UNSOUND *)
+      |> Queries.AD.to_var_may
 
     let eval_var ctx exp =
       match exp with
@@ -1124,18 +1109,17 @@ module Spec : Analyses.MCPSpec = struct
       let arglist' = List.map (stripCasts % constFold false) arglist in
       match (LibraryFunctions.find f).special arglist', f.vname, arglist with
       | ThreadCreate { thread; start_routine = func; _ }, _, _ ->
-        let funs_ls =
-          let ls = ctx.ask (Queries.ReachableFrom func) in
-          Queries.LS.filter
-            (fun lv ->
-               let lval = Mval.Exp.to_cil lv in
-               isFunctionType (typeOfLval lval))
-            ls
+        let funs_ad =
+          let ad = ctx.ask (Queries.ReachableFrom func) in
+          Queries.AD.filter
+            (function
+              | Queries.AD.Addr.Addr mval ->
+                isFunctionType (ValueDomain.Mval.type_of mval)
+              | _ -> false)
+            ad
         in
         let thread_fun =
-          funs_ls
-          |> Queries.LS.elements
-          |> List.map fst
+          Queries.AD.to_var_may funs_ad
           |> List.unique ~eq:(fun a b -> a.vid = b.vid)
           |> List.hd
         in
@@ -1148,7 +1132,7 @@ module Spec : Analyses.MCPSpec = struct
               ; ctx = Ctx.top ()
               }
             in
-            Tasks.singleton (funs_ls, f_d)
+            Tasks.singleton (funs_ad, f_d)
           in
           ctx.sideg tasks_var tasks ;
         in
@@ -1259,9 +1243,12 @@ module Spec : Analyses.MCPSpec = struct
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)
     let tasks_f =
-      Tasks.filter
-        (fun (fs, f_d) -> Queries.LS.exists (fun (ls_f, _) -> ls_f = f) fs)
-        tasks
+      let var_in_ad ad f = Queries.AD.exists (function
+          | Queries.AD.Addr.Addr (ls_f,_) -> CilType.Varinfo.equal ls_f f
+          | _ -> false
+        ) ad
+      in
+      Tasks.filter (fun (ad,_) -> var_in_ad ad f) tasks
     in
     let f_d = snd (Tasks.choose tasks_f) in
     [ { f_d with pred = d.pred } ]
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index 174cd6a914..a9088a4bb2 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -27,19 +27,20 @@ struct
     | Queries.MayPointTo exp -> if M.tracing then M.tracel "file" "query MayPointTo: %a" d_plainexp exp; Queries.Result.top q
     | _ -> Queries.Result.top q
 
-  let query_lv (ask: Queries.ask) exp =
+  let query_ad (ask: Queries.ask) exp =
     match ask.f (Queries.MayPointTo exp) with
-    | l when not (Queries.LS.is_top l) ->
-      Queries.LS.elements l
+    | ad when not (Queries.AD.is_top ad) -> Queries.AD.elements ad
     | _ -> []
   let print_query_lv ?msg:(msg="") ask exp =
-    let xs = query_lv ask exp in (* MayPointTo -> LValSet *)
-    let pretty_key k = Pretty.text (D.string_of_key k) in
-    if M.tracing then M.tracel "file" "%s MayPointTo %a = [%a]" msg d_exp exp (Pretty.docList ~sep:(Pretty.text ", ") pretty_key) xs
+    let addrs = query_ad ask exp in (* MayPointTo -> LValSet *)
+    let pretty_key = function
+      | Queries.AD.Addr.Addr (v,o) -> Pretty.text (D.string_of_key (v, ValueDomain.Addr.Offs.to_exp o))
+      | _ -> Pretty.text "" in
+    if M.tracing then M.tracel "file" "%s MayPointTo %a = [%a]" msg d_exp exp (Pretty.docList ~sep:(Pretty.text ", ") pretty_key) addrs
 
   let eval_fv ask exp: varinfo option =
-    match query_lv ask exp with
-    | [(v,_)] -> Some v
+    match query_ad ask exp with
+    | [addr] -> Queries.AD.Addr.to_var_may addr
     | _ -> None
 
 
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index b883c7e354..137a3103a5 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -289,6 +289,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
     ("ftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []]); (* TODO: use Call instead of Spawn *)
     ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
+    ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *)
     ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
     ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]);
   ]
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index c4a0c035f2..2c2b99a075 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -19,12 +19,12 @@ struct
 
   let assign_lval (ask: Queries.ask) lval local =
     match ask.f (MayPointTo (AddrOf lval)) with
-    | ls when Queries.LS.is_top ls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) ls ->
-      D.empty ()
-    | ls when Queries.LS.exists (fun (v, _) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)) ls ->
-      D.empty ()
-    | _ ->
-      local
+    | ad when Queries.AD.is_top ad -> D.empty ()
+    | ad when Queries.AD.exists (function
+        | Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)
+        | _ -> false
+      ) ad -> D.empty ()
+    | _ -> local
 
   let assign ctx lval rval =
     assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 656e1e6f14..4d5871cb80 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -38,9 +38,11 @@ struct
       match e with
       | Lval (Var v, offs) ->
         begin match a.f (Queries.MayPointTo (mkAddrOf (Var v,offs))) with
-          | a when not (Queries.LS.is_top a)
-                         && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) a) ->
-            Queries.LS.iter (fun (v,o) -> warn_lval st (v, Offs.of_exp o)) a
+          | ad when not (Queries.AD.is_top ad) ->
+            Queries.AD.iter (function
+                | Queries.AD.Addr.Addr mval -> warn_lval st mval
+                | _ -> ()
+              ) ad
           | _ -> ()
         end
       | _ -> ()
@@ -92,31 +94,33 @@ struct
   (* Remove null values from state that are unreachable from exp.*)
   let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
     let reachable =
-      let do_exp e =
+      let do_exp e a =
         match ask.f (Queries.ReachableFrom e) with
-        | a when not (Queries.LS.is_top a)  ->
-          let to_extra (v,o) xs = AD.of_mval (v, Offs.of_exp o) :: xs  in
-          Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
+        | ad when not (Queries.AD.is_top ad) ->
+          ad
+          |> Queries.AD.filter (function
+              | Queries.AD.Addr.Addr _ -> true
+              | _ -> false)
+          |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
-        | _ -> []
+        | _ -> AD.empty ()
       in
-      List.concat_map do_exp args
+      List.fold_right do_exp args (AD.empty ())
     in
-    let add_exploded_struct (one: AD.t) (many: AD.t) : AD.t =
-      let vars = AD.to_var_may one in
-      List.fold_right AD.add (List.concat_map to_addrs vars) many
+    let vars =
+      reachable
+      |> AD.to_var_may
+      |> List.concat_map to_addrs
+      |> AD.of_list
     in
-    let vars = List.fold_right add_exploded_struct reachable (AD.empty ()) in
     if D.is_top st
     then D.top ()
     else D.filter (fun x -> AD.mem x vars) st
 
   let get_concrete_lval (ask: Queries.ask) (lval:lval) =
     match ask.f (Queries.MayPointTo (mkAddrOf lval)) with
-    | a when Queries.LS.cardinal a = 1
-                   && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) a) ->
-      let v, o = Queries.LS.choose a in
-      Some (Var v, Offs.of_exp o)
+    | ad when Queries.AD.cardinal ad = 1 && not (Queries.AD.mem UnknownPtr ad) ->
+      Queries.AD.Addr.to_mval (Queries.AD.choose ad)
     | _ -> None
 
   let get_concrete_exp (exp:exp) gl (st:D.t) =
@@ -127,11 +131,13 @@ struct
 
   let might_be_null (ask: Queries.ask) lv gl st =
     match ask.f (Queries.MayPointTo (mkAddrOf lv)) with
-    | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) a) ->
-      let one_addr_might (v,o) =
-        D.exists (fun x -> GobOption.exists (fun x -> is_prefix_of (v, Offs.of_exp o) x) (Addr.to_mval x)) st
+    | ad when not (Queries.AD.is_top ad) ->
+      let one_addr_might = function
+        | Queries.AD.Addr.Addr mval ->
+          D.exists (fun addr -> GobOption.exists (fun x -> is_prefix_of mval x) (Addr.to_mval addr)) st
+        | _ -> false
       in
-      Queries.LS.exists one_addr_might a
+      Queries.AD.exists one_addr_might ad
     | _ -> false
 
   (*
@@ -143,8 +149,8 @@ struct
     warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval lval) ;
     warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local rval;
     match get_concrete_exp rval ctx.global ctx.local, get_concrete_lval (Analyses.ask_of_ctx ctx) lval with
-    | Some rv , Some (Var vt,ot) when might_be_null (Analyses.ask_of_ctx ctx) rv ctx.global ctx.local ->
-      D.add (Addr.of_mval (vt,ot)) ctx.local
+    | Some rv, Some mval when might_be_null (Analyses.ask_of_ctx ctx) rv ctx.global ctx.local ->
+      D.add (Addr.of_mval mval) ctx.local
     | _ -> ctx.local
 
   let branch ctx (exp:exp) (tv:bool) : D.t =
@@ -185,7 +191,7 @@ struct
     match lval, D.mem (return_addr ()) au with
     | Some lv, true ->
       begin match get_concrete_lval (Analyses.ask_of_ctx ctx) lv with
-        | Some (Var v,ofs) -> D.add (Addr.of_mval (v,ofs)) ctx.local
+        | Some mval -> D.add (Addr.of_mval mval) ctx.local
         | _ -> ctx.local
       end
     | _ -> ctx.local
@@ -198,9 +204,9 @@ struct
     | Malloc _, Some lv ->
       begin
         match get_concrete_lval (Analyses.ask_of_ctx ctx) lv with
-        | Some (Var v, offs) ->
+        | Some mval ->
           ctx.split ctx.local [Events.SplitBranch ((Lval lv), true)];
-          ctx.split (D.add (Addr.of_mval (v,offs)) ctx.local) [Events.SplitBranch ((Lval lv), false)];
+          ctx.split (D.add (Addr.of_mval mval) ctx.local) [Events.SplitBranch ((Lval lv), false)];
           raise Analyses.Deadcode
         | _ -> ctx.local
       end
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 99df5695a7..1bff7611a4 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -50,15 +50,12 @@ struct
       end
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
-        | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && Queries.LS.cardinal a = 1 ->
+        | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
           (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
-          let unique_pointed_to_heap_vars =
-            Queries.LS.filter (fun (v, _) -> ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v)) a
-            |> Queries.LS.elements
-            |> List.map fst
-            |> D.of_list
-          in
-          D.diff state unique_pointed_to_heap_vars
+          begin match Queries.AD.choose ad with
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *)
+            | _ -> state
+          end
         | _ -> state
       end
     | Abort ->
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index f489b08fe9..0375bd3f74 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -29,6 +29,17 @@ struct
     else
       Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())
 
+  let relevants_from_ad ad =
+    (* TODO: what about AD with both known and unknown pointers? *)
+    if Queries.AD.is_top ad then
+      VS.top ()
+    else
+      Queries.AD.fold (fun addr vs ->
+          match addr with
+          | Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs
+          | _ -> vs
+        ) ad (VS.empty ())
+
   (* transfer functions *)
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
@@ -62,8 +73,8 @@ struct
 
   let event ctx (e: Events.t) octx =
     match e with
-    | Access {lvals; kind = Write; _} ->
-      add_to_all_defined (relevants_from_ls lvals) ctx.local
+    | Access {ad; kind = Write; _} ->
+      add_to_all_defined (relevants_from_ad ad) ctx.local
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 5a3aeb55ce..7d8298a0a4 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -155,7 +155,7 @@ struct
     let remove' ctx ~warn l =
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
-      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex which may not be held";
+      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
       match Addr.to_mval l with
       | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
         let m',rmed = Multiplicity.decrement l m in
@@ -293,10 +293,10 @@ struct
 
   let event ctx e octx =
     match e with
-    | Events.Access {exp; lvals; kind; _} when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
+    | Events.Access {exp; ad; kind; _} when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       let is_recovered_to_st = not (ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx)) in
       (* must use original (pre-assign, etc) ctx queries *)
-      let old_access var_opt offs_opt =
+      let old_access var_opt =
         (* TODO: this used to use ctx instead of octx, why? *)
         (*privatization*)
         match var_opt with
@@ -325,24 +325,21 @@ struct
             )
         | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound."
       in
-      let module LS = Queries.LS in
+      let module AD = Queries.AD in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
-      let on_lvals ls =
-        let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in
-        let f (var, offs) =
-          let coffs = Offset.Exp.to_cil offs in
-          if CilType.Varinfo.equal var dummyFunDec.svar then
-            old_access None (Some coffs)
-          else
-            old_access (Some var) (Some coffs)
+      let on_ad ad =
+        let f = function
+          | AD.Addr.Addr (g,_) when g.vglob || has_escaped g -> old_access (Some g)
+          | UnknownPtr -> old_access None
+          | _ -> ()
         in
-        LS.iter f ls
+        AD.iter f ad
       in
-      begin match lvals with
-        | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) ->
+      begin match ad with
+        | ad when not (AD.is_top ad) ->
           (* the case where the points-to set is non top and does not contain unknown values *)
-          on_lvals ls
-        | ls when not (LS.is_top ls) ->
+          on_ad ad
+        | ad ->
           (* the case where the points-to set is non top and contains unknown values *)
           (* now we need to access all fields that might be pointed to: is this correct? *)
           begin match octx.ask (ReachableUkTypes exp) with
@@ -354,11 +351,11 @@ struct
                 | _ -> false
               in
               if Queries.TS.exists f ts then
-                old_access None None
+                old_access None
           end;
-          on_lvals ls
-        | _ ->
-          old_access None None
+          on_ad ad
+          (* | _ ->
+             old_access None None *) (* TODO: what about this case? *)
       end;
       ctx.local
     | _ ->
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
index 2c57fa360b..162527b32b 100644
--- a/src/analyses/mutexEventsAnalysis.ml
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -18,24 +18,12 @@ struct
   include UnitAnalysis.Spec
   let name () = "mutexEvents"
 
-  (* TODO: Use AddressDomain for queries *)
-  let eval_exp_addr (a: Queries.ask) exp =
-    let gather_addr (v,o) b = ValueDomain.Addr.of_mval (v, Addr.Offs.of_exp o) :: b in
-    match a.f (Queries.MayPointTo exp) with
-    | a when Queries.LS.is_top a ->
-      [Addr.UnknownPtr]
-    | a ->
-      let top_elt = (dummyFunDec.svar, `NoOffset) in
-      let addrs = Queries.LS.fold gather_addr (Queries.LS.remove top_elt a) [] in
-      if Queries.LS.mem top_elt a then
-        Addr.UnknownPtr :: addrs
-      else
-        addrs
+  let eval_exp_addr (a: Queries.ask) exp = a.f (Queries.MayPointTo exp)
 
-  let lock ctx rw may_fail nonzero_return_when_aquired a lv arg =
-    match lv with
+  let lock ctx rw may_fail nonzero_return_when_aquired a lv_opt arg =
+    match lv_opt with
     | None ->
-      List.iter (fun e ->
+      Queries.AD.iter (fun e ->
           ctx.split () [Events.Lock (e, rw)]
         ) (eval_exp_addr a arg);
       if may_fail then
@@ -43,7 +31,7 @@ struct
       raise Analyses.Deadcode
     | Some lv ->
       let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in
-      List.iter (fun e ->
+      Queries.AD.iter (fun e ->
           ctx.split () [sb; Events.Lock (e, rw)];
         ) (eval_exp_addr a arg);
       if may_fail then (
@@ -67,7 +55,7 @@ struct
   let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t =
     let remove_rw x = x in
     let unlock arg remove_fn =
-      List.iter (fun e ->
+      Queries.AD.iter (fun e ->
           ctx.split () [Events.Unlock (remove_fn e)]
         ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg);
       raise Analyses.Deadcode
@@ -83,7 +71,7 @@ struct
       (* mutex is unlocked while waiting but relocked when returns *)
       (* emit unlock-lock events for privatization *)
       let ms = eval_exp_addr (Analyses.ask_of_ctx ctx) m_arg in
-      List.iter (fun m ->
+      Queries.AD.iter (fun m ->
           (* unlock-lock each possible mutex as a split to be dependent *)
           (* otherwise may-point-to {a, b} might unlock a, but relock b *)
           ctx.split () [Events.Unlock m; Events.Lock (m, true)];
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 00e49260b4..806c35f464 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -18,7 +18,7 @@ struct
   module O = Offset.Unit
 
   module V = struct
-    include Printable.Prod(CilType.Varinfo)(O)
+    include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *)
     let is_write_only _ = false
   end
 
@@ -56,7 +56,11 @@ struct
       let attr = ctx.ask (Queries.EvalMutexAttr attr) in
       let mutexes = ctx.ask (Queries.MayPointTo mutex) in
       (* It is correct to iter over these sets here, as mutexes need to be intialized before being used, and an analysis that detects usage before initialization is a different analysis. *)
-      Queries.LS.iter (function (v, o) -> ctx.sideg (v,O.of_offs o) attr) mutexes;
+      Queries.AD.iter (function addr ->
+        match addr with
+        | Queries.AD.Addr.Addr (v,o) -> ctx.sideg (v,O.of_offs o) attr
+        | _ -> ()
+        ) mutexes;
       ctx.local
     | _ -> ctx.local
 
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 5cb34baa26..1bd4b6d544 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -15,11 +15,11 @@ struct
 
   let context _ _ = ()
 
-  let check_lval tainted ((v, offset): Queries.LS.elt) =
+  let check_mval tainted ((v, offset): Queries.LS.elt) =
     if not v.vglob && VS.mem v tainted then
       M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
 
-  let rem_lval tainted ((v, offset): Queries.LS.elt) = match offset with
+  let rem_mval tainted ((v, offset): Queries.LS.elt) = match offset with
     | `NoOffset -> VS.remove v tainted
     | _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
 
@@ -38,18 +38,21 @@ struct
         ) ctx.local
     )
 
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+  let enter ctx (_:lval option) (_:fundec) (args:exp list) : (D.t * D.t) list =
     if VS.is_empty ctx.local then
       [ctx.local,ctx.local]
     else (
-      let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
-      if Queries.LS.is_top reachable_from_args || VS.is_top ctx.local then
+      let reachable_from_args = List.fold (fun ad e -> Queries.AD.join ad (ctx.ask (ReachableFrom e))) (Queries.AD.empty ()) args in
+      if Queries.AD.is_top reachable_from_args || VS.is_top ctx.local then
         [ctx.local, ctx.local]
       else
         let reachable_vars =
-          Queries.LS.elements reachable_from_args
-          |> List.map fst
-          |> VS.of_list
+          let get_vars addr vs =
+            match addr with
+            | Queries.AD.Addr.Addr (v,_) -> VS.add v vs
+            | _ -> vs
+          in
+          Queries.AD.fold get_vars reachable_from_args (VS.empty ())
         in
         [VS.diff ctx.local reachable_vars, VS.inter reachable_vars ctx.local]
     )
@@ -79,26 +82,31 @@ struct
             ()
         ) longjmp_nodes;
       D.join modified_locals ctx.local
-    | Access {lvals; kind = Read; _} ->
-      if Queries.LS.is_top lvals then (
-        if not (VS.is_empty octx.local) then
+    | Access {ad; kind = Read; _} ->
+      (* TODO: what about AD with both known and unknown pointers? *)
+      begin match ad with
+        | ad when Queries.AD.is_top ad && not (VS.is_empty octx.local) ->
           M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
-      )
-      else (
-        Queries.LS.iter (fun lv ->
-            (* Use original access state instead of current with removed written vars. *)
-            check_lval octx.local lv
-          ) lvals
-      );
+        | ad ->
+          Queries.AD.iter (function
+              (* Use original access state instead of current with removed written vars. *)
+              | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (v, ValueDomain.Offs.to_exp o)
+              | _ -> ()
+            ) ad
+      end;
       ctx.local
-    | Access {lvals; kind = Write; _} ->
-      if Queries.LS.is_top lvals then
-        ctx.local
-      else (
-        Queries.LS.fold (fun lv acc ->
-            rem_lval acc lv
-          ) lvals ctx.local
-      )
+    | Access {ad; kind = Write; _} ->
+      (* TODO: what about AD with both known and unknown pointers? *)
+      begin match ad with
+        | ad when Queries.AD.is_top ad ->
+          ctx.local
+        | ad ->
+          Queries.AD.fold (fun addr vs ->
+              match addr with
+              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
+              | _ -> vs
+            ) ad ctx.local
+      end
     | _ -> ctx.local
 
 end
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 036d1bd2c6..0b776282e8 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -17,16 +17,8 @@ struct
   module C = MustSignals
   module G = SetDomain.ToppedSet (MHP) (struct let topname = "All Threads" end)
 
-  (* TODO: Use AddressDomain for queries *)
-  let eval_exp_addr (a: Queries.ask) exp =
-    let gather_addr (v,o) b = ValueDomain.Addr.of_mval (v, ValueDomain.Addr.Offs.of_exp o) :: b in
-    match a.f (Queries.MayPointTo exp) with
-    | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) a) ->
-      Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
-    | _ -> []
-
-  let possible_vinfos a cv_arg =
-    List.filter_map ValueDomain.Addr.to_var_may (eval_exp_addr a cv_arg)
+  let possible_vinfos (a: Queries.ask) cv_arg =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo cv_arg))
 
   (* transfer functions *)
 
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index d1d608ae06..9c2272fabb 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -302,12 +302,12 @@ struct
         ) (G.vars (ctx.global (V.vars g)))
     | _ -> Queries.Result.top q
 
-  let event ctx exp octx =
-    match exp with
-    | Events.Access {exp; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
+  let event ctx e octx =
+    match e with
+    | Events.Access {exp; ad; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       (* must use original (pre-assign, etc) ctx queries *)
       let conf = 110 in
-      let module LS = Queries.LS in
+      let module AD = Queries.AD in
       let part_access (vo:varinfo option): MCPAccess.A.t =
         (*partitions & locks*)
         Obj.obj (octx.ask (PartAccess (Memory {exp; var_opt=vo; kind})))
@@ -324,24 +324,24 @@ struct
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls
          -- this is the common case if we have a sound points-to set. *)
-      let on_lvals ls includes_uk =
-        let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in
+      let on_ad ad includes_uk =
         let conf = if reach then conf - 20 else conf in
         let conf = if includes_uk then conf - 10 else conf in
-        let f (var, offs) =
-          let coffs = Offset.Exp.to_cil offs in
-          if CilType.Varinfo.equal var dummyFunDec.svar then
-            add_access conf None
-          else
-            add_access conf (Some (var, coffs))
+        let f addr =
+          match addr with
+          | AD.Addr.Addr (g,o) when g.vglob || has_escaped g ->
+            let coffs = ValueDomain.Offs.to_cil o in
+            add_access conf (Some (g, coffs))
+          | UnknownPtr -> add_access conf None
+          | _ -> ()
         in
-        LS.iter f ls
+        AD.iter f ad
       in
-      begin match lvals with
-        | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) ->
+      begin match ad with
+        | ad when not (AD.is_top ad) ->
           (* the case where the points-to set is non top and does not contain unknown values *)
-          on_lvals ls false
-        | ls when not (LS.is_top ls) ->
+          on_ad ad false
+        | ad ->
           (* the case where the points-to set is non top and contains unknown values *)
           let includes_uk = ref false in
           (* now we need to access all fields that might be pointed to: is this correct? *)
@@ -358,9 +358,9 @@ struct
               in
               Queries.TS.iter f ts
           end;
-          on_lvals ls !includes_uk
-        | _ ->
-          add_access (conf - 60) None
+          on_ad ad !includes_uk
+          (* | _ ->
+             add_access (conf - 60) None *) (* TODO: what about this case? *)
       end;
       ctx.local
     | _ ->
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index d7328310dd..54ffcd2697 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -203,15 +203,14 @@ struct
     match q with
     | _ -> Queries.Result.top q
 
-  let query_lv ask exp =
+  let query_addrs ask exp =
     match ask (Queries.MayPointTo exp) with
-    | l when not (Queries.LS.is_top l) ->
-      Queries.LS.elements l
+    | ad when not (Queries.AD.is_top ad) -> Queries.AD.elements ad
     | _ -> []
 
   let eval_fv ask exp: varinfo option =
-    match query_lv ask exp with
-    | [(v,_)] -> Some v
+    match query_addrs ask exp with
+    | [addr] -> Queries.AD.Addr.to_var_may addr
     | _ -> None
 
 
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 76f4af8f9e..d053cd103b 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -6,12 +6,22 @@
 open GoblintCil
 open Analyses
 
+module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)
+
+let to_mvals ad =
+  (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
+  Queries.AD.fold (fun addr mvals ->
+      match addr with
+      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals (* TODO: use unconverted addrs in domain? *)
+      | _ -> mvals
+    ) ad (D.empty ())
+
 module Spec =
 struct
   include Analyses.IdentitySpec
 
   let name () = "taintPartialContexts"
-  module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)
+  module D = D
   module C = Lattice.Unit
 
   (* Add Lval or any Lval which it may point to to the set *)
@@ -19,7 +29,7 @@ struct
     let d = ctx.local in
     (match lval with
      | (Var v, offs) -> D.add (v, Offset.Exp.of_cil offs) d
-     | (Mem e, _) -> D.union (ctx.ask (Queries.MayPointTo e)) d
+     | (Mem e, _) -> D.union (to_mvals (ctx.ask (Queries.MayPointTo e))) d
     )
 
   (* this analysis is context insensitive*)
@@ -84,9 +94,9 @@ struct
       else
         deep_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.MayPointTo addr))) d shallow_addrs
+    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.MayPointTo addr)))) d shallow_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.ReachableFrom addr))) d deep_addrs
+    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.ReachableFrom addr)))) d deep_addrs
     in
     d
 
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 8a14f4102e..9ed62e7422 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -4,6 +4,7 @@ open GoblintCil
 open Analyses
 
 module M = Messages
+module AD = Queries.AD
 
 let has_escaped (ask: Queries.ask) (v: varinfo): bool =
   assert (not v.vglob);
@@ -26,22 +27,30 @@ struct
 
   let reachable (ask: Queries.ask) e: D.t =
     match ask.f (Queries.ReachableFrom e) with
-    | a when not (Queries.LS.is_top a) ->
-      let to_extra (v,o) set = D.add v set in
-      Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) (D.empty ())
+    | ad when not (Queries.AD.is_top ad) ->
+      let to_extra addr set =
+        match addr with
+        | Queries.AD.Addr.Addr (v,_) -> D.add v set
+        | _ -> set
+      in
+      Queries.AD.fold to_extra ad (D.empty ())
     (* Ignore soundness warnings, as invalidation proper will raise them. *)
-    | a ->
-      if M.tracing then M.tracel "escape" "reachable %a: %a\n" d_exp e Queries.LS.pretty a;
+    | ad ->
+      if M.tracing then M.tracel "escape" "reachable %a: %a\n" d_exp e Queries.AD.pretty ad;
       D.empty ()
 
   let mpt (ask: Queries.ask) e: D.t =
     match ask.f (Queries.MayPointTo e) with
-    | a when not (Queries.LS.is_top a) ->
-      let to_extra (v,o) set = D.add v set in
-      Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) (D.empty ())
+    | ad when not (AD.is_top ad) ->
+      let to_extra addr set =
+        match addr with
+        | AD.Addr.Addr (v,_) -> D.add v set
+        | _ -> set
+      in
+      AD.fold to_extra (AD.remove UnknownPtr ad) (D.empty ())
     (* Ignore soundness warnings, as invalidation proper will raise them. *)
-    | a ->
-      if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e Queries.LS.pretty a;
+    | ad ->
+      if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e AD.pretty ad;
       D.empty ()
 
   let thread_id ctx =
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 850bd677bd..f8759d9134 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -29,12 +29,15 @@ struct
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
-  (* TODO: Use AddressDomain for queries *)
   let access_address (ask: Queries.ask) write lv =
     match ask.f (Queries.MayPointTo (AddrOf lv)) with
-    | a when not (Queries.LS.is_top a) ->
-      let to_extra (v,o) xs = (v, Addr.Offs.of_exp o, write) :: xs  in
-      Queries.LS.fold to_extra a []
+    | ad when not (Queries.AD.is_top ad) ->
+      let to_extra addr xs =
+        match addr with
+        | Queries.AD.Addr.Addr (v,o) -> (v, o, write) :: xs
+        | _ -> xs
+      in
+      Queries.AD.fold to_extra ad []
     | _ ->
       M.info ~category:Unsound "Access to unknown address could be global"; []
 
@@ -165,9 +168,10 @@ struct
       List.fold_right remove_if_prefix (get_pfx v `NoOffset ofs v.vtype v.vtype) st
     in
     match a.f (Queries.MayPointTo (AddrOf lv)) with
-    | a when Queries.LS.cardinal a = 1 ->  begin
-        let var, ofs = Queries.LS.choose a in
-        init_vo var (Addr.Offs.of_exp ofs)
+    | ad when Queries.AD.cardinal ad = 1 ->
+      begin match Queries.AD.Addr.to_mval (Queries.AD.choose ad) with
+        | Some (var, ofs) -> init_vo var ofs
+        | None -> st
       end
     | _ -> st
 
@@ -189,21 +193,25 @@ struct
 
   let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
     let reachable =
-      let do_exp e =
+      let do_exp e a =
         match ask.f (Queries.ReachableFrom e) with
-        | a when not (Queries.LS.is_top a) ->
-          let to_extra (v,o) xs = AD.of_mval (v, Addr.Offs.of_exp o) :: xs  in
-          Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
+        | ad when not (Queries.AD.is_top ad) ->
+          ad
+          |> Queries.AD.filter (function
+              | Queries.AD.Addr.Addr _ -> true
+              | _ -> false)
+          |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
-        | _ -> []
+        | _ -> AD.empty ()
       in
-      List.concat_map do_exp args
+      List.fold_right do_exp args (AD.empty ())
     in
-    let add_exploded_struct (one: AD.t) (many: AD.t) : AD.t =
-      let vars = AD.to_var_may one in
-      List.fold_right AD.add (List.concat_map to_addrs vars) many
+    let vars =
+      reachable
+      |> AD.to_var_may
+      |> List.concat_map to_addrs
+      |> AD.of_list
     in
-    let vars = List.fold_right add_exploded_struct reachable (AD.empty ()) in
     if D.is_top st
     then D.top ()
     else D.filter (fun x -> AD.mem x vars) st
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index c3aebc985e..0aafbd1ad4 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -83,15 +83,17 @@ struct
       | Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *)
     in
     match ctx.ask (Queries.MayPointTo lval_to_query) with
-    | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
-      let warn_for_heap_var var =
-        if D.mem var state then
-          M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" var.vname transfer_fn_name
+    | ad when not (Queries.AD.is_top ad) ->
+      let warn_for_heap_var v =
+        if D.mem v state then
+          M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name
       in
       let pointed_to_heap_vars =
-        Queries.LS.elements a
-        |> List.map fst
-        |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
+        Queries.AD.fold (fun addr vars ->
+            match addr with
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars
+            | _ -> vars
+          ) ad []
       in
       List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *)
       (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
@@ -154,12 +156,12 @@ struct
     if D.is_empty caller_state then
       [caller_state, caller_state]
     else (
-      let reachable_from_args = List.fold_left (fun acc arg -> Queries.LS.join acc (ctx.ask (ReachableFrom arg))) (Queries.LS.empty ()) args in
-      if Queries.LS.is_top reachable_from_args || D.is_top caller_state then
+      let reachable_from_args = List.fold_left (fun ad arg -> Queries.AD.join ad (ctx.ask (ReachableFrom arg))) (Queries.AD.empty ()) args in
+      if Queries.AD.is_top reachable_from_args || D.is_top caller_state then
         [caller_state, caller_state]
       else
-        let reachable_vars = List.map fst (Queries.LS.elements reachable_from_args) in
-        let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in
+        let reachable_vars = Queries.AD.to_var_may reachable_from_args in
+        let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in (* TODO: use AD.mem directly *)
         [caller_state, callee_state]
     )
 
@@ -179,12 +181,13 @@ struct
     match desc.special arglist with
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
-        | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
+        | ad when not (Queries.AD.is_top ad) ->
           let pointed_to_heap_vars =
-            Queries.LS.elements a
-            |> List.map fst
-            |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
-            |> D.of_list
+            Queries.AD.fold (fun addr state ->
+                match addr with
+                | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsHeapVar var) -> D.add var state
+                | _ -> state
+              ) ad (D.empty ())
           in
           (* Side-effect the tid that's freeing all the heap vars collected here *)
           side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx);
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 3054f2e0da..634a684c7c 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -176,7 +176,7 @@ struct
   let may_change (ask: Queries.ask) (b:exp) (a:exp) : bool =
     (*b should be an address of something that changes*)
     let pt e = ask.f (Queries.MayPointTo e) in
-    let bls = pt b in
+    let bad = pt b in
     let bt =
       match unrollTypeDeep (Cilfacade.typeOf b) with
       | TPtr (t,_) -> t
@@ -208,26 +208,26 @@ struct
         | at -> at
       in
       bt = voidType || (isIntegralType at && isIntegralType bt) || (deref && typ_equal (TPtr (at,[]) ) bt) || typ_equal at bt ||
-              match a with
-              | Const _
-              | SizeOf _
-              | SizeOfE _
-              | SizeOfStr _
-              | AlignOf _
-              | AlignOfE _
-              | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
-              | UnOp (_,e,_)
-              | Real e
-              | Imag e -> type_may_change_t deref e
-              | BinOp (_,e1,e2,_) -> type_may_change_t deref e1 || type_may_change_t deref e2
-              | Lval (Var _,o)
-              | AddrOf (Var _,o)
-              | StartOf (Var _,o) -> may_change_t_offset o
-              | Lval (Mem e,o)    -> may_change_t_offset o || type_may_change_t true e
-              | AddrOf (Mem e,o)  -> may_change_t_offset o || type_may_change_t false e
-              | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t false e
-              | CastE (t,e) -> type_may_change_t deref e
-              | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
+      match a with
+      | Const _
+      | SizeOf _
+      | SizeOfE _
+      | SizeOfStr _
+      | AlignOf _
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+      | UnOp (_,e,_)
+      | Real e
+      | Imag e -> type_may_change_t deref e
+      | BinOp (_,e1,e2,_) -> type_may_change_t deref e1 || type_may_change_t deref e2
+      | Lval (Var _,o)
+      | AddrOf (Var _,o)
+      | StartOf (Var _,o) -> may_change_t_offset o
+      | Lval (Mem e,o)    -> may_change_t_offset o || type_may_change_t true e
+      | AddrOf (Mem e,o)  -> may_change_t_offset o || type_may_change_t false e
+      | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t false e
+      | CastE (t,e) -> type_may_change_t deref e
+      | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
 
     and lval_may_change_pt a bl : bool =
       let rec may_change_pt_offset o =
@@ -247,7 +247,7 @@ struct
         | CastE   (t,e) -> addrOfExp e
         | _ -> None
       in
-      let lval_is_not_disjoint (v,o) als =
+      let lval_is_not_disjoint (v,o) aad =
         let rec oleq o s =
           match o, s with
           | `NoOffset, _ -> true
@@ -255,18 +255,21 @@ struct
           | `Index (i1,o), `Index (i2,s) when exp_equal i1 i2     -> oleq o s
           | _ -> false
         in
-        if Queries.LS.is_top als
+        if Queries.AD.is_top aad
         then false
-        else Queries.LS.exists (fun (u,s) -> CilType.Varinfo.equal v u && oleq o s) als
+        else Queries.AD.exists (function
+            | Addr (u,s) -> CilType.Varinfo.equal v u && oleq o (Addr.Offs.to_exp s) (* TODO: avoid conversion? *)
+            | _ -> false
+          ) aad
       in
-      let (als, test) =
+      let (aad, test) =
         match addrOfExp a with
-        | None -> (Queries.LS.bot (), false)
+        | None -> (Queries.AD.bot (), false)
         | Some e ->
-          let als = pt e in
-          (als, lval_is_not_disjoint bl als)
+          let aad = pt e in
+          (aad, lval_is_not_disjoint bl aad)
       in
-      if (Queries.LS.is_top als) || Queries.LS.mem (dummyFunDec.svar, `NoOffset) als
+      if Queries.AD.is_top aad
       then type_may_change_apt a
       else test ||
            match a with
@@ -292,9 +295,12 @@ struct
     in
     let r =
       if Cil.isConstant b || Cil.isConstant a then false
-      else if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
+      else if Queries.AD.is_top bad
       then ((*Messages.warn ~category:Analyzer "No PT-set: switching to types ";*) type_may_change_apt a )
-      else Queries.LS.exists (lval_may_change_pt a) bls
+      else Queries.AD.exists (function
+          | Addr (v,o) -> lval_may_change_pt a (v, Addr.Offs.to_exp o) (* TODO: avoid conversion? *)
+          | _ -> false
+        ) bad
     in
     (*    if r
           then (Messages.warn ~category:Analyzer ~msg:("Kill " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r)
@@ -339,8 +345,11 @@ struct
       Some (v.vglob || (ask.f (Queries.IsMultiple v) || BaseUtil.is_global ask v))
     | Lval (Mem e, _) ->
       begin match ask.f (Queries.MayPointTo e) with
-        | ls when not (Queries.LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) ls) ->
-          Some (Queries.LS.exists (fun (v, _) -> is_global_var ask (Lval (var v)) = Some true) ls)
+        | ad when not (Queries.AD.is_top ad) ->
+          Some (Queries.AD.exists (function
+              | Addr (v,_) -> is_global_var ask (Lval (var v)) = Some true
+              | _ -> false
+            ) ad)
         | _ -> Some true
       end
     | CastE (t,e) -> is_global_var ask e
@@ -380,17 +389,11 @@ struct
   (* Give the set of reachables from argument. *)
   let reachables ~deep (ask: Queries.ask) es =
     let reachable e st =
-      match st with
-      | None -> None
-      | Some st ->
-        let q = if deep then Queries.ReachableFrom e else Queries.MayPointTo e in
-        let vs = ask.f q in
-        if Queries.LS.is_top vs then
-          None
-        else
-          Some (Queries.LS.join vs st)
+      let q = if deep then Queries.ReachableFrom e else Queries.MayPointTo e in
+      let ad = ask.f q in
+      Queries.AD.join ad st
     in
-    List.fold_right reachable es (Some (Queries.LS.empty ()))
+    List.fold_right reachable es (Queries.AD.empty ())
 
 
   (* Probably ok as is. *)
@@ -451,15 +454,17 @@ struct
     | None -> ctx.local
 
   let remove_reachable ~deep ask es st =
-    match reachables ~deep ask es with
-    | None -> D.top ()
-    | Some rs ->
-      (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction":
-         each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from.
-         It is unknown, why that was necessary. *)
-      Queries.LS.fold (fun lval st ->
-          remove ask (Mval.Exp.to_cil lval) st
-        ) rs st
+    let rs = reachables ~deep ask es in
+    if M.tracing then M.tracel "var_eq" "remove_reachable %a: %a\n" (Pretty.d_list ", " d_exp) es AD.pretty rs;
+    (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction":
+       each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from.
+       It is unknown, why that was necessary. *)
+    Queries.AD.fold (fun addr st ->
+        match addr with
+        | Queries.AD.Addr.Addr mval -> remove ask (ValueDomain.Mval.to_cil mval) st
+        | UnknownPtr -> D.top ()
+        | _ -> st
+      ) rs st
 
   let unknown_fn ctx lval f args =
     let desc = LF.find f in
@@ -489,8 +494,8 @@ struct
       end
     | ThreadCreate { arg; _ } ->
       begin match D.is_bot ctx.local with
-      | true -> raise Analyses.Deadcode
-      | false -> remove_reachable ~deep:true (Analyses.ask_of_ctx ctx) [arg] ctx.local
+        | true -> raise Analyses.Deadcode
+        | false -> remove_reachable ~deep:true (Analyses.ask_of_ctx ctx) [arg] ctx.local
       end
     | _ -> unknown_fn ctx lval f args
   (* query stuff *)
diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml
index 9f6ee56cbf..5981caf9ea 100644
--- a/src/cdomains/addressDomain.ml
+++ b/src/cdomains/addressDomain.ml
@@ -440,4 +440,6 @@ struct
     let r = narrow x y in
     if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
     r
+
+  let filter f ad = fold (fun addr ad -> if f addr then add addr ad else ad) ad (empty ())
 end
diff --git a/src/cdomains/mvalMapDomain.ml b/src/cdomains/mvalMapDomain.ml
index 9d7625c4f5..d0d2f8da85 100644
--- a/src/cdomains/mvalMapDomain.ml
+++ b/src/cdomains/mvalMapDomain.ml
@@ -281,13 +281,19 @@ struct
 
   let keys_from_lval lval (ask: Queries.ask) = (* use MayPointTo query to get all possible pointees of &lval *)
     (* print_query_lv ctx.ask (AddrOf lval); *)
-    let query_lv (ask: Queries.ask) exp = match ask.f (Queries.MayPointTo exp) with
-      | l when not (Queries.LS.is_top l) -> Queries.LS.elements l
+    let query_addrs (ask: Queries.ask) exp = match ask.f (Queries.MayPointTo exp) with
+      | ad when not (Queries.AD.is_top ad) -> Queries.AD.elements ad
       | _ -> []
     in
     let exp = AddrOf lval in
-    let xs = query_lv ask exp in (* MayPointTo -> LValSet *)
+    let addrs = query_addrs ask exp in (* MayPointTo -> LValSet *)
+    let keys = List.fold (fun vs addr -> 
+        match addr with
+        | Queries.AD.Addr.Addr (v,o) -> (v, ValueDomain.Offs.to_exp o) :: vs
+        | _ -> vs
+      ) [] addrs
+    in
     let pretty_key k = Pretty.text (string_of_key k) in
-    Messages.debug ~category:Analyzer "MayPointTo %a = [%a]" d_exp exp (Pretty.docList ~sep:(Pretty.text ", ") pretty_key) xs;
-    xs
+    Messages.debug ~category:Analyzer "MayPointTo %a = [%a]" d_exp exp (Pretty.docList ~sep:(Pretty.text ", ") pretty_key) keys;
+    keys
 end
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index a239be7c83..9d894b6b34 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -10,7 +10,7 @@ module M = Messages
 module BI = IntOps.BigIntOps
 module MutexAttr = MutexAttrDomain
 module VDQ = ValueDomainQueries
-module LS = VDQ.LS
+module AD = VDQ.AD
 module AddrSetDomain = SetDomain.ToppedSet(Addr)(struct let topname = "All" end)
 module ArrIdxDomain = IndexDomain
 
@@ -756,9 +756,9 @@ struct
       match exp, start_of_array_lval with
       | BinOp(IndexPI, Lval lval, add, _), (Var arr_start_var, NoOffset) when not (contains_pointer add) ->
         begin match ask.may_point_to (Lval lval) with
-          | v when LS.cardinal v = 1 && not (LS.is_top v) ->
-            begin match LS.choose v with
-              | (var,`Index (i,`NoOffset)) when Cil.isZero (Cil.constFold true i) && CilType.Varinfo.equal var arr_start_var ->
+          | v when AD.cardinal v = 1 && not (AD.is_top v) ->
+            begin match AD.choose v with
+              | AD.Addr.Addr (var,`Index (i,`NoOffset)) when ID.equal_to Z.zero i = `Eq && CilType.Varinfo.equal var arr_start_var ->
                 (* The idea here is that if a must(!) point to arr and we do sth like a[i] we don't want arr to be partitioned according to (arr+i)-&a but according to i instead  *)
                 add
               | _ -> BinOp(MinusPP, exp, StartOf start_of_array_lval, !ptrdiffType)
diff --git a/src/domains/events.ml b/src/domains/events.ml
index 2141ad17dd..06561bddbe 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -10,7 +10,7 @@ type t =
   | EnterMultiThreaded
   | SplitBranch of exp * bool (** Used to simulate old branch-based split. *)
   | AssignSpawnedThread of lval * ThreadIdDomain.Thread.t (** Assign spawned thread's ID to lval. *)
-  | Access of {exp: CilType.Exp.t; lvals: Queries.LS.t; kind: AccessKind.t; reach: bool}
+  | Access of {exp: CilType.Exp.t; ad: Queries.AD.t; kind: AccessKind.t; reach: bool}
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
@@ -41,7 +41,7 @@ let pretty () = function
   | EnterMultiThreaded -> text "EnterMultiThreaded"
   | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv
   | AssignSpawnedThread (lval, tid) -> dprintf "AssignSpawnedThread (%a, %a)" d_lval lval ThreadIdDomain.Thread.pretty tid
-  | Access {exp; lvals; kind; reach} -> dprintf "Access {exp=%a; lvals=%a; kind=%a; reach=%B}" CilType.Exp.pretty exp Queries.LS.pretty lvals AccessKind.pretty kind reach
+  | Access {exp; ad; kind; reach} -> dprintf "Access {exp=%a; ad=%a; kind=%a; reach=%B}" CilType.Exp.pretty exp Queries.AD.pretty ad AccessKind.pretty kind reach
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 214fcf1384..0388ce2995 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -34,6 +34,7 @@ module FlatYojson = Lattice.Flat (Printable.Yojson) (struct
 
 module SD = Basetype.Strings
 module VD = ValueDomain.Compound
+module AD = ValueDomain.AD
 
 module MayBool = BoolDomain.MayBool
 module MustBool = BoolDomain.MustBool
@@ -71,8 +72,8 @@ type invariant_context = Invariant.context = {
 (** GADT for queries with specific result type. *)
 type _ t =
   | EqualSet: exp -> ES.t t
-  | MayPointTo: exp -> LS.t t
-  | ReachableFrom: exp -> LS.t t
+  | MayPointTo: exp -> AD.t t
+  | ReachableFrom: exp -> AD.t t
   | ReachableUkTypes: exp -> TS.t t
   | Regions: exp -> LS.t t
   | MayEscape: varinfo -> MayBool.t t
@@ -140,8 +141,8 @@ struct
     (* Cannot group these GADTs... *)
     | EqualSet _ -> (module ES)
     | CondVars _ -> (module ES)
-    | MayPointTo _ -> (module LS)
-    | ReachableFrom _ -> (module LS)
+    | MayPointTo _ -> (module AD)
+    | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
     | MustLockset -> (module LS)
     | EvalFunvar _ -> (module LS)
@@ -204,8 +205,8 @@ struct
     (* Cannot group these GADTs... *)
     | EqualSet _ -> ES.top ()
     | CondVars _ -> ES.top ()
-    | MayPointTo _ -> LS.top ()
-    | ReachableFrom _ -> LS.top ()
+    | MayPointTo _ -> AD.top ()
+    | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
     | MustLockset -> LS.top ()
     | EvalFunvar _ -> LS.top ()
diff --git a/src/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml
index d366e6dda3..8266582ac2 100644
--- a/src/domains/valueDomainQueries.ml
+++ b/src/domains/valueDomainQueries.ml
@@ -4,6 +4,7 @@ open GoblintCil
 open BoolDomain
 
 module LS = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)
+module AD = PreValueDomain.AD
 
 module ID =
 struct
@@ -44,7 +45,7 @@ struct
 end
 
 type eval_int = exp -> ID.t
-type may_point_to = exp -> LS.t
+type may_point_to = exp -> AD.t
 type is_multiple = varinfo -> bool
 
 (** Subset of queries used by the valuedomain, using a simpler representation. *)
diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t
index 7a4439141d..9b02dcde76 100644
--- a/tests/regression/06-symbeq/21-mult_accs_rc.t
+++ b/tests/regression/06-symbeq/21-mult_accs_rc.t
@@ -10,6 +10,7 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Race] Memory location (struct s).data (race with conf. 100):
     write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
     write with [symblock:{p-lock:*.mutex}, mhp:{tid=[main]; created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}}, thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
+  [Warning][Unknown] unlocking mutex (NULL) which may not be held (21-mult_accs_rc.c:35:3-35:26)
   [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14)
@@ -24,6 +25,7 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9)
   [Success][Race] Memory location (struct s).data (safe):
     write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+  [Warning][Unknown] unlocking mutex (NULL) which may not be held (21-mult_accs_rc.c:35:3-35:26)
   [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14)