diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index da00f6209..00c391fa7 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2959,7 +2959,11 @@ def get_platform_toolset_str():
     if len(tokens) < 2:
         return default
     else:
-        return 'v' + tokens[0] + tokens[1]
+        if tokens[0] == "15": 
+            # Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141
+            return "v141"
+        else:
+            return 'v' + tokens[0] + tokens[1]
 
 def mk_vs_proj_property_groups(f, name, target_ext, type):
     f.write('  <ItemGroup Label="ProjectConfigurations">\n')
diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h
index b6c3c4ef2..508692e5a 100644
--- a/src/util/lp/bound_analyzer_on_row.h
+++ b/src/util/lp/bound_analyzer_on_row.h
@@ -253,7 +253,6 @@ public :
             if (str)
                 strict = true;
         }
-
         bound /= l_coeff;
         if (is_pos(l_coeff)) {
             limit_j(m_column_of_l, bound, true, false, strict);
diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h
index ea851b865..71d69c3a4 100644
--- a/src/util/lp/lar_core_solver.h
+++ b/src/util/lp/lar_core_solver.h
@@ -599,7 +599,7 @@ public:
         }
 
         if (no_r_lu()) { // it is the case where m_d_solver gives a degenerated basis, we need to roll back
-            std::cout << "no_r_lu" << std::endl;
+            //            std::cout << "no_r_lu" << std::endl;
             catch_up_in_lu_in_reverse(changes_of_basis, m_r_solver);
             m_r_solver.find_feasible_solution();
             m_d_basis = m_r_basis;
diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index d70636465..a0dba9de7 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -533,13 +533,19 @@ update_basis_and_x(int entering, int leaving, X const & tt) {
             init_factorization(m_factorization, m_A, m_basis, m_settings);
             if (!find_x_by_solving()) {
                 restore_x(entering, tt);
-                lean_assert(!A_mult_x_is_off());
+                if(A_mult_x_is_off()) {
+                    m_status = FLOATING_POINT_ERROR;
+                    m_iters_with_no_cost_growing++;
+                    return false;
+                }
+                    
                 init_factorization(m_factorization, m_A, m_basis, m_settings);
                 m_iters_with_no_cost_growing++;
                 if (m_factorization->get_status() != LU_status::OK) {
                     std::stringstream s;
-                    s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
-                    throw_exception(s.str());
+                    //                    s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
+                    m_status = FLOATING_POINT_ERROR;
+                    return false;
                 }
                 return false;
             }
diff --git a/src/util/lp/lu.hpp b/src/util/lp/lu.hpp
index b13583d17..2d2c7c7c4 100644
--- a/src/util/lp/lu.hpp
+++ b/src/util/lp/lu.hpp
@@ -605,13 +605,13 @@ void lu<T, X>::process_column(int j) {
     unsigned pi, pj;
     bool success = m_U.get_pivot_for_column(pi, pj, m_settings.c_partial_pivoting, j);
     if (!success) {
-        LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl);
+        //        LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl);
         m_failure = true;
         return;
     }
 
     if (static_cast<int>(pi) == -1) {
-        LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl);
+        // LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl);
         m_failure = true;
         return;
     }