diff --git a/src/math/polysat/polysat_params.pyg b/src/math/polysat/polysat_params.pyg
index a39add57b..fffb2bf71 100644
--- a/src/math/polysat/polysat_params.pyg
+++ b/src/math/polysat/polysat_params.pyg
@@ -4,6 +4,7 @@ def_module_params('polysat',
     params=(
         ('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts before giving up"),
         ('max_decisions', UINT, UINT_MAX, "maximum number of decisions before giving up"),
+        ('max_iterations', UINT, UINT_MAX, "maximum number of iterations before giving up"),
         # ('log', UINT, UINT_MAX, "polysat logging filter (TODO)"),
         ('log_start', UINT, UINT_MAX, "Enable logging on solver iteration N"),
         ('log_conflicts', BOOL, False, "log conflicts"),
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 3c0219c27..2e915dfe9 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -80,6 +80,7 @@ namespace polysat {
         m_params.append(p);
         m_config.m_max_conflicts = pp.max_conflicts();
         m_config.m_max_decisions = pp.max_decisions();
+        m_config.m_max_iterations = pp.max_iterations();
         m_config.m_log_start = pp.log_start();
         m_config.m_log_conflicts = pp.log_conflicts();
         m_config.m_slicing_congruence = pp.slicing_congruence();
@@ -96,7 +97,8 @@ namespace polysat {
         return
             m_lim.inc() &&
             (m_stats.m_num_conflicts < config().m_max_conflicts) &&
-            (m_stats.m_num_decisions < config().m_max_decisions);
+            (m_stats.m_num_decisions < config().m_max_decisions) &&
+            (m_stats.m_num_iterations < config().m_max_iterations);
     }
 
     lbool solver::check_sat() {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 67577a163..e9215a391 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -51,6 +51,7 @@ namespace polysat {
     struct config_t {
         uint64_t    m_max_conflicts = std::numeric_limits<uint64_t>::max();
         uint64_t    m_max_decisions = std::numeric_limits<uint64_t>::max();
+        uint64_t    m_max_iterations = std::numeric_limits<uint64_t>::max();
         unsigned    m_log_start     = UINT_MAX;
         bool        m_log_conflicts = false;
         bool        m_slicing_congruence = false;