diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp
index 6aed46f64..17be983fe 100644
--- a/src/ast/euf/euf_etable.cpp
+++ b/src/ast/euf/euf_etable.cpp
@@ -203,7 +203,7 @@ namespace euf {
         SASSERT(n->num_args() > 0);
         enode * n_prime;
         void * t = get_table(n); 
-        verbose_stream() << "insert " << n << "\n";
+        //verbose_stream() << "insert " << n << "\n";
         switch (static_cast<table_kind>(GET_TAG(t))) {
         case UNARY:
             n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n);
@@ -225,10 +225,10 @@ namespace euf {
         SASSERT(n->num_args() > 0);
         void * t = get_table(n); 
         static unsigned count = 0;
-        verbose_stream() << "erase " << (++count) << " " << n << "\n";
-        if (count == 10398) {
-            verbose_stream() << "here\n";
-        }
+        //verbose_stream() << "erase " << (++count) << " " << n << "\n";
+        // if (count == 10398) {
+        //     verbose_stream() << "here\n";
+        // }
         switch (static_cast<table_kind>(GET_TAG(t))) {
         case UNARY:
             UNTAG(unary_table*, t)->erase(n);
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index fc1c8d3dc..34666e040 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -150,21 +150,22 @@ namespace lp {
         }
         for (auto const& c : A.column(j)) {
             unsigned row_index = c.var();
-            unsigned i = lrac.m_r_basis[row_index];
-            auto old_val = lia.get_value(i);
+            unsigned bj = lrac.m_r_basis[row_index];
+            auto old_val = lia.get_value(bj);
             auto new_val = old_val - impq(c.coeff()*delta);
-            if (lia.has_lower(i) && new_val < lra.get_lower_bound(i))
+            if (lia.has_lower(bj) && new_val < lra.get_lower_bound(bj))
                 return false;
-            if (lia.has_upper(i) && new_val > lra.get_upper_bound(i))
+            if (lia.has_upper(bj) && new_val > lra.get_upper_bound(bj))
                 return false;
             if (old_val.is_int() && !new_val.is_int()){
                 return false; // do not waste resources on this case
             }
-            lp_assert(i != v || new_val.is_int())
+            // if bj == v, then, because we are patching the lra.get_value(v),
+            // we just need to assert that the lra.get_value(v) would be integral.
+            lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int());
         }
         
         lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta));
-         
         return true;
     }
     
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index f4067d9bb..4aecbf2cc 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -619,11 +619,10 @@ namespace lp {
     }
 
     void lar_solver::add_touched_row(unsigned rid) {
-        m_touched_rows.insert(rid);
+        if (m_settings.bound_propagation())
+            m_touched_rows.insert(rid);
     }
 
-   
-    
     bool lar_solver::use_tableau_costs() const {
         return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
     }
@@ -1019,7 +1018,7 @@ namespace lp {
         SASSERT(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE);
         SASSERT(m_columns_with_changed_bounds.empty());
         numeric_pair<mpq> const& rp = get_column_value(j);
-        return rp.x + m_delta * rp.y;        
+        return from_model_in_impq_to_mpq(rp);        
     }
 
     mpq lar_solver::get_tv_value(tv const& t) const {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index e73e6818c..fc58d0a70 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -497,6 +497,7 @@ class lar_solver : public column_namer {
     std::ostream& display(std::ostream& out) const;
 
     bool init_model() const;
+    mpq from_model_in_impq_to_mpq(const impq& v) const { return v.x + m_delta * v.y; }
     mpq get_value(column_index const& j) const;
     mpq get_tv_value(tv const& t) const;
     const impq& get_tv_ivalue(tv const& t) const;