diff --git a/src/math/lp/u_set.h b/src/math/lp/u_set.h
index 7bb92ca40..7f8b1bd6f 100644
--- a/src/math/lp/u_set.h
+++ b/src/math/lp/u_set.h
@@ -15,7 +15,7 @@ Author:
 
 Revision History:
 
-TBD use indexed_uint_set from src/util/uu_set.h, 
+TBD use indexed_uint_set from src/util/uint_set.h, 
 
 --*/
 #pragma once
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 29603db81..5ea615ab4 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -49,6 +49,7 @@ namespace smt {
         unsigned m_gb_simplify, m_gb_superpose, m_gb_compute_basis, m_gb_num_processed;
         unsigned m_nl_branching, m_nl_linear, m_nl_bounds, m_nl_cross_nested;
         unsigned m_branch_infeasible_int, m_branch_infeasible_var;
+        unsigned m_tableau_max_rows, m_tableau_max_columns;
 
         void reset() { memset(this, 0, sizeof(theory_arith_stats)); }
         theory_arith_stats() { reset(); }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index c223922f5..63cdc4f22 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -258,6 +258,7 @@ namespace smt {
 
         c_entry.m_row_id    = r_id;
         c_entry.m_row_idx   = r_idx;
+        m_stats.m_tableau_max_columns = std::max(m_stats.m_tableau_max_columns, (unsigned)c_idx + 1);
     }
 
     /**
@@ -832,6 +833,7 @@ namespace smt {
     */
     template<typename Ext>
     unsigned theory_arith<Ext>::mk_row() {
+        
         unsigned r;
         if (m_dead_rows.empty()) {
             r = m_rows.size();
@@ -844,6 +846,7 @@ namespace smt {
         m_in_to_check.assure_domain(r);
         SASSERT(m_rows[r].size() == 0);
         SASSERT(m_rows[r].num_entries() == 0);
+        m_stats.m_tableau_max_rows = std::max(m_stats.m_tableau_max_rows, m_rows.size());
         return r;
     }
 
diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h
index f73f86825..ee1268b79 100644
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@@ -48,6 +48,8 @@ namespace smt {
         st.update("arith pseudo nonlinear", m_stats.m_nl_linear);
         st.update("arith nonlinear bounds", m_stats.m_nl_bounds);
         st.update("arith nonlinear horner", m_stats.m_nl_cross_nested);
+        st.update("arith tableau max rows", m_stats.m_tableau_max_rows);
+        st.update("arith tableau max columns", m_stats.m_tableau_max_columns);
         m_arith_eq_adapter.collect_statistics(st);
     }