diff --git a/src/util/lp/lar_core_solver_def.h b/src/util/lp/lar_core_solver_def.h
index b945b0e51..ca7915c7d 100644
--- a/src/util/lp/lar_core_solver_def.h
+++ b/src/util/lp/lar_core_solver_def.h
@@ -265,12 +265,14 @@ unsigned lar_core_solver::get_number_of_non_ints() const {
 }
 
 void lar_core_solver::solve() {
+    TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
     lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
     lp_assert(m_r_solver.inf_set_is_correct());
 	TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.m_inf_set.size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
 	if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) {
-		m_r_solver.set_status(lp_status::OPTIMAL);
-		return;
+            m_r_solver.set_status(lp_status::OPTIMAL);
+            TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
+            return;
 	}
     ++settings().st().m_need_to_solve_inf;
     CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
@@ -310,6 +312,8 @@ void lar_core_solver::solve() {
     lp_assert(r_basis_is_OK());
     lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
     lp_assert(m_r_solver.inf_set_is_correct());
+
+    TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
 }
 
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 8e0ee89c6..48b08a215 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -403,12 +403,15 @@ bool lar_solver::maximize_term_on_tableau(const lar_term & term,
 
     m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::FEASIBLE);
     m_mpq_lar_core_solver.solve();
-    if (m_mpq_lar_core_solver.m_r_solver.get_status() == lp_status::UNBOUNDED)
+    lp_status st = m_mpq_lar_core_solver.m_r_solver.get_status();
+    TRACE("lar_solver", tout << st << "\n";);
+    if (st == lp_status::UNBOUNDED) {
         return false;
-
-    term_max = term.apply(m_mpq_lar_core_solver.m_r_x);
-
-    return true;
+    }
+    else {
+        term_max = term.apply(m_mpq_lar_core_solver.m_r_x);        
+        return true;
+    }
 }
 
 bool lar_solver::costs_are_zeros_for_r_solver() const {
@@ -452,7 +455,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
 
 void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
         
-    TRACE("lar_solver", print_term(term, tout << "prepare: "););
+    TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
     auto & rslv = m_mpq_lar_core_solver.m_r_solver;
     rslv.m_using_infeas_costs = false;
     lp_assert(costs_are_zeros_for_r_solver());
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 9a6549917..c1b8aa987 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -136,8 +136,6 @@ public:
     }
 
     const vector<unsigned> & non_basis() const { return m_nbasis; }
-
-
     
     void set_status(lp_status status) {
         m_status = status;
diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h
index a43764172..a91491313 100644
--- a/src/util/lp/lp_primal_core_solver_def.h
+++ b/src/util/lp/lp_primal_core_solver_def.h
@@ -775,6 +775,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
     X t;
     int leaving = find_leaving_and_t_precise(entering, t);
     if (leaving == -1) {
+        TRACE("lar_solver", tout << "non-leaving\n";);
         this->set_status(lp_status::UNBOUNDED);
         return;
     }
@@ -828,6 +829,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
         } else {
             this->set_status(lp_status::TENTATIVE_UNBOUNDED);
         }
+        TRACE("lar_solver", tout << this->get_status() << "\n";);
         return;
     }
     advance_on_entering_and_leaving(entering, leaving, t);
@@ -857,11 +859,11 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
         out << this->m_column_norms[j] << " ";
     }
     out << std::endl;
-    out << std::endl;
-}
+ }
 
 // 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();