diff --git a/sledge/.gitignore b/sledge/.gitignore
index f5a70988c..4c28634b3 100644
--- a/sledge/.gitignore
+++ b/sledge/.gitignore
@@ -2,6 +2,7 @@
 /bin/
 /llvm/
 /model/cxxabi.bc
+/model/dune
 /src/dune
 /src/import/dune
 /src/llair/dune
diff --git a/sledge/Makefile b/sledge/Makefile
index 6018ef8e9..8728bfd96 100644
--- a/sledge/Makefile
+++ b/sledge/Makefile
@@ -19,7 +19,7 @@ facebook/Makefile:
 DBG_TARGETS = $(patsubst %,_build/dev/%.exe,$(EXES)) $(patsubst %,_build/dev/%.install,$(INSTALLS))
 OPT_TARGETS = $(patsubst %,_build/release/%.exe,$(EXES)) $(patsubst %,_build/release/%.install,$(INSTALLS))
 
-DUNEINS = $(shell find src facebook -name dune.in)
+DUNEINS = $(shell find src facebook model -name dune.in)
 DUNES = $(patsubst %.in,%,$(DUNEINS))
 
 .PHONY: dunes
diff --git a/sledge/model/Makefile b/sledge/model/Makefile
index dfb68652c..cf8acba1d 100644
--- a/sledge/model/Makefile
+++ b/sledge/model/Makefile
@@ -9,9 +9,10 @@ CLANG_ARGS?=-g $(OPT_ARGS)
 
 # select llvm and clang
 SWITCH?=$(shell opam switch show)
-LLVM?=../llvm/_install/$(SWITCH)
+ROOT?=..
+LLVM=$(ROOT)/llvm/_install/$(SWITCH)
 
-LIBCXXABI=../llvm/projects/libcxxabi
+LIBCXXABI=$(ROOT)/llvm/projects/libcxxabi
 
 cxxabi.bc : cxxabi.cpp
 	$(LLVM)/bin/clang $(CLANG_ARGS) -I$(LLVM)/include/c++/v1 -I$(LIBCXXABI)/include -I$(LIBCXXABI)/src -c -emit-llvm cxxabi.cpp
diff --git a/sledge/model/dune.in b/sledge/model/dune.in
new file mode 100644
index 000000000..91dc32409
--- /dev/null
+++ b/sledge/model/dune.in
@@ -0,0 +1,32 @@
+(* -*- tuareg -*- *)
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+let deps = []
+
+;;
+Jbuild_plugin.V1.send
+@@ Format.sprintf
+     {|
+(rule
+ (targets cxxabi.bc)
+ (deps cxxabi.cpp Makefile llair_intrinsics.h)
+ (action (run make ROOT=../../.. cxxabi.bc)))
+
+(rule
+ (targets model.ml)
+ (deps cxxabi.bc)
+ (action (run ocaml-crunch -m plain -e bc -o model.ml .)))
+
+(library
+ (name model)
+ (public_name llair.model)
+ %s
+ (libraries %s))
+|}
+     (flags `lib deps)
+     (libraries deps)
diff --git a/sledge/sledge.opam b/sledge/sledge.opam
index 246d7279e..c80ff428c 100644
--- a/sledge/sledge.opam
+++ b/sledge/sledge.opam
@@ -14,6 +14,7 @@ depends: [
   "base" {>= "v0.12.0"}
   "cmdliner"
   "core_kernel"
+  "crunch" {build}
   "ctypes"
   "ctypes-foreign"
   "dune" {build}
diff --git a/sledge/src/llair/dune.in b/sledge/src/llair/dune.in
index 9597a3cef..9b1ec3f8f 100644
--- a/sledge/src/llair/dune.in
+++ b/sledge/src/llair/dune.in
@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"; "trace"]
+let deps = ["model"; "import"; "trace"]
 
 ;;
 Jbuild_plugin.V1.send
@@ -16,7 +16,7 @@ Jbuild_plugin.V1.send
  (name llair_)
  (public_name llair)
  %s
- (libraries ctypes ctypes.foreign llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo %s))
+ (libraries ctypes ctypes.foreign llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo llvm.linker %s))
 |}
      (flags `lib deps)
      (libraries deps)
diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index ddc1a29e8..59234fce7 100644
--- a/sledge/src/llair/frontend.ml
+++ b/sledge/src/llair/frontend.ml
@@ -1350,11 +1350,19 @@ let translate : string -> Llair.t =
   ;
   Llvm.install_fatal_error_handler invalid_llvm ;
   let llcontext = Llvm.global_context () in
+  let model_module =
+    let model_memorybuffer =
+      Llvm.MemoryBuffer.of_string
+        (Option.value_exn (Model.read "/cxxabi.bc"))
+    in
+    Llvm_irreader.parse_ir llcontext model_memorybuffer
+  in
   let llmodule =
     let llmemorybuffer = Llvm.MemoryBuffer.of_file file in
     try Llvm_irreader.parse_ir llcontext llmemorybuffer
     with Llvm_irreader.Error msg -> invalid_llvm msg
   in
+  Llvm_linker.link_modules' llmodule model_module ;
   Llvm_analysis.verify_module llmodule |> Option.iter ~f:invalid_llvm ;
   transform llmodule ;
   scan_locs llmodule ;