diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 30c5a7eab..4cf94efd1 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -205,5 +205,6 @@ val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
 (** Query *)
 
 val term : t -> Term.t
+val typ : t -> Typ.t
 val is_true : t -> bool
 val is_false : t -> bool
diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index c0850c2f6..9219f4305 100644
--- a/sledge/src/llair/frontend.ml
+++ b/sledge/src/llair/frontend.ml
@@ -654,13 +654,8 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
       Hashtbl.set memo_global ~key:llg ~data:(Global.mk g typ loc) ;
       let init =
         match Llvm.classify_value llg with
-        | GlobalVariable -> (
-          match Llvm.global_initializer llg with
-          | Some llinit ->
-              let siz = size_of x (Llvm.element_type llt) in
-              let init = xlate_value x llinit in
-              Some (init, siz)
-          | _ -> None )
+        | GlobalVariable ->
+            Option.map ~f:(xlate_value x) (Llvm.global_initializer llg)
         | _ -> None
       in
       Global.mk ?init g typ loc
diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml
index fcbd41c52..a095996a1 100644
--- a/sledge/src/llair/global.ml
+++ b/sledge/src/llair/global.ml
@@ -7,7 +7,7 @@
 
 (** Global variables *)
 
-type t = {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
+type t = {reg: Reg.t; init: Exp.t option; typ: Typ.t; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 let pp fs {reg} =
@@ -20,7 +20,7 @@ let pp fs {reg} =
 
 let pp_defn fs {reg; init; typ; loc} =
   Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Reg.pp reg Loc.pp loc
-    (Option.pp "@ = @[%a@]" (fun fs (init, _) -> Exp.pp fs init))
+    (Option.pp "@ = @[%a@]" Exp.pp)
     init
 
 let invariant g =
diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/global.mli
index 0d22cfc88..5f6200005 100644
--- a/sledge/src/llair/global.mli
+++ b/sledge/src/llair/global.mli
@@ -7,8 +7,7 @@
 
 (** Global variables *)
 
-type t = private
-  {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t}
+type t = private {reg: Reg.t; init: Exp.t option; typ: Typ.t; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
@@ -16,4 +15,4 @@ val pp_defn : t pp
 
 include Invariant.S with type t := t
 
-val mk : ?init:Exp.t * int -> Reg.t -> Typ.t -> Loc.t -> t
+val mk : ?init:Exp.t -> Reg.t -> Typ.t -> Loc.t -> t
diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml
index 56aeb4a6e..fb060c501 100644
--- a/sledge/src/symbheap/sh_domain.ml
+++ b/sledge/src/symbheap/sh_domain.ml
@@ -19,9 +19,9 @@ let report_fmt_thunk = Fn.flip pp
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Global.reg; init= Some (arr, siz)} ->
+    | {Global.reg; init= Some arr} ->
         let loc = Term.var (Reg.var reg) in
-        let len = Term.integer (Z.of_int siz) in
+        let len = Term.size_of (Exp.typ arr) in
         let arr = arr.term in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )