diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h
index 34079cd94..c21429c88 100644
--- a/src/math/lp/lp_dual_simplex_def.h
+++ b/src/math/lp/lp_dual_simplex_def.h
@@ -217,14 +217,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::fill_costs_bounds_
         m_can_enter_basis[j] = true;
         this->set_scaled_cost(j);
         this->m_lower_bounds[j] = numeric_traits<T>::zero();
-        this->m_upper_bounds[j] =numeric_traits<T>::one();
+        this->m_upper_bounds[j] = numeric_traits<T>::one();
         break;
     }
     case column_type::free_column: {
         m_can_enter_basis[j] = true;
         this->set_scaled_cost(j);
-        this->m_upper_bounds[j] = free_bound;
-        this->m_lower_bounds[j] =  -free_bound;
+        this->m_upper_bounds[j] =  free_bound;
+        this->m_lower_bounds[j] = -free_bound;
         break;
     }
     case column_type::boxed:
diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp
index bb8c17f33..d7bca705e 100644
--- a/src/tactic/arith/bv2real_rewriter.cpp
+++ b/src/tactic/arith/bv2real_rewriter.cpp
@@ -362,6 +362,11 @@ br_status bv2real_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
               tout << mk_pp(args[i], m()) << " ";
           }
           tout << "\n";);
+    
+    if (u().memory_exceeded()) {
+        std::cout << "tactic exception\n";
+        throw tactic_exception("bv2real-memory exceeded");
+    }
     if(f->get_family_id() == m_arith.get_family_id()) {
         switch (f->get_decl_kind()) {
         case OP_NUM:     return BR_FAILED;