diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 107c9f4bb..a988b1ba4 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -2163,9 +2163,6 @@ namespace smt {
                 }
 
                 SASSERT(is_quantifier(atom));
-                // Nested quantifiers as atoms are not expected but can occur
-                // in unsimplified formulas. Skip gracefully.
-                return;
             }
 
             void process_literal(expr* atom, polarity pol) {