From 3ed490d4edb298f85c8f0444ec869215ff140314 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Jan 2021 16:51:01 -0800
Subject: [PATCH] tune backtracking

---
 src/math/lp/lar_solver.cpp | 7 ++++---
 src/math/lp/lar_solver.h   | 2 ++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index ca491a169..534a63972 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1454,15 +1454,16 @@ namespace lp {
         vector<unsigned> became_feas;
         clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.inf_set());
         std::unordered_set<unsigned> basic_columns_with_changed_cost;
-        auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.inf_set();
-        for (auto j : inf_index_copy) {
+        m_inf_index_copy.reset();
+        for (auto j : m_mpq_lar_core_solver.m_r_solver.inf_set())
+            m_inf_index_copy.push_back(j);
+        for (auto j : m_inf_index_copy) {
             if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) {
                 continue;
             }
             // some basic columns might become non-basic - these columns need to be made feasible
             numeric_pair<mpq> delta;
             if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) {
-
                 change_basic_columns_dependend_on_a_given_nb_column(j, delta);
             }
             became_feas.push_back(j);
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 87227370f..cff0f9028 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -94,6 +94,8 @@ class lar_solver : public column_namer {
     // these are basic columns with the value changed, so the the corresponding row in the tableau
     // does not sum to zero anymore
     u_set                                               m_incorrect_columns;
+    // copy of m_r_solver.inf_set()
+    unsigned_vector                                     m_inf_index_copy;
     stacked_value<unsigned>                             m_term_count;
     vector<lar_term*>                                   m_terms;
     indexed_vector<mpq>                                 m_column_buffer;