diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp
index 97818ce8261..ba0155e975e 100644
--- a/src/ast/rewriter/datatype_rewriter.cpp
+++ b/src/ast/rewriter/datatype_rewriter.cpp
@@ -32,6 +32,10 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
         // simplify is_cons(nil) -> false
         //
         SASSERT(num_args == 1);
+        if (m_util.get_datatype_num_constructors(args[0]->get_sort()) == 1) {
+            result = m().mk_true();
+            return BR_DONE;
+        }
         if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
             return BR_FAILED;
         if (to_app(args[0])->get_decl() == m_util.get_recognizer_constructor(f))