From 6027224e34f84b45e0b2b6476c7246353eae4661 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 7 Feb 2020 14:21:11 -0800
Subject: [PATCH] do not throttle lp bound propagation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/stacked_vector.h |  4 +++-
 src/smt/theory_lra.cpp       | 24 +++++++++---------------
 2 files changed, 12 insertions(+), 16 deletions(-)

diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h
index ad83b3d87..90131fbeb 100644
--- a/src/math/lp/stacked_vector.h
+++ b/src/math/lp/stacked_vector.h
@@ -140,8 +140,10 @@ public:
         for (unsigned j = m_changes.size(); j-- > first_change; ) {
             const auto & p = m_changes[j];
             unsigned jc = p.first;
-            if (jc < m_vector.size())
+            if (jc < m_vector.size()) {
                 m_vector[jc] = p.second; // restore the old value
+                m_vector[jc] = p.second; // restore the old value
+            }
         }
         resize(m_changes, first_change);
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 745541446..ccf4a17c8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2346,23 +2346,18 @@ public:
             
     }
 
-    unsigned m_propagation_delay{1};
-    unsigned m_propagation_count{0};
-    
     bool should_propagate() {
-        ++m_propagation_count;
-        return BP_NONE != propagation_mode() && (m_propagation_count >= m_propagation_delay);
+        return BP_NONE != propagation_mode();
     }
 
-    void update_propagation_threshold(bool made_progress) {
-        m_propagation_count = 0;
-        if (made_progress) {
-            m_propagation_delay = std::max(1u, m_propagation_delay-1u);
-        }
-        else {
-            m_propagation_delay += 2;
-        }
-    }
+    // void update_propagation_threshold(bool  made_progress) {
+    //      if (made_progress) {
+    //         m_propagation_delay = std::max(1u, m_propagation_delay-1u);
+    //     }
+    //     else {
+    //         m_propagation_delay += 2;
+    //     }
+    // }
 
     void propagate_bounds_with_lp_solver() {
         if (!should_propagate()) 
@@ -2383,7 +2378,6 @@ public:
                 propagate_lp_solver_bound(bp.m_ibounds[i]);
             }
         }
-        update_propagation_threshold(props < m_stats.m_bound_propagations1);
     }
 
     bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {