diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 332723172..cff530416 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -197,6 +197,8 @@ let exec_inst i q =
    |Alloc _ | Memset _ | Memcpy _ | Memmov _ | Free _ ->
       Some q
   | Abort _ -> None
+  | Intrinsic {reg= Some reg; _} -> Some (exec_kill reg q)
+  | Intrinsic {reg= None; _} -> Some q
 
 (** Treat any intrinsic function as havoc on the return register [aret] *)
 let exec_intrinsic ~skip_throw:_ aret i _ pre =
diff --git a/sledge/dune b/sledge/dune
index 709c3b5c1..5dcd7472d 100644
--- a/sledge/dune
+++ b/sledge/dune
@@ -29,8 +29,8 @@
 (library
  (name ppx_sledge)
  (kind ppx_rewriter)
- (libraries ppx_compare ppx_expect ppx_hash ppx_here ppx_inline_test ppx_let
-   ppx_sexp_conv ppx_sexp_value)
+ (libraries ppx_compare ppx_enumerate ppx_expect ppx_hash ppx_here
+   ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_variants_conv)
  (preprocess no_preprocessing))
 
 (subdir
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index c687772a4..864a56737 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -70,7 +70,13 @@ let exec_inst inst pre =
       Exec.alloc pre ~reg:(X.reg reg) ~num:(X.term num) ~len
   | Free {ptr; _} -> Exec.free pre ~ptr:(X.term ptr)
   | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:X.reg reg))
-  | Abort _ -> Exec.abort pre )
+  | Abort _ -> Exec.abort pre
+  | Intrinsic {reg; name; args; _} ->
+      let areturn = Option.map ~f:X.reg reg in
+      let intrinsic = Llair.Intrinsic.to_string name in
+      let actuals = IArray.map ~f:X.term args in
+      Exec.intrinsic ~skip_throw:true pre areturn intrinsic actuals
+      |> Option.get_lazy (fail "exec_inst: %a" Llair.Inst.pp inst) )
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw r i es q =
diff --git a/sledge/src/llair/intrinsics.ml b/sledge/src/llair/intrinsics.ml
new file mode 100644
index 000000000..1775a891f
--- /dev/null
+++ b/sledge/src/llair/intrinsics.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.
+ *)
+
+(** Intrinsic instruction opcodes *)
+
+type t = [`nop] [@@deriving compare, equal, hash, sexp, enumerate, variants]
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index f549a1506..56b360b04 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -17,6 +17,24 @@ module Function = Function
 module Global = Global
 module GlobalDefn = GlobalDefn
 
+module Intrinsic = struct
+  include Intrinsics
+  module Intrinsic_to_String = Bijection.Make (Intrinsics) (String)
+
+  let t_to_name =
+    Iter.of_list all
+    |> Iter.map ~f:(fun i -> (i, Variants.to_name i))
+    |> Intrinsic_to_String.of_iter
+
+  let to_string i = Intrinsic_to_String.find_left i t_to_name
+
+  let of_name s =
+    try Some (Intrinsic_to_String.find_right s t_to_name)
+    with Not_found -> None
+
+  let pp ppf i = Format.pp_print_string ppf (to_string i)
+end
+
 type inst =
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
   | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
@@ -28,6 +46,8 @@ type inst =
   | Free of {ptr: Exp.t; loc: Loc.t}
   | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t}
   | Abort of {loc: Loc.t}
+  | Intrinsic of
+      {reg: Reg.t option; name: Intrinsic.t; args: Exp.t iarray; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 type cmnd = inst iarray [@@deriving compare, equal, hash, sexp]
@@ -258,6 +278,10 @@ let pp_inst fs inst =
         (Option.pp "%a := " Reg.pp)
         reg msg Loc.pp loc
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
+  | Intrinsic {reg; name; args; loc} ->
+      pf "@[<2>%aintrinsic %a(%a);@]\t%a"
+        (Option.pp "%a := " Reg.pp)
+        reg Intrinsic.pp name (IArray.pp ",@ " Exp.pp) args Loc.pp loc
 
 let pp_actuals pp_actual fs actuals =
   Format.fprintf fs "@ (@[%a@])" (IArray.pp ",@ " pp_actual) actuals
@@ -352,6 +376,7 @@ module Inst = struct
   let free ~ptr ~loc = Free {ptr; loc}
   let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
   let abort ~loc = Abort {loc}
+  let intrinsic ~reg ~name ~args ~loc = Intrinsic {reg; name; args; loc}
 
   let loc = function
     | Move {loc; _}
@@ -363,18 +388,23 @@ module Inst = struct
      |Alloc {loc; _}
      |Free {loc; _}
      |Nondet {loc; _}
-     |Abort {loc; _} ->
+     |Abort {loc; _}
+     |Intrinsic {loc; _} ->
         loc
 
   let union_locals inst vs =
     match inst with
     | Move {reg_exps; _} ->
         IArray.fold ~f:(fun (reg, _) vs -> Reg.Set.add reg vs) reg_exps vs
-    | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
+    | Load {reg; _}
+     |Alloc {reg; _}
+     |Nondet {reg= Some reg; _}
+     |Intrinsic {reg= Some reg; _} ->
         Reg.Set.add reg vs
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
      |Nondet {reg= None; _}
-     |Abort _ ->
+     |Abort _
+     |Intrinsic {reg= None; _} ->
         vs
 
   let locals inst = union_locals inst Reg.Set.empty
@@ -392,6 +422,7 @@ module Inst = struct
     | Free {ptr; loc= _} -> f ptr s
     | Nondet {reg= _; msg= _; loc= _} -> s
     | Abort {loc= _} -> s
+    | Intrinsic {reg= _; name= _; args; loc= _} -> IArray.fold ~f args s
 end
 
 (** Jumps *)
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 7b54458b1..78886a877 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -16,6 +16,14 @@ module Function = Function
 module Global = Global
 module GlobalDefn = GlobalDefn
 
+module Intrinsic : sig
+  include module type of Intrinsics
+
+  val to_string : t -> string
+  val of_name : string -> t option
+  val pp : t pp
+end
+
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
@@ -42,6 +50,9 @@ type inst = private
       (** Bind [reg] to an arbitrary value, representing non-deterministic
           approximation of behavior described by [msg]. *)
   | Abort of {loc: Loc.t}  (** Trigger abnormal program termination *)
+  | Intrinsic of
+      {reg: Reg.t option; name: Intrinsic.t; args: Exp.t iarray; loc: Loc.t}
+      (** Bind [reg] to the value of applying intrinsic [name] to [args]. *)
 
 (** A (straight-line) command is a sequence of instructions. *)
 type cmnd = inst iarray
@@ -122,6 +133,14 @@ module Inst : sig
   val free : ptr:Exp.t -> loc:Loc.t -> inst
   val nondet : reg:Reg.t option -> msg:string -> loc:Loc.t -> inst
   val abort : loc:Loc.t -> inst
+
+  val intrinsic :
+       reg:Reg.t option
+    -> name:Intrinsic.t
+    -> args:Exp.t iarray
+    -> loc:Loc.t
+    -> t
+
   val loc : inst -> Loc.t
   val locals : inst -> Reg.Set.t
   val fold_exps : inst -> 's -> f:(Exp.t -> 's -> 's) -> 's