diff --git a/TODO.md b/TODO.md
index 0eb7a05..73b4af7 100644
--- a/TODO.md
+++ b/TODO.md
@@ -6,5 +6,3 @@ Place for TODOs/FIXMEs, especially if not expressed in other places. See README.
 * FIXME: `separate_subst` has a default argument `keep_uni=false`. Rethink for each use case if it is the correct argument.
 * TODO: more parsimonious use of parentheses in printing expressions and types.
 * TODO: 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. In update mode, if typechecking fails, retry without type annotation. In verify mode, check that the resulting type matches the interface type from `.gadti` -- is not less general. In update mode, regenerate the `.gadti` file.
-* FIXME: when checking discarded in term abduction, in iteration 0 (only?), check modulo renaming of alien sort variables.
-* FIXME: missing "assert false" branches in exported code?
diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf
index e2b309b..de035df 100644
Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ
diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm
index 48c50a1..435f944 100644
--- a/doc/invargent-manual.tm
+++ b/doc/invargent-manual.tm
@@ -732,6 +732,16 @@
     with the nodes cannot be eliminated from the constraint during initial
     simplification.
 
+    <item*|<verbatim|-keep_assert_false>>Keep <verbatim|assert false> clauses
+    in exported code. When faced with multiple maximally general types of a
+    function, we sometimes want to prevent some interpretations by asserting
+    that a combination of arguments is not possible. These arguments will not
+    be compatible with the type inferred, causing exported code to fail to
+    typecheck. Sometimes we indicate unreachable cases just for
+    documentation. If the type is tight this will cause exported code to fail
+    to typecheck too. This option keeps pattern matching branches with
+    <verbatim|assert false> in their bodies in exported code nevertheless.
+
     <item*|<verbatim|-term_abduction_timeout>>Limit on term simple abduction
     steps (default 700). Simple abduction works with a single implication
     branch, which roughly corresponds to a single branch -- an execution path
diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml
index c42a53e..d07abef 100644
--- a/src/InvarGenT.ml
+++ b/src/InvarGenT.ml
@@ -84,6 +84,8 @@ let main () =
     "The exported type for which `Num` is an alias (default `int`); apply `S.of_int` to numerals.";
     "-full_annot", Arg.Set full_annot,
     "Annotate the `function` and `let..in` nodes in generated OCaml code";
+    "-keep_assert_false", Arg.Clear OCaml.drop_assert_false,
+    "Keep `assert false` clauses in exported code";
     "-term_abduction_timeout", Arg.Set_int Abduction.timeout_count,
     "Limit on term simple abduction steps (default 700)";
     "-term_abduction_fail", Arg.Set_int Abduction.fail_timeout_count,
diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml
index 241677f..1d3ef24 100644
--- a/src/InvarGenTTest.ml
+++ b/src/InvarGenTTest.ml
@@ -145,15 +145,15 @@ let tests = "InvarGenT" >::: [
       "non_pointwise_avl_small_rec" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~richer_answers:true "non_pointwise_avl_small_rec" ());
+           test_case "non_pointwise_avl_small_rec" ());
       "non_pointwise_avl_small" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~richer_answers:true "non_pointwise_avl_small" ());
+           test_case "non_pointwise_avl_small" ());
       "non_pointwise_avl" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~richer_answers:true "non_pointwise_avl" ());
+           test_case "non_pointwise_avl" ());
       "non_pointwise_vary" >::
         (fun () ->
            todo "harder test";
diff --git a/src/OCaml.ml b/src/OCaml.ml
index db5d9eb..cb71877 100644
--- a/src/OCaml.ml
+++ b/src/OCaml.ml
@@ -8,6 +8,7 @@
 
 let num_is = ref "int"
 let num_is_mod = ref false
+let drop_assert_false = ref true
 
 open Terms
 open Format
@@ -120,9 +121,12 @@ let postprocess elim_extypes e =
     | App (e1, e2, loc) ->
       App (aux e1, aux e2, loc)
     | Lam (ann, cls, loc) ->
-      let cls = List.filter (not % single_assert_false) cls in
+      let cls =
+        if !drop_assert_false
+        then List.filter (not % single_assert_false) cls
+        else cls in
       Lam (ann, List.map (fun (p,e)->p, aux e) cls, loc)
-    | AssertFalse _ -> assert false
+    | AssertFalse _ as e -> e
     | (AssertLeq _ | AssertEqty _) as e -> e
     | Letrec (docu, ann, x, e1, e2, loc) ->
       Letrec (docu, ann, x, aux e1, aux e2, loc)
diff --git a/src/OCaml.mli b/src/OCaml.mli
index a7920e3..02f6cc8 100644
--- a/src/OCaml.mli
+++ b/src/OCaml.mli
@@ -10,6 +10,9 @@
 val num_is : string ref
 (** See the [-num_is_mod] option. *)
 val num_is_mod : bool ref
+(** Drop [assert false] clauses from exported code, see the
+    [-drop_assert_false] option. *)
+val drop_assert_false : bool ref
 
 val pr_ml :
   funtys:bool -> lettys:bool ->