diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index f5d9d6100..12e3c09ea 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -2198,8 +2198,6 @@ namespace smt {
                     }
                     else {
                         SASSERT(is_quantifier(curr));
-                        SASSERT(is_lambda(curr));
-                        //UNREACHABLE(); // can't happen, the quantifier is supposed to be flat.
                     }
                 }
             }