diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index ef71d37da..13288a214 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -103,7 +103,6 @@ struct statistics {
     unsigned m_make_feasible = 0;
     unsigned m_total_iterations = 0;
     unsigned m_iters_with_no_cost_growing = 0;
-    unsigned m_num_factorizations = 0;
     unsigned m_num_of_implied_bounds = 0;
     unsigned m_need_to_solve_inf = 0;
     unsigned m_max_cols = 0;
@@ -137,44 +136,47 @@ struct statistics {
     unsigned m_bounds_tightening_conflicts = 0;
     unsigned m_bounds_tightenings = 0;
     unsigned m_nla_throttled_lemmas = 0;
+    unsigned m_nla_bounds_lemmas = 0;
+    unsigned m_nla_bounds_propagations = 0;
     ::statistics m_st = {};
 
     void reset() {
         *this = statistics{};
     }
     void collect_statistics(::statistics& st) const {
-        st.update("arith-factorizations", m_num_factorizations);
-        st.update("arith-make-feasible", m_make_feasible);
-        st.update("arith-max-columns", m_max_cols);
-        st.update("arith-max-rows", m_max_rows);
-        st.update("arith-gcd-calls", m_gcd_calls);
-        st.update("arith-gcd-conflict", m_gcd_conflicts);
-        st.update("arith-cube-calls", m_cube_calls);
-        st.update("arith-cube-success", m_cube_success);
-        st.update("arith-patches", m_patches);
-        st.update("arith-patches-success", m_patches_success);
-        st.update("arith-hnf-calls", m_hnf_cutter_calls);
-        st.update("arith-hnf-cuts", m_hnf_cuts);
-        st.update("arith-gomory-cuts", m_gomory_cuts);
-        st.update("arith-horner-calls", m_horner_calls);
-        st.update("arith-horner-conflicts", m_horner_conflicts);
-        st.update("arith-horner-cross-nested-forms", m_cross_nested_forms);
-        st.update("arith-grobner-calls", m_grobner_calls);
-        st.update("arith-grobner-conflicts", m_grobner_conflicts);
-        st.update("arith-offset-eqs", m_offset_eqs);
-        st.update("arith-fixed-eqs", m_fixed_eqs);
+        st.update("arith-lp-make-feasible", m_make_feasible);
+        st.update("arith-lp-max-columns", m_max_cols);
+        st.update("arith-lp-max-rows", m_max_rows);
+        st.update("arith-lp-offset-eqs", m_offset_eqs);
+        st.update("arith-lp-fixed-eqs", m_fixed_eqs);
+        st.update("arith-lia-patches", m_patches);
+        st.update("arith-lia-patches-success", m_patches_success);
+        st.update("arith-lia-gcd-calls", m_gcd_calls);
+        st.update("arith-lia-gcd-conflict", m_gcd_conflicts);
+        st.update("arith-lia-cube-calls", m_cube_calls);
+        st.update("arith-lia-cube-success", m_cube_success);
+        st.update("arith-lia-hermite-calls", m_hnf_cutter_calls);
+        st.update("arith-lia-hermite-cuts", m_hnf_cuts);
+        st.update("arith-lia-gomory-cuts", m_gomory_cuts);
+        st.update("arith-lia-diophantine-calls", m_dio_calls);
+        st.update("arith-lia-diophantine-tighten-conflicts", m_dio_tighten_conflicts);
+        st.update("arith-lia-diophantine-rewrite-conflicts", m_dio_rewrite_conflicts);
+        st.update("arith-lia-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
+        st.update("arith-lia-bounds-tightenings", m_bounds_tightenings);
+        st.update("arith-nla-horner-calls", m_horner_calls);
+        st.update("arith-nla-horner-conflicts", m_horner_conflicts);
+        st.update("arith-nla-horner-cross-nested-forms", m_cross_nested_forms);
+        st.update("arith-nla-grobner-calls", m_grobner_calls);
+        st.update("arith-nla-grobner-conflicts", m_grobner_conflicts);
         st.update("arith-nla-add-bounds", m_nla_add_bounds);
         st.update("arith-nla-propagate-bounds", m_nla_propagate_bounds);
         st.update("arith-nla-propagate-eq", m_nla_propagate_eq);
         st.update("arith-nla-lemmas", m_nla_lemmas);
-        st.update("arith-nra-calls", m_nra_calls);   
-        st.update("arith-bounds-improvements", m_nla_bounds_improvements);
-        st.update("arith-dio-calls", m_dio_calls);
-        st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts);
-        st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts);
-        st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
-        st.update("arith-bounds-tightenings", m_bounds_tightenings);
+        st.update("arith-nla-nra-calls", m_nra_calls);   
+        st.update("arith-nla-bounds-improvements", m_nla_bounds_improvements);
         st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas);
+        st.update("arith-nla-bounds-lemmas", m_nla_bounds_lemmas);
+        st.update("artih-nla-bounds-propagations", m_nla_bounds_propagations);
         st.copy(m_st);
     }
 };
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 66505c698..3d947dbe8 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -378,6 +378,7 @@ namespace nla {
     bool monomial_bounds::add_lemma() {
         if (c().lra.get_status() != lp::lp_status::INFEASIBLE)
             return false;
+        c().lp_settings().stats().m_nla_bounds_lemmas++;
         lp::explanation exp;
         c().lra.get_infeasibility_explanation(exp);
         lemma_builder lemma(c(), "propagate fixed - infeasible lra");
@@ -422,6 +423,7 @@ namespace nla {
         TRACE(nla_solver, tout << "propagate fixed " << m << " =  0, fixed_to_zero = " << fixed_to_zero << "\n";);
         c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, rational(0), dep);
         
+        c().lp_settings().stats().m_nla_bounds_propagations++;
         // propagate fixed equality
         auto exp = get_explanation(dep);        
         c().add_fixed_equality(m.var(), rational(0), exp);
@@ -431,7 +433,7 @@ namespace nla {
         auto* dep = explain_fixed(m, k);
         TRACE(nla_solver, tout << "propagate fixed " << m << " = " << k << "\n";);
         c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
-        
+        c().lp_settings().stats().m_nla_bounds_propagations++;
         // propagate fixed equality
         auto exp = get_explanation(dep);        
         c().add_fixed_equality(m.var(), k, exp);
@@ -448,6 +450,7 @@ namespace nla {
 
         if (k == 1) {
             lp::explanation exp = get_explanation(dep);
+            c().lp_settings().stats().m_nla_bounds_propagations++;
             c().add_equality(m.var(), w, exp);
         }
     }