diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index a517b520a..5d9ee543e 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -2038,8 +2038,13 @@ namespace lp {
 
             if (ret != lia_move::undef) 
                 return ret;
-            if (ret == lia_move::undef)
+            if (ret == lia_move::undef) {
                 lra.settings().dio_calls_period() *= 2;
+                if (lra.settings().dio_calls_period() >= 16) {
+                    lra.settings().dio_enable_gomory_cuts() = true;
+                    lra.settings().set_run_gcd_test(true);
+                }
+            }
             return ret;
         }
 
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index ea662f111..3a49f6d5b 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -37,7 +37,6 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_dio = lp_p.dio();
     m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
     m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
-    m_dio_branching_period = lp_p.dio_branching_period();
     m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
     m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
     m_dio_calls_period = lp_p.dio_calls_period();
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 82af740d0..e9ad11ce3 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -133,13 +133,7 @@ struct statistics {
     unsigned m_fixed_eqs = 0;
     unsigned m_dio_calls = 0;
     unsigned m_dio_tighten_conflicts = 0;
-    unsigned m_dio_branch_iterations= 0;
-    unsigned m_dio_branching_depth = 0;
-    unsigned m_dio_branch_from_proofs = 0;
-    unsigned m_dio_branching_infeasibles = 0;
     unsigned m_dio_rewrite_conflicts = 0;
-    unsigned m_dio_branching_sats = 0;
-    unsigned m_dio_branching_conflicts = 0;
     unsigned m_bounds_tightening_conflicts = 0;
     unsigned m_bounds_tightenings = 0;
     ::statistics m_st = {};
@@ -176,14 +170,7 @@ struct statistics {
         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-branch-iterations", m_dio_branch_iterations);
-        st.update("arith-dio-branch-depths", m_dio_branching_depth);
-        st.update("arith-dio-branch-from-proofs", m_dio_branch_from_proofs);
-        st.update("arith-dio-branching-infeasibles", m_dio_branching_infeasibles);
         st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts);
-        st.update("arith-dio-branching-sats", m_dio_branching_sats);
-        st.update("arith-dio-branching-depth", m_dio_branching_depth);
-        st.update("arith-dio-branching-conflicts", m_dio_branching_conflicts);
         st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
         st.update("arith-bounds-tightenings", m_bounds_tightenings);
         st.copy(m_st);
@@ -261,8 +248,6 @@ private:
     bool             m_dio = false;
     bool             m_dio_enable_gomory_cuts = false;
     bool             m_dio_enable_hnf_cuts = true;
-    unsigned         m_dio_branching_period = 100; //  do branching rarely
-    unsigned         m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
     bool             m_dump_bound_lemmas = false;
     bool             m_dio_ignore_big_nums = false;
     unsigned         m_dio_calls_period = 4;
@@ -277,13 +262,12 @@ public:
     unsigned random_next() { return m_rand(); }
     unsigned random_next(unsigned u ) { return m_rand(u); }
     bool dio() { return m_dio; }
+    bool & dio_enable_gomory_cuts() { return m_dio_enable_gomory_cuts; }
     bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; }
     bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; }
     bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; }
-    unsigned dio_branching_period() const { return m_dio_branching_period; }
     bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; }
     void set_random_seed(unsigned s) { m_rand.set_seed(s); }
-    unsigned dio_report_branch_with_term_tigthening_period() const { return m_dio_report_branch_with_term_tigthening_period; }
     bool bound_progation() const { 
         return m_bound_propagation;
     }