diff --git a/src/math/polysat/polysat_params.pyg b/src/math/polysat/polysat_params.pyg
index 9d60e3682..a26a1a3a7 100644
--- a/src/math/polysat/polysat_params.pyg
+++ b/src/math/polysat/polysat_params.pyg
@@ -4,7 +4,8 @@ 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"),
-        ('log', UINT, UINT_MAX, "polysat logging filter (enable logging in iteration N)"),
+        # ('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"),
         ('slicing.congruence', BOOL, False, "bitvector slicing: add virtual congruence terms"),
     )
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index f91565f86..80e86747c 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -80,12 +80,12 @@ 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_log_iteration = pp.log();
+        m_config.m_log_start = pp.log_start();
         m_config.m_log_conflicts = pp.log_conflicts();
         m_config.m_slicing_congruence = pp.slicing_congruence();
 
         // TODO: log filter to enable/disable based on submodules
-        if (m_config.m_log_iteration == 0)
+        if (m_config.m_log_start == 0)
             set_log_enabled(true);
         else
             set_log_enabled(false);
@@ -106,7 +106,7 @@ namespace polysat {
         LOG("Starting");
         while (should_search()) {
             m_stats.m_num_iterations++;
-            if (m_stats.m_num_iterations == config().m_log_iteration)
+            if (m_stats.m_num_iterations == config().m_log_start)
                 set_log_enabled(true);
             LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
             LOG("Free variables: " << m_free_pvars);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index f90c81ad5..d1a8daa6e 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -46,7 +46,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();
-        unsigned    m_log_iteration = UINT_MAX;
+        unsigned    m_log_start     = UINT_MAX;
         bool        m_log_conflicts = false;
         bool        m_slicing_congruence = false;
     };