diff --git a/lib/pulse/lib/Pulse.Lib.Dv.fst b/lib/pulse/lib/Pulse.Lib.Dv.fst
index 3f41dae39..429491408 100644
--- a/lib/pulse/lib/Pulse.Lib.Dv.fst
+++ b/lib/pulse/lib/Pulse.Lib.Dv.fst
@@ -18,4 +18,4 @@ module Pulse.Lib.Dv
 
 let while_ cond body = ()
 let par f1 f2 = ()
-let rec unreachable t = unreachable t
+let rec unreachable t () = unreachable t ()
diff --git a/lib/pulse/lib/Pulse.Lib.Dv.fsti b/lib/pulse/lib/Pulse.Lib.Dv.fsti
index 763b44a0f..d47db8e2a 100644
--- a/lib/pulse/lib/Pulse.Lib.Dv.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Dv.fsti
@@ -18,4 +18,4 @@ module Pulse.Lib.Dv
 
 val while_ (cond: unit -> Dv bool) (body: unit -> Dv unit) : Dv unit
 val par (f1: unit -> Dv unit) (f2: unit -> Dv unit) : Dv unit
-val unreachable (t: Type0) : Dv t
+val unreachable (t: Type0) : unit -> Dv t
diff --git a/src/checker/Pulse.Extract.Main.fst b/src/checker/Pulse.Extract.Main.fst
index 6f2a60a70..73ed103df 100644
--- a/src/checker/Pulse.Extract.Main.fst
+++ b/src/checker/Pulse.Extract.Main.fst
@@ -462,7 +462,7 @@ let rec extract_dv g (p:st_term) : T.Tac ECL.term =
 
     | Tm_Unreachable { c } ->
       ECL.mk_meta_monadic (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv ["Pulse"; "Lib"; "Dv"; "unreachable"])))
-        [comp_res c, R.Q_Explicit])
+        [comp_res c, R.Q_Explicit; unit_tm, R.Q_Explicit])
 
     | Tm_WithInv { body } -> extract_dv g body
 
diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst
index 64a944ce9..ee6d2a08b 100644
--- a/src/extraction/ExtractPulse.fst
+++ b/src/extraction/ExtractPulse.fst
@@ -123,7 +123,7 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
     when (string_of_mlpath p = "Pulse.Lib.Dv.while_") ->
     EWhile(cb test, cb body)
 
-  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _ ])
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _ ])
     when (string_of_mlpath p = "Pulse.Lib.Dv.unreachable") ->
     EAbortS (string_of_mlpath p)
 
diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml
index 46c9ff2eb..de2e5089b 100644
--- a/src/ocaml/plugin/generated/ExtractPulse.ml
+++ b/src/ocaml/plugin/generated/ExtractPulse.ml
@@ -442,12 +442,12 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) =
                  uu___3);
               FStar_Extraction_ML_Syntax.mlty = uu___4;
               FStar_Extraction_ML_Syntax.loc = uu___5;_},
-            uu___6::[])
+            uu___6::uu___7::[])
            when
-           let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-           uu___7 = "Pulse.Lib.Dv.unreachable" ->
-           let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-           FStar_Extraction_Krml.EAbortS uu___7
+           let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           uu___8 = "Pulse.Lib.Dv.unreachable" ->
+           let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           FStar_Extraction_Krml.EAbortS uu___8
        | FStar_Extraction_ML_Syntax.MLE_App
            ({
               FStar_Extraction_ML_Syntax.expr =
@@ -483,7 +483,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) =
        | uu___1 ->
            FStar_Compiler_Effect.raise
              FStar_Extraction_Krml.NotSupportedByKrmlExtension)
-let (uu___277 : unit) =
+let (uu___278 : unit) =
   FStar_Extraction_Krml.register_pre_translate_type_without_decay
     pulse_translate_type_without_decay;
   FStar_Extraction_Krml.register_pre_translate_expr pulse_translate_expr
\ No newline at end of file
diff --git a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml
index 53c2ccffb..d38f4a738 100644
--- a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml
+++ b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml
@@ -4415,7 +4415,9 @@ let rec (extract_dv :
                                                 "Dv";
                                                 "unreachable"])))
                                        [((Pulse_Syntax_Base.comp_res c),
-                                          FStar_Reflection_V2_Data.Q_Explicit)])))
+                                          FStar_Reflection_V2_Data.Q_Explicit);
+                                       (Pulse_Reflection_Util.unit_tm,
+                                         FStar_Reflection_V2_Data.Q_Explicit)])))
                       | Pulse_Syntax_Base.Tm_WithInv
                           { Pulse_Syntax_Base.name1 = uu___3;
                             Pulse_Syntax_Base.body6 = body;