diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index ac4d9369b..1837f28f9 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -149,6 +149,18 @@ struct statistics {
     unsigned m_nla_throttled_horner_lemmas = 0;
     unsigned m_nla_throttled_factor_zero_lemmas = 0;
     unsigned m_nla_throttled_factor_neutral_lemmas = 0;
+    unsigned m_nla_permanently_banned_lemmas = 0;
+    unsigned m_nla_permanently_banned_order_lemmas = 0;
+    unsigned m_nla_permanently_banned_binomial_sign_lemmas = 0;
+    unsigned m_nla_permanently_banned_monotone_lemmas = 0;
+    unsigned m_nla_permanently_banned_tangent_lemmas = 0;
+    unsigned m_nla_permanently_banned_basic_sign_lemmas = 0;
+    unsigned m_nla_permanently_banned_powers_lemmas = 0;
+    unsigned m_nla_permanently_banned_division_lemmas = 0;
+    unsigned m_nla_permanently_banned_grobner_lemmas = 0;
+    unsigned m_nla_permanently_banned_horner_lemmas = 0;
+    unsigned m_nla_permanently_banned_factor_zero_lemmas = 0;
+    unsigned m_nla_permanently_banned_factor_neutral_lemmas = 0;
     ::statistics m_st = {};
 
     void reset() {
@@ -173,6 +185,18 @@ struct statistics {
         st.update("arith-nla-throttled-horner-lemmas", m_nla_throttled_horner_lemmas);
         st.update("arith-nla-throttled-factor-zero-lemmas", m_nla_throttled_factor_zero_lemmas);
         st.update("arith-nla-throttled-factor-neutral-lemmas", m_nla_throttled_factor_neutral_lemmas);
+        st.update("arith-nla-permanently-banned-lemmas", m_nla_permanently_banned_lemmas);
+        st.update("arith-nla-permanently-banned-order-lemmas", m_nla_permanently_banned_order_lemmas);
+        st.update("arith-nla-permanently-banned-binomial-sign-lemmas", m_nla_permanently_banned_binomial_sign_lemmas);
+        st.update("arith-nla-permanently-banned-monotone-lemmas", m_nla_permanently_banned_monotone_lemmas);
+        st.update("arith-nla-permanently-banned-tangent-lemmas", m_nla_permanently_banned_tangent_lemmas);
+        st.update("arith-nla-permanently-banned-basic-sign-lemmas", m_nla_permanently_banned_basic_sign_lemmas);
+        st.update("arith-nla-permanently-banned-powers-lemmas", m_nla_permanently_banned_powers_lemmas);
+        st.update("arith-nla-permanently-banned-division-lemmas", m_nla_permanently_banned_division_lemmas);
+        st.update("arith-nla-permanently-banned-grobner-lemmas", m_nla_permanently_banned_grobner_lemmas);
+        st.update("arith-nla-permanently-banned-horner-lemmas", m_nla_permanently_banned_horner_lemmas);
+        st.update("arith-nla-permanently-banned-factor-zero-lemmas", m_nla_permanently_banned_factor_zero_lemmas);
+        st.update("arith-nla-permanently-banned-factor-neutral-lemmas", m_nla_permanently_banned_factor_neutral_lemmas);
         st.update("arith-gcd-conflict", m_gcd_conflicts);
         st.update("arith-cube-calls", m_cube_calls);
         st.update("arith-cube-success", m_cube_success);
diff --git a/src/math/lp/nla_throttle.cpp b/src/math/lp/nla_throttle.cpp
index 404ede6f4..6d3fbe809 100644
--- a/src/math/lp/nla_throttle.cpp
+++ b/src/math/lp/nla_throttle.cpp
@@ -197,6 +197,47 @@ bool nla_throttle::insert_new_impl(const signature& sig) {
         // Check if this lemma should be permanently banned
         if (should_permanently_ban(sig, k)) {
             m_permanently_forbidden.insert(sig);
+            m_stats.m_nla_permanently_banned_lemmas++;
+            
+            // Update specific lemma type permanent ban statistics
+            switch (k) {
+                case ORDER_LEMMA:
+                    m_stats.m_nla_permanently_banned_order_lemmas++;
+                    break;
+                case BINOMIAL_SIGN_LEMMA:
+                    m_stats.m_nla_permanently_banned_binomial_sign_lemmas++;
+                    break;
+                case MONOTONE_LEMMA:
+                    m_stats.m_nla_permanently_banned_monotone_lemmas++;
+                    break;
+                case TANGENT_LEMMA:
+                    m_stats.m_nla_permanently_banned_tangent_lemmas++;
+                    break;
+                case BASIC_SIGN_LEMMA:
+                    m_stats.m_nla_permanently_banned_basic_sign_lemmas++;
+                    break;
+                case POWERS_LEMMA:
+                    m_stats.m_nla_permanently_banned_powers_lemmas++;
+                    break;
+                case DIVISION_LEMMA:
+                    m_stats.m_nla_permanently_banned_division_lemmas++;
+                    break;
+                case GROBNER_LEMMA:
+                    m_stats.m_nla_permanently_banned_grobner_lemmas++;
+                    break;
+                case HORNER_LEMMA:
+                    m_stats.m_nla_permanently_banned_horner_lemmas++;
+                    break;
+                case FACTOR_ZERO_LEMMA:
+                    m_stats.m_nla_permanently_banned_factor_zero_lemmas++;
+                    break;
+                case FACTOR_NEUTRAL_LEMMA:
+                    m_stats.m_nla_permanently_banned_factor_neutral_lemmas++;
+                    break;
+                default:
+                    TRACE(nla_throttle, tout << "Unexpected throttle kind in permanent ban: " << static_cast<int>(k) << "\n";);
+            }
+            
             TRACE(nla_throttle, 
                   tout << "banned lemma for life, kind=" << static_cast<int>(k) 
                        << " after " << count << " throttles\n";);