diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 57de85232..93bcdbc41 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -23,7 +23,7 @@ let init globals =
   IArray.fold globals Sh.emp ~f:(fun global q ->
       match (global : Llair.GlobalDefn.t) with
       | {name; init= Some (seq, siz)} ->
-          let loc = Term.var (X.global name) in
+          let loc = 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})
@@ -114,8 +114,7 @@ let localize_entry globals actuals formals freturn locals shadow pre entry =
   let wrt =
     Term.Set.of_iter
       (Iter.append
-         (Iter.map ~f:(Term.var << X.global)
-            (Llair.Global.Set.to_iter globals))
+         (Iter.map ~f:X.global (Llair.Global.Set.to_iter globals))
          (Iter.map ~f:Term.var (List.to_iter formals)))
   in
   let function_summary_pre = garbage_collect entry ~wrt in
diff --git a/sledge/src/fol/funsym.ml b/sledge/src/fol/funsym.ml
index 2d4401b7f..059c135db 100644
--- a/sledge/src/fol/funsym.ml
+++ b/sledge/src/fol/funsym.ml
@@ -32,7 +32,11 @@ let pp ppf f =
   | BitAshr -> pf "ashr"
   | Signed n -> pf "(s%i)" n
   | Unsigned n -> pf "(u%i)" n
-  | Uninterp sym -> pf "%s" sym
+  | Uninterp sym ->
+      if String.is_empty sym then pf ""
+      else if Char.equal sym.[0] '@' || Char.equal sym.[0] '%' then
+        Trace.pp_styled `Bold "%s" ppf sym
+      else pf "%s" sym
 
 let uninterp s = Uninterp s
 
diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index d00459e33..d292fe294 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -121,16 +121,16 @@ end = struct
     if x == y then 0
     else
       match (x, y) with
-      | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-          Int.compare i j
+      | Var {id= 0; name= s}, Var {id= 0; name= t} -> String.compare s t
+      | Var {id= i; name= _}, Var {id= j; name= _} -> Int.compare i j
       | _ -> compare x y
 
   let equal x y =
     x == y
     ||
     match (x, y) with
-    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-        Int.equal i j
+    | Var {id= 0; name= s}, Var {id= 0; name= t} -> String.equal s t
+    | Var {id= i; name= _}, Var {id= j; name= _} -> Int.equal i j
     | _ -> equal x y
 
   let rec ppx strength fs trm =
diff --git a/sledge/src/fol/var0.ml b/sledge/src/fol/var0.ml
index 1ef6193fb..714c640c6 100644
--- a/sledge/src/fol/var0.ml
+++ b/sledge/src/fol/var0.ml
@@ -16,15 +16,13 @@ module Make (T : REPR) = struct
   let ppx strength ppf v =
     let id = id v in
     let name = name v in
-    match id with
-    | -1 -> Trace.pp_styled `Bold "%@%s" ppf name
-    | 0 -> Trace.pp_styled `Bold "%%%s" ppf name
-    | _ -> (
+    if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name
+    else
       match strength v with
       | None -> Format.fprintf ppf "%%%s_%d" name id
       | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" ppf name id
       | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" ppf name id
-      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf )
+      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
 
   let pp = ppx (fun _ -> None)
 
@@ -52,7 +50,7 @@ module Make (T : REPR) = struct
     let x' = make ~id:(max + 1) ~name in
     (x', Set.add x' wrt)
 
-  let program ~name ~global = make ~id:(if global then -1 else 0) ~name
+  let program ~name = make ~id:0 ~name
   let identified ~name ~id = make ~id ~name
 
   (** Variable renaming substitutions *)
diff --git a/sledge/src/fol/var_intf.ml b/sledge/src/fol/var_intf.ml
index 4e6d8d16c..92d2d0801 100644
--- a/sledge/src/fol/var_intf.ml
+++ b/sledge/src/fol/var_intf.ml
@@ -40,7 +40,7 @@ module type VAR = sig
 
   val id : t -> int
   val name : t -> string
-  val program : name:string -> global:bool -> t
+  val program : name:string -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index cb80fcf8a..83ed46363 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -9,21 +9,9 @@ open Fol
 module T = Term
 module F = Formula
 
-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
-  Var.program ~name ~global:false
-
+let uconst name = T.apply (Funsym.uninterp ("@" ^ name)) [||]
+let global g = uconst (Llair.Global.name g)
+let reg r = Var.program ~name:(Llair.Reg.name r)
 let regs rs = Var.Set.of_iter (Iter.map ~f:reg (Llair.Reg.Set.to_iter rs))
 let uap0 f = T.apply f [||]
 let uap1 f a = T.apply f [|a|]
@@ -73,9 +61,8 @@ and term : Llair.Exp.t -> T.t =
       F.inject
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
-  | 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)
+  | Reg {name; typ= _} -> T.var (Var.program ~name)
+  | Global {name; typ= _} | Function {name; typ= _} -> uconst name
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
   | Integer {typ= _; data} -> T.integer data
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
index ac1c3de82..18bfac78a 100644
--- a/sledge/src/llair_to_Fol.mli
+++ b/sledge/src/llair_to_Fol.mli
@@ -7,9 +7,7 @@
 
 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 global : Llair.Global.t -> Term.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
 val term : Llair.Exp.t -> Term.t