diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index c65da431e..6dada445b 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -554,6 +554,7 @@ namespace polysat {
         m_justification[v] = justification::unassigned();
         if (!is_valid) {
             LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
+            ++m_stats.m_num_viable_fallback;
             // Try to find a valid replacement value
             switch (m_viable_fallback.find_viable(v, val)) {
             case dd::find_t::singleton:
@@ -1194,12 +1195,13 @@ namespace polysat {
     }
 
     void solver::collect_statistics(statistics& st) const {
-        st.update("polysat iterations",   m_stats.m_num_iterations);
-        st.update("polysat decisions",    m_stats.m_num_decisions);
-        st.update("polysat conflicts",    m_stats.m_num_conflicts);
-        st.update("polysat bailouts",     m_stats.m_num_bailouts);
-        st.update("polysat propagations", m_stats.m_num_propagations);
-        st.update("polysat restarts",     m_stats.m_num_restarts);
+        st.update("polysat iterations",      m_stats.m_num_iterations);
+        st.update("polysat decisions",       m_stats.m_num_decisions);
+        st.update("polysat conflicts",       m_stats.m_num_conflicts);
+        st.update("polysat bailouts",        m_stats.m_num_bailouts);
+        st.update("polysat propagations",    m_stats.m_num_propagations);
+        st.update("polysat restarts",        m_stats.m_num_restarts);
+        st.update("polysat viable fallback", m_stats.m_num_viable_fallback);
     }
 
     bool solver::invariant() {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index da3921f1d..2b4c7bd18 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -54,6 +54,7 @@ namespace polysat {
             unsigned m_num_conflicts;
             unsigned m_num_bailouts;
             unsigned m_num_restarts;
+            unsigned m_num_viable_fallback;  ///< how often did we query the univariate solver
             void reset() { memset(this, 0, sizeof(*this)); }
             stats() { reset(); }
         };