From 03e411c22d98cf527014b65acf06b318a9871198 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 11 Apr 2020 02:27:47 -0700
Subject: [PATCH] fix #3868

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/bound_analyzer_on_row.h |  4 +++-
 src/smt/theory_arith_core.h         |  8 +++-----
 src/smt/theory_lra.cpp              | 28 ++++++----------------------
 3 files changed, 12 insertions(+), 28 deletions(-)

diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 89ddf6336..f8666521a 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -59,7 +59,9 @@ public :
     void analyze() {
         for (const auto & c : m_row) {
             if ((m_column_of_l == -2) && (m_column_of_u == -2))
-                break;
+                return;
+            if (c.coeff().is_big()) 
+                return;
             analyze_bound_on_var_on_coeff(c.var(), c.coeff());
         }
         if (m_column_of_u >= 0)
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index eab01c5f5..c538d78c4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3029,10 +3029,8 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::propagate_bounds() {
         TRACE("propagate_bounds_detail", display(tout););
-        typename svector<unsigned>::iterator it  = m_to_check.begin();
-        typename svector<unsigned>::iterator end = m_to_check.end();
-        for (; it != end; ++it) {
-            row & r = m_rows[*it];
+        for (unsigned r_idx : m_to_check) {
+            row & r = m_rows[r_idx];
             if (r.get_base_var() != null_theory_var) {
                 if (r.size() < max_lemma_size()) { // Ignore big rows.
                     int lower_idx;
@@ -3054,7 +3052,7 @@ namespace smt {
                     }
 
                     // sneaking cheap eq detection in this loop
-                    propagate_cheap_eq(*it);
+                    propagate_cheap_eq(r_idx);
                 }
 
 #if 0
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ce54fd33d..52d716565 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2994,8 +2994,6 @@ public:
 
     void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) {
         lp::constraint_index ci = b.get_constraint(is_true);
-        lp::column_index j = lp().to_column_index(b.get_var());
-        bool was_fixed = lp().is_fixed(j);
         m_solver->activate(ci);
         if (is_infeasible()) {
             return;
@@ -3008,7 +3006,7 @@ public:
             ++m_stats.m_assert_upper;
         }
         inf_rational const& value = b.get_value(is_true);
-        if (value.is_rational()) {
+        if (propagate_eqs() && value.is_rational()) {
             propagate_eqs(b.tv(), ci, k, b, value.get_rational());
         }
     }
@@ -3052,28 +3050,14 @@ public:
     typedef std::pair<rational, bool> value_sort_pair;
     typedef pair_hash<obj_hash<rational>, bool_hash> value_sort_pair_hash;
     typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-    value2var               m_fixed_var_table;
+    value2var                       m_fixed_var_table;
 
     void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) {
-        bool best_bound = false;
-        if (k == lp::GE) {
-            best_bound = set_lower_bound(t, ci, value);
+        if (k == lp::GE && set_lower_bound(t, ci, value) && has_upper_bound(t.index(), ci, value)) {
+            fixed_var_eh(b.get_var(), value);
         }
-        else if (k == lp::LE) {
-            best_bound = set_upper_bound(t, ci, value);
-        }
-
-        if (propagate_eqs() && best_bound) {
-            if (k == lp::GE) {
-                if (has_upper_bound(t.index(), ci, value)) {
-                    fixed_var_eh(b.get_var(), value);
-                }
-            }
-            else if (k == lp::LE) {
-                if (has_lower_bound(t.index(), ci, value)) {
-                    fixed_var_eh(b.get_var(), value);
-                }
-            }
+        else if (k == lp::LE && set_upper_bound(t, ci, value) && has_lower_bound(t.index(), ci, value)) {
+            fixed_var_eh(b.get_var(), value);
         }
     }