diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 774dc09f3..ceeb1617f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1704,9 +1704,13 @@ public:
                 continue;
             }
 
-            if (a.is_numeral(q, r2) && r2.is_pos() && is_bounded(n)) {
+            if (a.is_numeral(q, r2) && r2.is_pos()) {
                 rational val_v = get_value(v);
                 if (val_v == div(r1, r2)) continue;
+                if (!is_bounded(n)) {
+                    TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
+                    continue;
+                }
             
                 TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
                 rational div_r = div(r1, r2);
diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h
index a91491313..ad861cc7a 100644
--- a/src/util/lp/lp_primal_core_solver_def.h
+++ b/src/util/lp/lp_primal_core_solver_def.h
@@ -357,20 +357,20 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>::try_jump_to_
                                                                                                           bool & unlimited) {
     switch(this->m_column_types[entering]){
     case column_type::boxed: 
-            if (m_sign_of_entering_delta > 0) {
-                t = this->m_upper_bounds[entering] - this->m_x[entering];
-                if (unlimited || t <= theta){
-                    lp_assert(t >= zero_of_type<X>());
-                    return true;
-                }
-            } else { // m_sign_of_entering_delta == -1
-                t = this->m_x[entering] - this->m_lower_bounds[entering];
-                if (unlimited || t <= theta) {
-                    lp_assert(t >= zero_of_type<X>());
-                    return true;
-                }
+        if (m_sign_of_entering_delta > 0) {
+            t = this->m_upper_bounds[entering] - this->m_x[entering];
+            if (unlimited || t <= theta){
+                lp_assert(t >= zero_of_type<X>());
+                return true;
             }
-            return false;
+        } else { // m_sign_of_entering_delta == -1
+            t = this->m_x[entering] - this->m_lower_bounds[entering];
+            if (unlimited || t <= theta) {
+                lp_assert(t >= zero_of_type<X>());
+                return true;
+            }
+        }
+        return false;
     case column_type::upper_bound:
         if (m_sign_of_entering_delta > 0) {
             t = this->m_upper_bounds[entering] - this->m_x[entering];
@@ -863,7 +863,6 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
 
 // returns the number of iterations
 template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
-    TRACE("lar_solver", pretty_print(tout););
     if (numeric_traits<T>::precise() && this->m_settings.use_tableau())
         return solve_with_tableau();