diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index f3ebcfb78..e13e0a591 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -65,7 +65,7 @@ let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function
 
 let rec apron_texpr_of_llair_exp exp q =
   match (exp : Llair.Exp.t) with
-  | Reg {name} | Function {name} ->
+  | Reg {name} | Global {name} | Function {name} ->
       Some (Texpr1.Var (apron_var_of_name name))
   | Integer {data} -> Some (Texpr1.Cst (Coeff.s_of_int (Z.to_int data)))
   | Float {data} -> (
@@ -278,7 +278,7 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     todo "Summaries not yet implemented for interval analysis" ()
   else
     let mangle r =
-      Llair.Reg.program (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
+      Llair.Reg.mk (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
     in
     let args = List.combine_exn formals actuals in
     let q' = List.fold ~f:(fun (f, a) q -> assign (mangle f) a q) args q in
@@ -311,4 +311,4 @@ type summary = t
 
 let pp_summary = pp
 let apply_summary _ _ = None
-let create_summary ~locals:_ ~formals:_ q = (q, q)
+let create_summary ~globals:_ ~locals:_ ~formals:_ q = (q, q)
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index 1c500160a..c8a7c1521 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -343,10 +343,10 @@ let xlate_float : x -> Llvm.llvalue -> Exp.t =
   let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
   Exp.float typ data
 
-let xlate_name x ?global : Llvm.llvalue -> Reg.t =
+let xlate_name x : Llvm.llvalue -> Reg.t =
  fun llv ->
   let typ = xlate_type x (Llvm.type_of llv) in
-  Reg.program ?global typ (find_name llv)
+  Reg.mk typ (find_name llv)
 
 let xlate_name_opt : x -> Llvm.llvalue -> Reg.t option =
  fun x instr ->
@@ -457,7 +457,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
         , Exp.function_
             (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv))
         )
-    | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
+    | GlobalVariable -> ([], Exp.global (xlate_global x llv).name)
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
     | ConstantInt -> ([], xlate_int x llv)
     | ConstantFP -> ([], xlate_float x llv)
@@ -501,7 +501,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
           todo "types with undetermined size: %a" pp_lltype llt () ;
         let name = Printf.sprintf "undef_%i" !undef_count in
         let loc = Loc.none in
-        let reg = Reg.program typ name in
+        let reg = Reg.mk typ name in
         let msg = Llvm.string_of_llvalue llv in
         ([Inst.nondet ~reg:(Some reg) ~msg ~loc], Exp.reg reg)
     | Instruction
@@ -751,7 +751,7 @@ and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
   GlobTbl.find_or_add memo_global llg ~default:(fun () ->
       [%Trace.call fun {pf} -> pf "%a" pp_llvalue llg]
       ;
-      let g = xlate_name x ~global:() llg in
+      let g = Global.mk (xlate_type x (Llvm.type_of llg)) (find_name llg) in
       let loc = find_loc llg in
       (* add to tbl without initializer in case of recursive occurrences in
          its own initializer *)
@@ -772,7 +772,7 @@ and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
       in
       GlobalDefn.mk ?init g loc
       |>
-      [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp_defn] )
+      [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp] )
 
 type pop_thunk = Loc.t -> Llair.inst list
 
@@ -925,7 +925,7 @@ let rec xlate_func_name x llv =
       ( []
       , Exp.function_
           (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv)) )
-  | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
+  | GlobalVariable -> ([], Exp.global (xlate_global x llv).name)
   | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
   | Argument | Instruction _ -> xlate_value x llv
   | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@@ -1147,7 +1147,7 @@ let xlate_instr :
             && not (Llvm.is_declaration llfunc)
           then
             warn "ignoring variable arguments to variadic function: %a"
-              GlobalDefn.pp (xlate_global x llfunc) () ;
+              Global.pp (xlate_global x llfunc).name () ;
           assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;
           Array.length (Llvm.param_types (Llvm.element_type lltyp)) )
       in
@@ -1264,8 +1264,8 @@ let xlate_instr :
          e.g. either cleanup or rethrow. *)
       let i32, tip, cxa_exception = landingpad_typs x instr in
       let pi8, _, exc_typ = exception_typs in
-      let exc = Exp.reg (Reg.program pi8 (find_name instr ^ ".exc")) in
-      let ti = Reg.program tip (name ^ ".ti") in
+      let exc = Exp.reg (Reg.mk pi8 (find_name instr ^ ".exc")) in
+      let ti = Reg.mk tip (name ^ ".ti") in
       (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
       let load_ti =
         let typ = cxa_exception in
@@ -1451,11 +1451,11 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
   let freturn =
     match typ with
     | Pointer {elt= Function {return= Some typ; _}} ->
-        Some (Reg.program typ "freturn")
+        Some (Reg.mk typ "freturn")
     | _ -> None
   in
   let _, _, exc_typ = exception_typs in
-  let fthrow = Reg.program exc_typ "fthrow" in
+  let fthrow = Reg.mk exc_typ "fthrow" in
   ( match Llvm.block_begin llf with
   | Before entry_blk ->
       let pop = pop_stack_frame_of_function x llf entry_blk in
diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index 5aeb3a79f..ad2fc4345 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -91,15 +91,15 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
         ; skip_throw= false
         ; function_summaries= true
         ; entry_points
-        ; globals= Declared Llair.Reg.Set.empty }
+        ; globals= Declared Llair.Global.Set.empty }
         pgm
     in
     Per_function
-      (Llair.Function.Map.map summary_table ~f:Llair.Reg.Set.union_list)
+      (Llair.Function.Map.map summary_table ~f:Llair.Global.Set.union_list)
   else
     Declared
-      (Llair.Reg.Set.of_iter
-         (Iter.map ~f:(fun g -> g.reg) (IArray.to_iter pgm.globals)))
+      (Llair.Global.Set.of_iter
+         (Iter.map ~f:(fun g -> g.name) (IArray.to_iter pgm.globals)))
 
 let analyze =
   let%map_open bound =
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 2de05504e..6adaa14ca 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -322,9 +322,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       else
         let globals = Domain_used_globals.by_function opts.globals name in
         let function_summary, post_state =
-          Dom.create_summary ~locals post_state
-            ~formals:
-              (Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals)
+          Dom.create_summary ~globals ~locals ~formals post_state
         in
         Llair.Function.Tbl.add_multi ~key:name ~data:function_summary
           summary_table ;
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index e18605ddc..0e24692f7 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -32,7 +32,7 @@ module type Dom = sig
 
   val call :
        summaries:bool
-    -> globals:Llair.Reg.Set.t
+    -> globals:Llair.Global.Set.t
     -> actuals:Llair.Exp.t list
     -> areturn:Llair.Reg.t option
     -> formals:Llair.Reg.t list
@@ -57,7 +57,11 @@ module type Dom = sig
   val pp_summary : summary pp
 
   val create_summary :
-    locals:Llair.Reg.Set.t -> formals:Llair.Reg.Set.t -> t -> summary * t
+       globals:Llair.Global.Set.t
+    -> locals:Llair.Reg.Set.t
+    -> formals:Llair.Reg.t list
+    -> t
+    -> summary * t
 
   val apply_summary : t -> summary -> t option
 end
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index 7caad0b76..c28bcbf72 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -12,8 +12,9 @@ module type State_domain_sig = sig
   include Domain_intf.Dom
 
   val create_summary :
-       locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.Set.t
+       globals:Llair.Global.Set.t
+    -> locals:Llair.Reg.Set.t
+    -> formals:Llair.Reg.t list
     -> entry:t
     -> current:t
     -> summary * t
@@ -79,8 +80,8 @@ module Make (State_domain : State_domain_sig) = struct
         (List.pp ",@ " Llair.Exp.pp)
         (List.rev actuals)
         (List.pp ",@ " Llair.Reg.pp)
-        (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals
-        State_domain.pp current]
+        (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp
+        globals State_domain.pp current]
     ;
     let caller_current, state_from_call =
       State_domain.call ~summaries ~globals ~actuals ~areturn ~formals
@@ -116,9 +117,9 @@ module Make (State_domain : State_domain_sig) = struct
 
   let pp_summary = State_domain.pp_summary
 
-  let create_summary ~locals ~formals (entry, current) =
+  let create_summary ~globals ~locals ~formals (entry, current) =
     let fs, next =
-      State_domain.create_summary ~locals ~formals ~entry ~current
+      State_domain.create_summary ~globals ~locals ~formals ~entry ~current
     in
     (fs, (entry, next))
 
diff --git a/sledge/src/domain_relation.mli b/sledge/src/domain_relation.mli
index 957abc1ae..0f1af3326 100644
--- a/sledge/src/domain_relation.mli
+++ b/sledge/src/domain_relation.mli
@@ -12,8 +12,9 @@ module type State_domain_sig = sig
   include Domain_intf.Dom
 
   val create_summary :
-       locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.Set.t
+       globals:Llair.Global.Set.t
+    -> locals:Llair.Reg.Set.t
+    -> formals:Llair.Reg.t list
     -> entry:t
     -> current:t
     -> summary * t
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 4ff5c8c29..60fed440c 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -22,8 +22,8 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 let init globals =
   IArray.fold globals Sh.emp ~f:(fun global q ->
       match (global : Llair.GlobalDefn.t) with
-      | {reg; init= Some (seq, siz)} ->
-          let loc = Term.var (X.reg reg) in
+      | {name; init= Some (seq, siz)} ->
+          let loc = Term.var (X.global name) in
           let len = Term.integer (Z.of_int siz) in
           let seq = X.term seq in
           Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
@@ -121,7 +121,8 @@ let localize_entry globals actuals formals freturn locals shadow pre entry =
   let formals_set = Var.Set.of_list formals in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let function_summary_pre =
-    garbage_collect entry ~wrt:(Var.Set.union formals_set (X.regs globals))
+    garbage_collect entry
+      ~wrt:(Var.Set.union formals_set (X.globals globals))
   in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
   let foot = Sh.exists formals_set function_summary_pre in
@@ -150,8 +151,8 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
       (List.pp ",@ " Llair.Exp.pp)
       (List.rev actuals)
       (List.pp ",@ " Llair.Reg.pp)
-      (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals pp
-      q]
+      (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp globals
+      pp q]
   ;
   let actuals = List.map ~f:X.term actuals in
   let areturn = Option.map ~f:X.reg areturn in
@@ -248,13 +249,18 @@ let pp_summary fs {xs; foot; post} =
   Format.fprintf fs "@[<v>xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs
     pp foot pp post
 
-let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
+let create_summary ~globals ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
-    pf "formals %a@ entry: %a@ current: %a" Llair.Reg.Set.pp formals pp
-      entry pp post]
+    pf "formals %a@ entry: %a@ current: %a"
+      (List.pp ",@ " Llair.Reg.pp)
+      formals pp entry pp post]
   ;
+  let globals = X.globals globals in
+  let formals =
+    Var.Set.of_iter (Iter.map ~f:X.reg (List.to_iter formals))
+  in
+  let formals = Var.Set.union formals globals in
   let locals = X.regs locals in
-  let formals = X.regs formals in
   let foot = Sh.exists locals entry in
   let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
   let restore_formals q =
diff --git a/sledge/src/domain_sh.mli b/sledge/src/domain_sh.mli
index e832aa8e7..70249f754 100644
--- a/sledge/src/domain_sh.mli
+++ b/sledge/src/domain_sh.mli
@@ -9,11 +9,10 @@
 
 include Domain_intf.Dom
 
-(* formals should include all the parameters of the summary. That is both
-   formals and globals. *)
 val create_summary :
-     locals:Llair.Reg.Set.t
-  -> formals:Llair.Reg.Set.t
+     globals:Llair.Global.Set.t
+  -> locals:Llair.Reg.Set.t
+  -> formals:Llair.Reg.t list
   -> entry:t
   -> current:t
   -> summary * t
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index 5d0ffb849..c8f6aeacd 100644
--- a/sledge/src/domain_unit.ml
+++ b/sledge/src/domain_unit.ml
@@ -39,5 +39,5 @@ let resolve_callee lookup ptr _ =
 type summary = unit
 
 let pp_summary fs () = Format.pp_print_string fs "()"
-let create_summary ~locals:_ ~formals:_ _ = ((), ())
+let create_summary ~globals:_ ~locals:_ ~formals:_ _ = ((), ())
 let apply_summary _ _ = Some ()
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 4267087c9..58accca28 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -7,28 +7,30 @@
 
 (** Used-globals abstract domain *)
 
-type t = Llair.Reg.Set.t [@@deriving equal, sexp]
+type t = Llair.Global.Set.t [@@deriving equal, sexp]
 
-let pp = Llair.Reg.Set.pp
+let pp = Llair.Global.Set.pp
 let report_fmt_thunk = Fun.flip pp
-let empty = Llair.Reg.Set.empty
+let empty = Llair.Global.Set.empty
 
 let init globals =
   [%Trace.info
     "pgm globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ;
   empty
 
-let join l r = Some (Llair.Reg.Set.union l r)
+let join l r = Some (Llair.Global.Set.union l r)
 let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
-let retn _ _ from_call post = Llair.Reg.Set.union from_call post
+let retn _ _ from_call post = Llair.Global.Set.union from_call post
 let dnf t = [t]
 
-let add_if_global v gs =
-  if Llair.Reg.is_global v then Llair.Reg.Set.add v gs else gs
+let used_globals exp s =
+  Llair.Exp.fold_exps exp s ~f:(fun e s ->
+      match Llair.Global.of_exp e with
+      | Some g -> Llair.Global.Set.add g s
+      | None -> s )
 
-let used_globals exp s = Llair.Exp.fold_regs ~f:add_if_global exp s
 let exec_assume st exp = Some (used_globals exp st)
 let exec_kill _ st = st
 
@@ -89,14 +91,14 @@ let resolve_callee lookup ptr st =
 type summary = t
 
 let pp_summary = pp
-let create_summary ~locals:_ ~formals:_ state = (state, state)
-let apply_summary st summ = Some (Llair.Reg.Set.union st summ)
+let create_summary ~globals:_ ~locals:_ ~formals:_ state = (state, state)
+let apply_summary st summ = Some (Llair.Global.Set.union st summ)
 
 (** Query *)
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
-  | Declared of Llair.Reg.Set.t
+  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
+  | Declared of Llair.Global.Set.t
 
 let by_function : r -> Llair.Function.t -> t =
  fun s fn ->
@@ -113,4 +115,4 @@ let by_function : r -> Llair.Function.t -> t =
            used-globals pre-analysis "
           Llair.Function.pp fn () ) )
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r]
+  [%Trace.retn fun {pf} r -> pf "%a" Llair.Global.Set.pp r]
diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli
index 2fe681252..c1a93a02e 100644
--- a/sledge/src/domain_used_globals.mli
+++ b/sledge/src/domain_used_globals.mli
@@ -7,11 +7,11 @@
 
 (** Used-globals abstract domain *)
 
-include Domain_intf.Dom with type summary = Llair.Reg.Set.t
+include Domain_intf.Dom with type summary = Llair.Global.Set.t
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
+  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
       (** per-function used-globals map *)
-  | Declared of Llair.Reg.Set.t  (** program-wide set *)
+  | Declared of Llair.Global.Set.t  (** program-wide set *)
 
 val by_function : r -> Llair.Function.t -> summary
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 896a65c9f..19695863b 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -62,7 +62,8 @@ module T = struct
   [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | Reg of {name: string; global: bool; typ: Typ.t}
+    | Reg of {name: string; typ: Typ.t}
+    | Global of {name: string; typ: Typ.t [@ignore]}
     | Function of {name: string; typ: Typ.t [@ignore]}
     | Label of {parent: string; name: string}
     | Integer of {data: Z.t; typ: Typ.t}
@@ -128,8 +129,8 @@ let rec pp fs exp =
     Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
   in
   match exp with
-  | Reg {name; global= true} -> pf "%@%s" name
-  | Reg {name; global= false} -> pf "%%%s" name
+  | Reg {name} -> pf "%%%s" name
+  | Global {name} -> pf "%@%s%a" name pp_demangled name
   | Function {name} -> pf "&%s%a" name pp_demangled name
   | Label {name} -> pf "%s" name
   | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
@@ -172,7 +173,7 @@ let valid_idx idx elts = 0 <= idx && idx < IArray.length elts
 let rec invariant exp =
   let@ () = Invariant.invariant [%here] exp [%sexp_of: t] in
   match exp with
-  | Reg {typ} -> assert (Typ.is_sized typ)
+  | Reg {typ} | Global {typ} -> assert (Typ.is_sized typ)
   | Function {typ= Pointer {elt= Function _}} -> ()
   | Function _ -> assert false
   | Integer {data; typ} -> (
@@ -251,7 +252,9 @@ let rec invariant exp =
 
 and typ_of exp =
   match exp with
-  | Reg {typ} | Function {typ} | Integer {typ} | Float {typ} -> typ
+  | Reg {typ} | Global {typ} | Function {typ} | Integer {typ} | Float {typ}
+    ->
+      typ
   | Label _ -> Typ.ptr
   | Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst
   | Ap1 (Select idx, typ, _) -> (
@@ -296,15 +299,38 @@ module Reg = struct
 
   let name = function Reg x -> x.name | r -> violates invariant r
   let typ = function Reg x -> x.typ | r -> violates invariant r
-  let is_global = function Reg x -> x.global | r -> violates invariant r
-  let pp_demangled ppf r = pp_demangled ppf (name r)
 
   let of_exp = function
     | Reg _ as e -> Some (e |> check invariant)
     | _ -> None
 
-  let program ?global typ name =
-    Reg {name; global= Option.is_some global; typ} |> check invariant
+  let mk typ name = Reg {name; typ} |> check invariant
+end
+
+(** Globals are the expressions constructed by [Global] *)
+module Global = struct
+  include T
+
+  let pp = pp
+
+  module Set = struct
+    include Set
+
+    let pp = Set.pp pp_exp
+  end
+
+  let invariant x =
+    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+    match x with Global _ -> invariant x | _ -> assert false
+
+  let name = function Global x -> x.name | r -> violates invariant r
+  let typ = function Global x -> x.typ | r -> violates invariant r
+
+  let of_exp = function
+    | Global _ as e -> Some (e |> check invariant)
+    | _ -> None
+
+  let mk typ name = Global {name; typ} |> check invariant
 end
 
 (** Function names are the expressions constructed by [Function] *)
@@ -338,6 +364,7 @@ let reg x = x
 (* constants *)
 
 let function_ f = f
+let global g = g
 let label ~parent ~name = Label {parent; name} |> check invariant
 let integer typ data = Integer {data; typ} |> check invariant
 let null = integer Typ.ptr Z.zero
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 1f0b7a32c..d94b04b52 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -72,7 +72,8 @@ type opN = Record  (** Record (array / struct) constant *)
 [@@deriving compare, equal, hash, sexp]
 
 type t = private
-  | Reg of {name: string; global: bool; typ: Typ.t}  (** Virtual register *)
+  | Reg of {name: string; typ: Typ.t}  (** Virtual register *)
+  | Global of {name: string; typ: Typ.t [@ignore]}  (** Global constant *)
   | Function of {name: string; typ: Typ.t [@ignore]}  (** Function name *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
@@ -104,15 +105,36 @@ module Reg : sig
   end
 
   val pp : t pp
-  val pp_demangled : t pp
 
   include Invariant.S with type t := t
 
   val of_exp : exp -> t option
-  val program : ?global:unit -> Typ.t -> string -> t
+  val mk : Typ.t -> string -> t
+  val name : t -> string
+  val typ : t -> Typ.t
+end
+
+(** Exp.Global is re-exported as Global *)
+module Global : sig
+  type exp := t
+  type t = private exp [@@deriving compare, equal, hash, sexp]
+
+  module Set : sig
+    include Set.S with type elt := t
+
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
+    val pp : t pp
+  end
+
+  val pp : t pp
+
+  include Invariant.S with type t := t
+
+  val of_exp : exp -> t option
+  val mk : Typ.t -> string -> t
   val name : t -> string
   val typ : t -> Typ.t
-  val is_global : t -> bool
 end
 
 (** Exp.Function is re-exported as Function *)
@@ -140,6 +162,7 @@ val reg : Reg.t -> t
 
 (* constants *)
 val function_ : Function.t -> t
+val global : Global.t -> t
 val label : parent:string -> name:string -> t
 val null : t
 val bool : bool -> t
@@ -199,6 +222,7 @@ val update : Typ.t -> rcd:t -> int -> elt:t -> t
 
 (** Traverse *)
 
+val fold_exps : t -> 's -> f:(t -> 's -> 's) -> 's
 val fold_regs : t -> 's -> f:(Reg.t -> 's -> 's) -> 's
 
 (** Query *)
diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml
new file mode 100644
index 000000000..185b20767
--- /dev/null
+++ b/sledge/src/llair/global.ml
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Globals *)
+
+include Exp.Global
diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/global.mli
new file mode 100644
index 000000000..74f2f0418
--- /dev/null
+++ b/sledge/src/llair/global.mli
@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Globals *)
+
+include module type of struct
+  include Exp.Global
+end
diff --git a/sledge/src/llair/globalDefn.ml b/sledge/src/llair/globalDefn.ml
index ca98b674e..f10b8539c 100644
--- a/sledge/src/llair/globalDefn.ml
+++ b/sledge/src/llair/globalDefn.ml
@@ -7,26 +7,18 @@
 
 (** Global variables *)
 
-type t = {reg: Reg.t; init: (Exp.t * int) option; loc: Loc.t}
+type t = {name: Global.t; init: (Exp.t * int) option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
-let pp fs {reg} =
-  let name = Reg.name reg in
-  let pf pp =
-    Format.pp_open_box fs 2 ;
-    Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp
-  in
-  pf "@%s%a" name Reg.pp_demangled reg
-
-let pp_defn fs {reg; init; loc} =
-  Format.fprintf fs "@[<2>%a %a%a %a@]" Typ.pp (Reg.typ reg) Reg.pp reg
+let pp ppf {name; init; loc} =
+  Format.fprintf ppf "@[<2>%a %a%a %a@]" Typ.pp (Global.typ name) Global.pp
+    name
     (Option.pp "@ = @[%a@]" Exp.pp)
     (Option.map ~f:fst init) Loc.pp loc
 
 let invariant g =
   let@ () = Invariant.invariant [%here] g [%sexp_of: t] in
-  let {reg} = g in
-  assert (Typ.is_sized (Reg.typ reg)) ;
-  assert (Reg.is_global reg)
+  let {name} = g in
+  assert (Typ.is_sized (Global.typ name))
 
-let mk ?init reg loc = {reg; init; loc} |> check invariant
+let mk ?init name loc = {name; init; loc} |> check invariant
diff --git a/sledge/src/llair/globalDefn.mli b/sledge/src/llair/globalDefn.mli
index d6550daf0..5eaa1e489 100644
--- a/sledge/src/llair/globalDefn.mli
+++ b/sledge/src/llair/globalDefn.mli
@@ -7,12 +7,11 @@
 
 (** Global variables *)
 
-type t = private {reg: Reg.t; init: (Exp.t * int) option; loc: Loc.t}
+type t = private {name: Global.t; init: (Exp.t * int) option; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
-val pp_defn : t pp
 
 include Invariant.S with type t := t
 
-val mk : ?init:Exp.t * int -> Reg.t -> Loc.t -> t
+val mk : ?init:Exp.t * int -> Global.t -> Loc.t -> t
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 6d3bacc5a..f7a4a3516 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -14,6 +14,7 @@ module Typ = Typ
 module Reg = Reg
 module Exp = Exp
 module Function = Function
+module Global = Global
 module GlobalDefn = GlobalDefn
 
 type inst =
@@ -228,7 +229,7 @@ and dummy_func =
         "dummy"
   ; formals= []
   ; freturn= None
-  ; fthrow= Reg.program Typ.ptr "dummy"
+  ; fthrow= Reg.mk Typ.ptr "dummy"
   ; locals= Reg.Set.empty
   ; entry= dummy_block
   ; loc= Loc.none }
@@ -601,7 +602,7 @@ module Program = struct
     assert (
       not
         (Iter.contains_dup (IArray.to_iter pgm.globals) ~cmp:(fun g1 g2 ->
-             Reg.compare g1.GlobalDefn.reg g2.GlobalDefn.reg )) )
+             Global.compare g1.name g2.name )) )
 
   let mk ~globals ~functions =
     { globals= IArray.of_list_rev globals
@@ -610,7 +611,7 @@ module Program = struct
 
   let pp fs {globals; functions} =
     Format.fprintf fs "@[<v>@[%a@]@ @ @ @[%a@]@]"
-      (IArray.pp "@\n@\n" GlobalDefn.pp_defn)
+      (IArray.pp "@\n@\n" GlobalDefn.pp)
       globals
       (List.pp "@\n@\n" Func.pp)
       ( Function.Map.values functions
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index f4679c3e8..d65cadf11 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -13,6 +13,7 @@ module Typ = Typ
 module Reg = Reg
 module Exp = Exp
 module Function = Function
+module Global = Global
 module GlobalDefn = GlobalDefn
 
 (** Instructions for memory manipulation or other non-control effects. *)
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index a7de81324..cb80fcf8a 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -13,10 +13,16 @@ let func f =
   let name = Llair.Function.name f in
   Var.program ~name ~global:true
 
+let global g =
+  let name = Llair.Global.name g in
+  Var.program ~name ~global:true
+
+let globals gs =
+  Var.Set.of_iter (Iter.map ~f:global (Llair.Global.Set.to_iter gs))
+
 let reg r =
   let name = Llair.Reg.name r in
-  let global = Llair.Reg.is_global r in
-  Var.program ~name ~global
+  Var.program ~name ~global:false
 
 let regs rs = Var.Set.of_iter (Iter.map ~f:reg (Llair.Reg.Set.to_iter rs))
 let uap0 f = T.apply f [||]
@@ -67,7 +73,8 @@ and term : Llair.Exp.t -> T.t =
       F.inject
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
-  | Reg {name; global; typ= _} -> T.var (Var.program ~name ~global)
+  | Reg {name; typ= _} -> T.var (Var.program ~name ~global:false)
+  | Global {name; typ= _} -> T.var (Var.program ~name ~global:true)
   | Function {name; typ= _} -> T.var (Var.program ~name ~global:true)
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
index 8ca00887c..ac1c3de82 100644
--- a/sledge/src/llair_to_Fol.mli
+++ b/sledge/src/llair_to_Fol.mli
@@ -8,6 +8,8 @@
 open Fol
 
 val func : Llair.Function.t -> Var.t
+val global : Llair.Global.t -> Var.t
+val globals : Llair.Global.Set.t -> Var.Set.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
 val term : Llair.Exp.t -> Term.t