diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index d920af30a..789d1b819 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -83,7 +83,6 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
     let summary_table =
       Used_globals_executor.compute_summaries
         { bound= 1
-        ; skip_throw= false
         ; function_summaries= true
         ; entry_points
         ; globals= Declared Llair.Global.Set.empty }
@@ -101,9 +100,6 @@ let analyze =
     flag "bound"
       (optional_with_default 1 int)
       ~doc:"<int> stop execution exploration at depth <int>"
-  and exceptions =
-    flag "exceptions" no_arg
-      ~doc:"explore executions that throw and handle exceptions"
   and function_summaries =
     flag "function-summaries" no_arg
       ~doc:"use function summaries (in development)"
@@ -131,10 +127,9 @@ let analyze =
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
-    let skip_throw = not exceptions in
     Domain_sh.simplify_states := not no_simplify_states ;
     Timer.enabled := stats ;
-    exec {bound; skip_throw; function_summaries; entry_points; globals} pgm ;
+    exec {bound; function_summaries; entry_points; globals} pgm ;
     Report.coverage pgm ;
     Report.safe_or_unsafe ()
 
diff --git a/sledge/model/cxxabi.cpp b/sledge/model/cxxabi.cpp
index e094848df..819e490a9 100644
--- a/sledge/model/cxxabi.cpp
+++ b/sledge/model/cxxabi.cpp
@@ -6,19 +6,34 @@
  */
 
 #include "cxa_default_handlers.cpp"
-#include "cxa_exception.cpp"
 #include "cxa_exception_storage.cpp"
 #include "cxa_guard.cpp"
 #include "cxa_handlers.cpp"
 #include "llair_intrinsics.h"
+#ifdef EXCEPTIONS
+#include "cxa_exception.cpp"
+#endif
 
 extern "C" {
 
 void abort_message(const char* format, ...) { abort(); }
 
+#ifndef EXCEPTIONS
+
+__attribute__((noreturn)) void __llair_throw(void* thrown_exception) {
+  __llair_unreachable();
+}
+
+void* __cxa_allocate_exception(size_t thrown_size) throw() {
+  __llair_unreachable();
+}
+
+#else
+
 __attribute__((always_inline)) _Unwind_Reason_Code
 _Unwind_RaiseException(_Unwind_Exception* unwind_exception) {
   __llair_throw(thrown_object_from_cxa_exception(
       abi::cxa_exception_from_exception_unwind_exception(unwind_exception)));
 }
+#endif
 }
diff --git a/sledge/model/llair_intrinsics.h b/sledge/model/llair_intrinsics.h
index 81ca43882..3f74125a9 100644
--- a/sledge/model/llair_intrinsics.h
+++ b/sledge/model/llair_intrinsics.h
@@ -11,17 +11,18 @@
 extern "C" {
 #endif
 
-__attribute__((noreturn)) void __llair_throw(void* thrown_exception);
-
-/* express assumption that an execution is not possible */
-__attribute__((noreturn)) void __llair_unreachable();
-
-/* allocation that cannot fail. */
+/* allocation that cannot fail */
 void* __llair_alloc(unsigned size);
 
 /* non-deterministic choice */
 int __llair_choice();
 
+/* throw an exception */
+__attribute__((noreturn)) void __llair_throw(void* thrown_exception);
+
+/* executions that call __llair_unreachable are assumed to be impossible */
+__attribute__((noreturn)) void __llair_unreachable();
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt
index 4c09423c2..860d1685a 100644
--- a/sledge/sledge-help.txt
+++ b/sledge/sledge-help.txt
@@ -53,7 +53,6 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
                          or "unit" (unit domain)
-  [-exceptions]          explore executions that throw and handle exceptions
   [-function-summaries]  use function summaries (in development)
   [-fuzzer]              add a harness for libFuzzer targets
   [-margin <cols>]       wrap debug tracing at <cols> columns
@@ -151,7 +150,6 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
                          or "unit" (unit domain)
-  [-exceptions]          explore executions that throw and handle exceptions
   [-function-summaries]  use function summaries (in development)
   [-fuzzer]              add a harness for libFuzzer targets
   [-margin <cols>]       wrap debug tracing at <cols> columns
@@ -238,7 +236,6 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
                          or "unit" (unit domain)
-  [-exceptions]          explore executions that throw and handle exceptions
   [-function-summaries]  use function summaries (in development)
   [-margin <cols>]       wrap debug tracing at <cols> columns
   [-no-simplify-states]  do not simplify states during symbolic execution
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 802150538..6f9b98665 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -11,7 +11,6 @@
 
 type exec_opts =
   { bound: int
-  ; skip_throw: bool
   ; function_summaries: bool
   ; entry_points: string list
   ; globals: Domain_used_globals.r }
@@ -446,9 +445,7 @@ module Make (Dom : Domain_intf.Dom) = struct
                   (Domain_used_globals.by_function opts.globals callee.name)
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
-    | Throw {exc} ->
-        if opts.skip_throw then Work.skip
-        else exec_throw stk state block exc
+    | Throw {exc} -> exec_throw stk state block exc
     | Unreachable -> Work.skip
 
   let exec_inst : Llair.inst -> Dom.t -> (Dom.t, Dom.t * Llair.inst) result
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index d97d08aef..cf8619fd1 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -9,7 +9,6 @@
 
 type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
-  ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
   ; entry_points: string list  (** C linkage names of entry points *)
   ; globals: Domain_used_globals.r }
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 7176a37f8..4a59975a2 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -68,7 +68,7 @@ let exec_inst inst pre =
   | Intrinsic {reg; name; args; _} ->
       let areturn = Option.map ~f:X.reg reg in
       let actuals = IArray.map ~f:X.term args in
-      Exec.intrinsic ~skip_throw:true pre areturn name actuals )
+      Exec.intrinsic pre areturn name actuals )
   |> Option.map ~f:simplify
 
 let value_determined_by ctx us a =
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 57f98fbf3..2811e7165 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -734,7 +734,7 @@ let free pre ~ptr = exec_spec pre (free_spec ptr)
 let nondet pre = function Some reg -> kill pre reg | None -> pre
 let abort _ = None
 
-let intrinsic ~skip_throw :
+let intrinsic :
        Sh.t
     -> Var.t option
     -> Llair.Intrinsic.t
@@ -809,11 +809,6 @@ let intrinsic ~skip_throw :
    *)
   (* size_t strlen (const char* ptr) *)
   | Some reg, `strlen, [|ptr|] -> exec_spec pre (strlen_spec reg ptr)
-  (*
-   * cxxabi
-   *)
-  | Some _, `__cxa_allocate_exception, [|_|] when skip_throw ->
-      Some (Sh.false_ pre.us)
   (*
    * folly
    *)
@@ -827,7 +822,7 @@ let intrinsic ~skip_throw :
       | `posix_memalign | `realloc | `mallocx | `rallocx | `xallocx
       | `sallocx | `dallocx | `sdallocx | `nallocx | `malloc_usable_size
       | `mallctl | `mallctlnametomib | `mallctlbymib | `strlen
-      | `__cxa_allocate_exception | `_ZN5folly13usingJEMallocEv )
+      | `_ZN5folly13usingJEMallocEv )
     , _ ) ->
       fail "%aintrinsic %a%a;"
         (Option.pp "%a := " Var.pp)
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index 90d2935bd..3f9235d08 100644
--- a/sledge/src/exec.mli
+++ b/sledge/src/exec.mli
@@ -20,9 +20,4 @@ val nondet : Sh.t -> Var.t option -> Sh.t
 val abort : Sh.t -> Sh.t option
 
 val intrinsic :
-     skip_throw:bool
-  -> Sh.t
-  -> Var.t option
-  -> Llair.Intrinsic.t
-  -> Term.t iarray
-  -> Sh.t option
+  Sh.t -> Var.t option -> Llair.Intrinsic.t -> Term.t iarray -> Sh.t option
diff --git a/sledge/src/llair/intrinsics.ml b/sledge/src/llair/intrinsics.ml
index 15aaf257b..4eef1da58 100644
--- a/sledge/src/llair/intrinsics.ml
+++ b/sledge/src/llair/intrinsics.ml
@@ -33,8 +33,6 @@ type t =
   | `malloc_stats_print
   | (* cstring *)
     `strlen
-  | (* cxxabi *)
-    `__cxa_allocate_exception
   | (* folly *)
     `_ZN5folly13usingJEMallocEv ]
 [@@deriving compare, equal, hash, sexp, enumerate, variants]
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index a1f252777..168d28a4d 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -572,9 +572,14 @@ module BlockQ = HashQueue.Make (Block_label)
 module Func = struct
   type t = func [@@deriving compare, equal, hash, sexp_of]
 
-  let is_undefined = function
-    | {entry= {cmnd; term= Unreachable; _}; _} -> IArray.is_empty cmnd
-    | _ -> false
+  let undefined_entry =
+    Block.mk ~lbl:"undefined" ~cmnd:IArray.empty ~term:Term.unreachable
+
+  let mk_undefined ~name ~formals ~freturn ~fthrow ~loc =
+    let locals = Reg.Set.empty in
+    {name; formals; freturn; fthrow; locals; entry= undefined_entry; loc}
+
+  let is_undefined func = func.entry == undefined_entry
 
   let fold_cfg func s ~f =
     let seen = BlockS.create 0 in
@@ -672,13 +677,6 @@ module Func = struct
     resolve_parent_and_jumps entry ;
     IArray.iter cfg ~f:resolve_parent_and_jumps ;
     func |> check invariant
-
-  let mk_undefined ~name ~formals ~freturn ~fthrow =
-    let entry =
-      Block.mk ~lbl:"" ~cmnd:IArray.empty ~term:Term.unreachable
-    in
-    let cfg = IArray.empty in
-    mk ~name ~entry ~formals ~freturn ~fthrow ~cfg
 end
 
 (** Derived meta-data *)