diff --git a/sledge/src/domain/itv.ml b/sledge/src/domain/itv.ml
index 70cb93ef0..43e3a4da5 100644
--- a/sledge/src/domain/itv.ml
+++ b/sledge/src/domain/itv.ml
@@ -106,7 +106,7 @@ and apron_texpr_of_llair_term tm q typ =
         try Float.of_string data with _ -> failwith "malformed float: %s"
       in
       Some (Texpr1.Cst (Coeff.s_of_float f))
-  | Ap1 (Convert {unsigned= false; dst; src}, t) -> (
+  | Ap1 (Convert {dst; src}, t) -> (
     match (apron_typ_of_llair_typ dst, apron_typ_of_llair_typ src) with
     | None, _ | _, None -> None
     | Some dst, Some src ->
@@ -117,8 +117,7 @@ and apron_texpr_of_llair_term tm q typ =
           Some (Texpr1.Unop (Texpr1.Cast, t, dst, Texpr0.Rnd)) )
   (* extraction to unsigned 1-bit int is llvm encoding of C boolean;
      restrict to [0,1] *)
-  | Ap1 (Extract {unsigned= true; bits= 1}, _t) ->
-      Some (Texpr1.Cst (Coeff.i_of_int 0 1))
+  | Ap1 (Unsigned {bits= 1}, _t) -> Some (Texpr1.Cst (Coeff.i_of_int 0 1))
   (* "t xor true" and "true xor t" are negation *)
   | Ap2 (Xor, t, Integer {data}) when Z.is_true data ->
       let%map t = apron_texpr_of_llair_term t q typ in
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 5a31effdd..eff512c30 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -13,7 +13,9 @@ module T = struct
   module T0 = struct
     type op1 =
       (* conversion *)
-      | Convert of {unsigned: bool; dst: Typ.t}
+      | Signed of {bits: int}
+      | Unsigned of {bits: int}
+      | Convert of {src: Typ.t}
       (* array/struct operations *)
       | Select of int
     [@@deriving compare, equal, hash, sexp]
@@ -150,11 +152,11 @@ let rec pp fs exp =
     | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
     | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
     | Float {data} -> pf "%s" data
-    | Ap1 (Convert {dst; unsigned= true}, Integer {bits}, arg) ->
+    | Ap1 (Signed {bits}, dst, arg) ->
+        pf "((%a)(s%i)@ %a)" Typ.pp dst bits pp arg
+    | Ap1 (Unsigned {bits}, dst, arg) ->
         pf "((%a)(u%i)@ %a)" Typ.pp dst bits pp arg
-    | Ap1 (Convert {dst= Integer {bits}; unsigned= true}, src, arg) ->
-        pf "((u%i)(%a)@ %a)" bits Typ.pp src pp arg
-    | Ap1 (Convert {dst}, src, arg) ->
+    | Ap1 (Convert {src}, dst, arg) ->
         pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg
     | Ap1 (Select idx, _, rcd) -> pf "%a[%i]" pp rcd idx
     | Ap2 (Splat, _, byt, siz) -> pf "%a^%a" pp byt pp siz
@@ -211,10 +213,19 @@ let rec invariant exp =
   | Float {typ} -> (
     match typ with Float _ -> assert true | _ -> assert false )
   | Label _ -> assert true
-  | Ap1 (Convert {dst}, src, arg) ->
-      assert (not (Typ.equal dst src)) ;
-      assert (Typ.convertible dst src) ;
-      assert (Typ.castable src (typ_of arg))
+  | Ap1 (Signed {bits}, dst, arg) -> (
+    match (dst, typ_of arg) with
+    | Integer {bits= dst_bits}, Typ.Integer _ -> assert (bits <= dst_bits)
+    | _ -> assert false )
+  | Ap1 (Unsigned {bits}, dst, arg) -> (
+    match (dst, typ_of arg) with
+    | Integer {bits= dst_bits}, Typ.Integer _ -> assert (bits < dst_bits)
+    | _ -> assert false )
+  | Ap1 (Convert {src= Integer _}, Integer _, _) -> assert false
+  | Ap1 (Convert {src}, dst, arg) ->
+      assert (Typ.convertible src dst) ;
+      assert (Typ.castable src (typ_of arg)) ;
+      assert (not (Typ.equal src dst) (* avoid redundant representations *))
   | Ap1 (Select idx, typ, rcd) -> (
       assert (Typ.castable typ (typ_of rcd)) ;
       match typ with
@@ -273,7 +284,7 @@ and typ_of exp =
   match exp.desc with
   | Reg {typ} | Nondet {typ} | Integer {typ} | Float {typ} -> typ
   | Label _ -> Typ.ptr
-  | Ap1 (Convert {dst}, _, _) -> dst
+  | Ap1 ((Signed _ | Unsigned _ | Convert _), dst, _) -> dst
   | Ap1 (Select idx, typ, _) -> (
     match typ with
     | Array {elt} -> elt
@@ -411,11 +422,17 @@ let float typ data =
 
 (* type conversions *)
 
-let convert ?(unsigned = false) ~dst ~src exp =
-  ( if (not unsigned) && Typ.equal dst src then exp
-  else
-    { desc= Ap1 (Convert {unsigned; dst}, src, exp)
-    ; term= Term.convert ~unsigned ~dst ~src exp.term } )
+let signed bits x ~to_:typ =
+  {desc= Ap1 (Signed {bits}, typ, x); term= Term.signed bits x.term}
+  |> check invariant
+
+let unsigned bits x ~to_:typ =
+  {desc= Ap1 (Unsigned {bits}, typ, x); term= Term.unsigned bits x.term}
+  |> check invariant
+
+let convert src ~to_:dst exp =
+  { desc= Ap1 (Convert {src}, dst, exp)
+  ; term= Term.convert src ~to_:dst exp.term }
   |> check invariant
 
 (* comparisons *)
@@ -427,8 +444,8 @@ let binary op mk ?typ x y =
 let ubinary op mk ?typ x y =
   let typ = match typ with Some typ -> typ | None -> typ_of x in
   let umk x y =
-    let extract = Term.extract ~unsigned:true ~bits:(Typ.bit_size_of typ) in
-    mk (extract x) (extract y)
+    let unsigned = Term.unsigned (Typ.bit_size_of typ) in
+    mk (unsigned x) (unsigned y)
   in
   binary op umk ~typ x y
 
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 160f26108..c6a05a34a 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -11,14 +11,25 @@
     bitwise-logical, etc. operations over literal values and registers. *)
 
 type op1 =
-  | Convert of {unsigned: bool; dst: Typ.t}
-      (** Convert between specified types, possibly with loss of
-          information. In [Ap1 (Convert {unsigned; dst}, src, arg)], if
-          [src] is an [Integer] type, then [unsigned] indicates that [arg]
-          should be interpreted as an [unsigned] integer. If [src] is a
-          [Float] type and [dst] is an [Integer] type, then [unsigned]
-          indidates that the result should be the nearest non-negative
-          value. *)
+  | Signed of {bits: int}
+      (** [Ap1 (Signed {bits= n}, dst, arg)] is [arg] interpreted as an
+          [n]-bit signed integer and injected into the [dst] type. That is,
+          it two's-complement--decodes the low [n] bits of the infinite
+          two's-complement encoding of [arg]. The injection into [dst] is a
+          no-op, so [dst] must be an integer type with bitwidth at least
+          [n]. *)
+  | Unsigned of {bits: int}
+      (** [Ap1 (Unsigned {bits= n}, dst, arg)] is [arg] interpreted as an
+          [n]-bit unsigned integer and injected into the [dst] type. That
+          is, it unsigned-binary--decodes the low [n] bits of the infinite
+          two's-complement encoding of [arg]. The injection into [dst] is a
+          no-op, so [dst] must be an integer type with bitwidth greater than
+          [n]. *)
+  | Convert of {src: Typ.t}
+      (** [Ap1 (Convert {src}, dst, arg)] is [arg] converted from type [src]
+          to type [dst], possibly with loss of information. The [src] and
+          [dst] types must be [Typ.convertible] and must not both be
+          [Integer] types. *)
   | Select of int  (** Select an index from a record *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -140,7 +151,9 @@ val integer : Typ.t -> Z.t -> t
 val float : Typ.t -> string -> t
 
 (* type conversions *)
-val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
+val signed : int -> t -> to_:Typ.t -> t
+val unsigned : int -> t -> to_:Typ.t -> t
+val convert : Typ.t -> to_:Typ.t -> t -> t
 
 (* comparisons *)
 val eq : ?typ:Typ.t -> t -> t -> t
diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/llair/exp_test.ml
new file mode 100644
index 000000000..07bb74028
--- /dev/null
+++ b/sledge/src/llair/exp_test.ml
@@ -0,0 +1,49 @@
+(*
+ * 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.
+ *)
+
+let%test_module _ =
+  ( module struct
+    (* let () = Trace.init ~margin:68 ~config:all () *)
+    let () = Trace.init ~margin:68 ~config:none ()
+
+    open Exp
+
+    let pp e = Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp e.term
+    let ( ! ) i = integer Typ.siz (Z.of_int i)
+
+    let%expect_test _ =
+      pp (signed 1 !1 ~to_:Typ.bool) ;
+      [%expect {| {desc= ((i1)(s1) 1); term= -1} |}]
+
+    let%expect_test _ =
+      pp (unsigned 1 !(-1) ~to_:Typ.byt) ;
+      [%expect {| {desc= ((i8)(u1) -1); term= 1} |}]
+
+    let%expect_test _ =
+      pp (signed 8 !(-1) ~to_:Typ.int) ;
+      [%expect {| {desc= ((i32)(s8) -1); term= -1} |}]
+
+    let%expect_test _ =
+      pp (unsigned 8 !(-1) ~to_:Typ.int) ;
+      [%expect {| {desc= ((i32)(u8) -1); term= 255} |}]
+
+    let%expect_test _ =
+      pp (signed 8 !255 ~to_:Typ.byt) ;
+      [%expect {| {desc= ((i8)(s8) 255); term= -1} |}]
+
+    let%expect_test _ =
+      pp (signed 7 !255 ~to_:Typ.byt) ;
+      [%expect {| {desc= ((i8)(s7) 255); term= -1} |}]
+
+    let%expect_test _ =
+      pp (unsigned 7 !255 ~to_:Typ.byt) ;
+      [%expect {| {desc= ((i8)(u7) 255); term= 127} |}]
+
+    let%expect_test _ =
+      pp (uge (integer Typ.bool Z.minus_one) (signed 1 !1 ~to_:Typ.bool)) ;
+      [%expect {| {desc= (-1 u≥ ((i1)(s1) 1)); term= -1} |}]
+  end )
diff --git a/sledge/src/llair/exp_test.mli b/sledge/src/llair/exp_test.mli
new file mode 100644
index 000000000..81857a06f
--- /dev/null
+++ b/sledge/src/llair/exp_test.mli
@@ -0,0 +1,6 @@
+(*
+ * 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.
+ *)
diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index f967f9dd9..b3438d453 100644
--- a/sledge/src/llair/frontend.ml
+++ b/sledge/src/llair/frontend.ml
@@ -22,7 +22,7 @@ type llvaluekind = [%import: (Llvm.ValueKind.t[@with Opcode.t := llopcode])]
 [@@deriving sexp]
 
 let _pp_lllinkage fs l = Sexp.pp_hum fs (sexp_of_lllinkage l)
-let _pp_llopcode fs l = Sexp.pp_hum fs (sexp_of_llopcode l)
+let pp_llopcode fs l = Sexp.pp_hum fs (sexp_of_llopcode l)
 let pp_llvaluekind fs l = Sexp.pp_hum fs (sexp_of_llvaluekind l)
 
 exception Invalid_llvm of string
@@ -356,8 +356,18 @@ let ptr_idx x ~ptr ~idx ~llelt =
   Exp.add ~typ:Typ.ptr ptr
     (Exp.mul ~typ:Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx)
 
+let convert_to_siz =
+  let siz_bits = Typ.bit_size_of Typ.siz in
+  fun typ arg ->
+    match (typ : Typ.t) with
+    | Integer {bits} ->
+        if siz_bits < bits then Exp.signed siz_bits arg ~to_:Typ.siz
+        else if siz_bits > bits then Exp.signed bits arg ~to_:Typ.siz
+        else arg
+    | _ -> fail "convert_to_siz: %a" Typ.pp typ ()
+
 let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t =
- fun x typ arg -> Exp.convert ~dst:(i32 x) ~src:typ arg
+ fun x typ arg -> Exp.convert typ ~to_:(i32 x) arg
 
 let rec xlate_intrinsic_exp : string -> (x -> Llvm.llvalue -> Exp.t) option
     =
@@ -479,12 +489,20 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
       ( if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then
         todo "vector operations: %a" pp_llvalue llv () )
   in
-  let convert ?unsigned () =
+  let convert opcode =
     let dst = Lazy.force typ in
     let rand = Llvm.operand llv 0 in
     let src = xlate_type x (Llvm.type_of rand) in
     let arg = xlate_value x rand in
-    Exp.convert ?unsigned ~dst ~src arg
+    match opcode with
+    | Trunc -> Exp.signed (Typ.bit_size_of dst) arg ~to_:dst
+    | SExt -> Exp.signed (Typ.bit_size_of src) arg ~to_:dst
+    | ZExt -> Exp.unsigned (Typ.bit_size_of src) arg ~to_:dst
+    | (BitCast | AddrSpaceCast) when Typ.equal dst src -> arg
+    | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc | FPExt | PtrToInt
+     |IntToPtr | BitCast | AddrSpaceCast ->
+        Exp.convert src ~to_:dst arg
+    | _ -> fail "convert: %a" pp_llopcode opcode ()
   in
   let binary (mk : ?typ:_ -> _) =
     Lazy.force check_vector ;
@@ -496,10 +514,9 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
         Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) )
   in
   ( match opcode with
-  | AddrSpaceCast | BitCast -> convert ()
-  | Trunc | ZExt | FPToUI | UIToFP | PtrToInt | IntToPtr ->
-      convert ~unsigned:true ()
-  | SExt | FPTrunc | FPExt | FPToSI | SIToFP -> convert ()
+  | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc
+   |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast ->
+      convert opcode
   | ICmp -> (
     match Option.value_exn (Llvm.icmp_predicate llv) with
     | Eq -> binary Exp.eq
@@ -602,15 +619,16 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
       if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then
         todo "vector operations: %a" pp_llvalue llv () ;
       let len = Llvm.num_operands llv in
-      if len <= 1 then convert ()
+      assert (len > 0 || invalid_llvm (Llvm.string_of_llvalue llv)) ;
+      if len = 1 then convert BitCast
       else
         let rec xlate_indices i =
           [%Trace.call fun {pf} ->
             pf "%i %a" i pp_llvalue (Llvm.operand llv i)]
           ;
           let idx =
-            Exp.convert ~dst:Typ.siz
-              ~src:(xlate_type x (Llvm.type_of (Llvm.operand llv i)))
+            convert_to_siz
+              (xlate_type x (Llvm.type_of (Llvm.operand llv i)))
               (xlate_rand i)
           in
           ( if i = 1 then
@@ -891,8 +909,8 @@ let xlate_instr :
       let reg = xlate_name x instr in
       let rand = Llvm.operand instr 0 in
       let num =
-        Exp.convert ~dst:Typ.siz
-          ~src:(xlate_type x (Llvm.type_of rand))
+        convert_to_siz
+          (xlate_type x (Llvm.type_of rand))
           (xlate_value x rand)
       in
       assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
@@ -936,8 +954,8 @@ let xlate_instr :
             let reg = xlate_name x instr in
             let num_operand = Llvm.operand instr 0 in
             let num =
-              Exp.convert ~dst:Typ.siz
-                ~src:(xlate_type x (Llvm.type_of num_operand))
+              convert_to_siz
+                (xlate_type x (Llvm.type_of num_operand))
                 (xlate_value x num_operand)
             in
             let len = Exp.integer Typ.siz (Z.of_int 1) in
diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 92937b699..e9e4db10c 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -9,20 +9,13 @@
 
 [@@@warning "+9"]
 
-module Z = struct
-  include Z
-
-  (** Interpret as a bounded integer with specified signedness and width. *)
-  let extract ?(unsigned = false) bits z =
-    if unsigned then Z.extract z 0 bits else Z.signed_extract z 0 bits
-end
-
 module rec T : sig
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type op1 =
-    | Extract of {unsigned: bool; bits: int}
-    | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
+    | Signed of {bits: int}
+    | Unsigned of {bits: int}
+    | Convert of {src: Typ.t; dst: Typ.t}
     | Select of int
   [@@deriving compare, equal, hash, sexp]
 
@@ -81,8 +74,9 @@ and T0 : sig
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type op1 =
-    | Extract of {unsigned: bool; bits: int}
-    | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
+    | Signed of {bits: int}
+    | Unsigned of {bits: int}
+    | Convert of {src: Typ.t; dst: Typ.t}
     | Select of int
   [@@deriving compare, equal, hash, sexp]
 
@@ -128,8 +122,9 @@ end = struct
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type op1 =
-    | Extract of {unsigned: bool; bits: int}
-    | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
+    | Signed of {bits: int}
+    | Unsigned of {bits: int}
+    | Convert of {src: Typ.t; dst: Typ.t}
     | Select of int
   [@@deriving compare, equal, hash, sexp]
 
@@ -219,13 +214,9 @@ let rec pp ?is_x fs term =
     | Float {data} -> pf "%s" data
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
-    | Ap1 (Extract {unsigned; bits}, arg) ->
-        pf "(%s%i)@ %a" (if unsigned then "u" else "i") bits pp arg
-    | Ap1 (Convert {dst; unsigned= true; src= Integer {bits}}, arg) ->
-        pf "((%a)(u%i)@ %a)" Typ.pp dst bits pp arg
-    | Ap1 (Convert {unsigned= true; dst= Integer {bits}; src}, arg) ->
-        pf "((u%i)(%a)@ %a)" bits Typ.pp src pp arg
-    | Ap1 (Convert {dst; src}, arg) ->
+    | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg
+    | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg
+    | Ap1 (Convert {src; dst}, arg) ->
         pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg
     | Ap2 (Eq, x, y) -> pf "(%a@ = %a)" pp x pp y
     | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y
@@ -352,9 +343,12 @@ let invariant e =
   | ApN (Concat, mems) -> assert (Vector.length mems <> 1)
   | ApN (Record, elts) | RecN (Record, elts) ->
       assert (not (Vector.is_empty elts))
-  | Ap1 (Convert {dst; src}, _) ->
-      assert (not (Typ.equivalent dst src)) ;
-      assert (Typ.convertible dst src)
+  | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false
+  | Ap1 (Convert {src; dst}, _) ->
+      assert (Typ.convertible src dst) ;
+      assert (
+        not (Typ.equivalent src dst) (* avoid redundant representations *)
+      )
   | _ -> ()
   [@@warning "-9"]
 
@@ -500,27 +494,18 @@ let label ~parent ~name = Label {parent; name} |> check invariant
 
 (* type conversions *)
 
-let simp_extract ~unsigned bits arg =
+let simp_signed bits arg =
   match arg with
-  | Integer {data} -> integer (Z.extract ~unsigned bits data)
-  | _ -> Ap1 (Extract {unsigned; bits}, arg)
-
-let simp_convert ~unsigned dst src arg =
-  match (dst, src) with
-  | Typ.Integer {bits= m; _}, Typ.Integer {bits= n; _} -> (
-      if m < n then
-        match arg with
-        | Integer {data} -> integer (Z.extract m data)
-        | _ -> Ap1 (Convert {unsigned= false; dst; src}, arg)
-      else
-        match arg with
-        | Integer {data} -> integer (Z.extract ~unsigned n data)
-        | _ ->
-            if unsigned then Ap1 (Convert {unsigned; dst; src}, arg)
-            else arg )
-  | _ ->
-      if Typ.equivalent dst src then arg
-      else Ap1 (Convert {unsigned; dst; src}, arg)
+  | Integer {data} -> integer (Z.signed_extract data 0 bits)
+  | _ -> Ap1 (Signed {bits}, arg)
+
+let simp_unsigned bits arg =
+  match arg with
+  | Integer {data} -> integer (Z.extract data 0 bits)
+  | _ -> Ap1 (Unsigned {bits}, arg)
+
+let simp_convert src dst arg =
+  if Typ.equivalent src dst then arg else Ap1 (Convert {src; dst}, arg)
 
 (* arithmetic *)
 
@@ -685,7 +670,7 @@ let simp_cond cnd thn els =
 (* boolean / bitwise *)
 
 let rec is_boolean = function
-  | Ap1 ((Extract {bits= 1; _} | Convert {dst= Integer {bits= 1; _}; _}), _)
+  | Ap1 ((Unsigned {bits= 1} | Convert {dst= Integer {bits= 1; _}; _}), _)
    |Ap2 ((Eq | Dq | Lt | Le), _, _) ->
       true
   | Ap2 ((Div | Rem | And | Or | Xor | Shl | Lshr | Ashr), x, y)
@@ -898,8 +883,9 @@ let rec_app key =
 
 let norm1 op x =
   ( match op with
-  | Extract {unsigned; bits} -> simp_extract ~unsigned bits x
-  | Convert {unsigned; dst; src} -> simp_convert ~unsigned dst src x
+  | Signed {bits} -> simp_signed bits x
+  | Unsigned {bits} -> simp_unsigned bits x
+  | Convert {src; dst} -> simp_convert src dst x
   | Select idx -> simp_select idx x )
   |> check invariant
 
@@ -933,12 +919,9 @@ let normN op xs =
 
 (* exposed interface *)
 
-let extract ?(unsigned = false) ~bits term =
-  norm1 (Extract {unsigned; bits}) term
-
-let convert ?(unsigned = false) ~dst ~src term =
-  norm1 (Convert {unsigned; dst; src}) term
-
+let signed bits term = norm1 (Signed {bits}) term
+let unsigned bits term = norm1 (Unsigned {bits}) term
+let convert src ~to_:dst term = norm1 (Convert {src; dst}) term
 let eq = norm2 Eq
 let dq = norm2 Dq
 let lt = norm2 Lt
diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli
index 4e6b82fce..ab3804b3f 100644
--- a/sledge/src/llair/term.mli
+++ b/sledge/src/llair/term.mli
@@ -13,15 +13,19 @@
 type comparator_witness
 
 type op1 =
-  | Extract of {unsigned: bool; bits: int}
-      (** Interpret integer argument with given signedness and bitwidth. *)
-  | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
-      (** Convert between specified types, possibly with loss of
-          information. If [src] is an [Integer] type, then [unsigned]
-          indicates that the argument should be interpreted as an [unsigned]
-          integer. If [src] is a [Float] type and [dst] is an [Integer]
-          type, then [unsigned] indidates that the result should be the
-          nearest non-negative value. *)
+  | Signed of {bits: int}
+      (** [Ap1 (Signed {bits= n}, arg)] is [arg] interpreted as an [n]-bit
+          signed integer. That is, it two's-complement--decodes the low [n]
+          bits of the infinite two's-complement encoding of [arg]. *)
+  | Unsigned of {bits: int}
+      (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit
+          unsigned integer. That is, it unsigned-binary--decodes the low [n]
+          bits of the infinite two's-complement encoding of [arg]. *)
+  | Convert of {src: Typ.t; dst: Typ.t}
+      (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src]
+          to type [dst], possibly with loss of information. The [src] and
+          [dst] types must be [Typ.convertible] and must not both be
+          [Integer] types. *)
   | Select of int  (** Select an index from a record *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -151,8 +155,9 @@ val rational : Q.t -> t
 val float : string -> t
 
 (* type conversions *)
-val extract : ?unsigned:bool -> bits:int -> t -> t
-val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
+val signed : int -> t -> t
+val unsigned : int -> t -> t
+val convert : Typ.t -> to_:Typ.t -> t -> t
 
 (* comparisons *)
 val eq : t -> t -> t
diff --git a/sledge/src/llair/term_test.ml b/sledge/src/llair/term_test.ml
index b2ed97866..6fde19254 100644
--- a/sledge/src/llair/term_test.ml
+++ b/sledge/src/llair/term_test.ml
@@ -30,51 +30,16 @@ let%test_module _ =
     let y = var y_
     let z = var z_
 
-    let%test "booleans distinct" = is_false (eq minus_one zero)
-    let%test "unsigned booleans distinct" = is_false (eq one zero)
-
-    let%test "boolean overflow" =
-      is_true
-        (Exp.eq
-           (Exp.integer Typ.bool Z.minus_one)
-           (Exp.convert ~dst:Typ.bool ~src:Typ.siz
-              (Exp.integer Typ.siz Z.one)))
-          .term
-
-    let%expect_test _ =
-      pp
-        (Exp.convert ~dst:Typ.byt ~unsigned:true ~src:Typ.int
-           (Exp.integer Typ.int (Z.of_int 255)))
-          .term ;
-      [%expect {| -1 |}]
-
-    let%expect_test _ =
-      pp
-        (Exp.convert ~dst:Typ.byt ~unsigned:false ~src:Typ.int
-           (Exp.integer Typ.int (Z.of_int 255)))
-          .term ;
-      [%expect {| -1 |}]
-
-    let%expect_test _ =
-      pp
-        (Exp.convert ~dst:Typ.int ~unsigned:true ~src:Typ.byt
-           (Exp.integer Typ.byt (Z.of_int (-1))))
-          .term ;
-      [%expect {| 255 |}]
-
-    let%expect_test _ =
-      pp
-        (Exp.convert ~dst:Typ.int ~unsigned:false ~src:Typ.byt
-           (Exp.integer Typ.byt (Z.of_int (-1))))
-          .term ;
-      [%expect {| -1 |}]
+    let%test "booleans distinct" = is_false (true_ = false_)
+    let%test "u1 values distinct" = is_false (one = zero)
+    let%test "boolean overflow" = is_true (minus_one = signed 1 one)
+    let%test _ = is_true (one = unsigned 1 minus_one)
 
     let%test "unsigned boolean overflow" =
       is_true
         (Exp.uge
            (Exp.integer Typ.bool Z.minus_one)
-           (Exp.convert ~dst:Typ.bool ~src:Typ.siz
-              (Exp.integer Typ.siz Z.one)))
+           (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool))
           .term
 
     let%expect_test _ =
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 1a9e9480d..7bfe28327 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -16,13 +16,11 @@ let%test_module _ =
     let pp = printf pp
     let pp_classes = printf pp_classes
     let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
-    let i8 = Typ.int
-    let i64 = Typ.siz
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
     let ( - ) = Term.sub
     let ( * ) = Term.mul
-    let f = Term.convert ~dst:i64 ~src:i8
+    let f = Term.unsigned 8
     let g = Term.rem
     let wrt = Var.Set.empty
     let t_, wrt = Var.fresh "t" ~wrt
@@ -99,9 +97,10 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          %x_5 = %y_6 = %z_7
+          %x_5 = %y_6 = %z_7 = ((u8) %x_5)
 
-          {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} |}]
+          {sat= true;
+           rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((u8) %x_5) ↦ %x_5]]} |}]
 
     let%test _ = entails_eq r2 x z
     let%test _ = entails_eq (or_ r1 r2) x y
@@ -326,10 +325,6 @@ let%test_module _ =
       pp r15 ; [%expect {|
           {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
-    let%test _ = entails_eq r15 b (Term.convert ~dst:Typ.bool ~src:i64 !1)
-
-    let%test _ =
-      entails_eq r15
-        (Term.convert ~dst:i64 ~unsigned:true ~src:Typ.bool b)
-        !1
+    let%test _ = entails_eq r15 b (Term.signed 1 !1)
+    let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
   end )