diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 7025facb6..4b915d769 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -144,7 +144,6 @@ bool lar_solver::row_has_a_big_num(unsigned i) const {
     return false;
 }
 
-    
 void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) {
     // todo : create a map from term basic vars to the rows where they are used
     unsigned basis_j = m_mpq_lar_core_solver.m_r_solver.m_basis[i];
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 136c5bcd3..98ba56470 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -151,8 +151,12 @@ public:
         x = y = null_lpvar;
         for (auto& c : lp().get_row(r)) {
             lpvar v = c.var();
-            if (column_is_fixed(v))
+            if (column_is_fixed(v)) {
+                // if (get_lower_bound_rational(c.var()).is_big())
+                //     return false;
                 continue;
+            }
+           
             if (c.coeff().is_one() && x == null_lpvar) {
                 x = v;
                 continue;
@@ -173,6 +177,8 @@ public:
             if (!column_is_fixed(c.var()))
                 continue;
             k -= c.coeff() * get_lower_bound_rational(c.var());
+            if (k.is_big())
+                return false;
         }
         
         if (y == null_lpvar)
@@ -184,7 +190,7 @@ public:
             return true;
         }
 
-        if (/*r.get_base_var() != x &&*/ x > y) {
+        if (!lp().is_base(x) && x > y) {
             std::swap(x, y);
             k.neg();
         }