diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index b5d2ee7719..9483faecff 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1435,7 +1435,11 @@ namespace smt {
                     }
                 }
                 
+                unsigned max_count = 20;
                 for (auto t : tn.enum_terms(srt)) {
+                    if (max_count == 0)
+                        break;
+                    --max_count;
                     unsigned generation = 0; // todo - inherited from sub-term of t?
                     TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m)
                                                    << " to instantiation set of S" << std::endl;);