From 73696725e4f81ee690247dcfaa2a91eda77974c4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 7 Feb 2026 10:45:15 -1000
Subject: [PATCH] Revert "try fixed int patch period"

This reverts commit 3e2027ec110634699015fa8d4b98767c787888ff.
---
 src/math/lp/int_solver.cpp       | 8 ++++++--
 src/math/lp/lp_params_helper.pyg | 2 +-
 src/math/lp/lp_settings.h        | 2 +-
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 020c628aa..c4de2c3ff 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -54,7 +54,6 @@ namespace lp {
             m_hnf_cut_period = settings().hnf_cut_period();
             m_initial_dio_calls_period = settings().dio_calls_period();
             m_patch_period = settings().m_int_patch_period;
-            SASSERT(m_patch_period > 0);
         } 
 
         bool has_lower(unsigned j) const {
@@ -160,7 +159,8 @@ namespace lp {
         }
         
         bool should_patch() {
-            return m_number_of_calls % m_patch_period == 0;
+            // period == 0 means no throttling (old behavior)
+            return settings().m_int_patch_period == 0 || m_number_of_calls % m_patch_period == 0;
         }
 
         lia_move patch_basic_columns() {
@@ -172,8 +172,12 @@ namespace lp {
                     patch_basic_column(j);
             if (!lra.has_inf_int()) {
                 lia.settings().stats().m_patches_success++;
+                m_patch_period = std::max(1u, settings().m_int_patch_period);
                 return lia_move::sat;
             }
+            // Only throttle if enabled (period > 0)
+            if (settings().m_int_patch_period > 0 && m_patch_period < 16)
+                m_patch_period *= 2;
             return lia_move::undef;     
         }
 
diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg
index de4e9d3fe..a903ae343 100644
--- a/src/math/lp/lp_params_helper.pyg
+++ b/src/math/lp/lp_params_helper.pyg
@@ -9,6 +9,6 @@ def_module_params(module_name='lp',
                           ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
                           ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
                           ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
-                          ('int_patch_period', UINT, 1, 'Skip int_patch_period - 1 calls and then call the patching'),
+                          ('int_patch_period', UINT, 0, 'Period for patching integer columns (0 = no throttling, 1 = throttle adaptively)'),
                          ))
                          
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 18faaf64f..f3745b87b 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -239,7 +239,7 @@ public:
     unsigned         column_number_threshold_for_using_lu_in_lar_solver = 4000;
     unsigned         m_int_gomory_cut_period = 4;
     unsigned         m_int_find_cube_period = 4;
-    unsigned         m_int_patch_period = 1;
+    unsigned         m_int_patch_period = 0;
 private:
     unsigned         m_hnf_cut_period = 4;
     bool             m_int_run_gcd_test = true;