diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 462c9855a..46491bc23 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -191,7 +191,10 @@ namespace opt {
             SASSERT(delta_per_step.is_int());
             SASSERT(delta_per_step.is_pos());
             is_sat = m_s->check_sat(0, nullptr);
-            TRACE("opt", tout << "check " << is_sat << "\n";);
+            TRACE("opt", tout << "check " << is_sat << "\n";
+                  tout << "lower: " << m_lower[obj_index] << "\n";
+                  tout << "upper: " << m_upper[obj_index] << "\n";
+                  );
             if (is_sat == l_true) {                
                 m_s->maximize_objective(obj_index, bound);
                 m_s->get_model(m_model);
@@ -232,6 +235,8 @@ namespace opt {
         }
         m_s->pop(num_scopes);        
 
+        TRACE("opt", tout << is_sat << " " << num_scopes << "\n";);
+
         if (is_sat == l_false && !m_model) {
             return l_false;
         }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ceeb1617f..27362fc77 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -955,6 +955,7 @@ public:
     }
 
     void push_scope_eh() {
+        TRACE("arith", tout << "push\n";);
         m_scopes.push_back(scope());
         scope& s = m_scopes.back();
         s.m_bounds_lim = m_bounds_trail.size();
@@ -969,6 +970,7 @@ public:
     }
 
     void pop_scope_eh(unsigned num_scopes) {
+        TRACE("arith", tout << "pop " << num_scopes << "\n";);
         if (num_scopes == 0) {
             return;
         }
diff --git a/src/util/lp/lar_core_solver_def.h b/src/util/lp/lar_core_solver_def.h
index ca7915c7d..476e11698 100644
--- a/src/util/lp/lar_core_solver_def.h
+++ b/src/util/lp/lar_core_solver_def.h
@@ -278,6 +278,7 @@ void lar_core_solver::solve() {
     CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
     lp_assert((!settings().use_tableau()) || r_basis_is_OK());
     if (need_to_presolve_with_double_solver()) {
+        TRACE("lar_solver", tout << "presolving\n";);
         prefix_d();
         lar_solution_signature solution_signature;
         vector<unsigned> changes_of_basis = find_solution_signature_with_doubles(solution_signature);
@@ -293,6 +294,7 @@ void lar_core_solver::solve() {
         lp_assert(!settings().use_tableau() || r_basis_is_OK());
     } else {
         if (!settings().use_tableau()) {
+            TRACE("lar_solver", tout << "no tablau\n";);
             bool snapped = m_r_solver.snap_non_basic_x_to_bound();   
             lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
             if (snapped)
@@ -300,8 +302,10 @@ void lar_core_solver::solve() {
         }
         if (m_r_solver.m_look_for_feasible_solution_only)
             m_r_solver.find_feasible_solution();
-        else
+        else {
+            TRACE("lar_solver", tout << "solve\n";);
             m_r_solver.solve();
+        }
         lp_assert(!settings().use_tableau() || r_basis_is_OK());
     }
     if (m_r_solver.get_status() == lp_status::INFEASIBLE) {
diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h
index ad861cc7a..bc3ccc055 100644
--- a/src/util/lp/lp_primal_core_solver_def.h
+++ b/src/util/lp/lp_primal_core_solver_def.h
@@ -863,6 +863,7 @@ 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", tout << "solve " << this->get_status() << "\n";);
     if (numeric_traits<T>::precise() && this->m_settings.use_tableau())
         return solve_with_tableau();
 
@@ -882,6 +883,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
         }
         one_iteration();
 
+        TRACE("lar_solver", tout << "one iteration: " << this->get_status() << "\n";);
         lp_assert(!this->m_using_infeas_costs || this->costs_on_nbasis_are_zeros());
         switch (this->get_status()) {
         case lp_status::OPTIMAL:  // double check that we are at optimum
diff --git a/src/util/lp/lp_primal_core_solver_tableau_def.h b/src/util/lp/lp_primal_core_solver_tableau_def.h
index 8f9cf7ff1..0d6f7ac92 100644
--- a/src/util/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/util/lp/lp_primal_core_solver_tableau_def.h
@@ -35,6 +35,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
     X t;
     int leaving = find_leaving_and_t_tableau(entering, t);
     if (leaving == -1) {
+        TRACE("lar_solver", tout << "nothing leaving " << entering << "\n";);
         this->set_status(lp_status::UNBOUNDED);
         return;
     }
@@ -117,6 +118,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
         }
         else 
             one_iteration_tableau();
+        TRACE("lar_solver", tout << "one iteration tableau " << this->get_status() << "\n";);
         switch (this->get_status()) {
         case lp_status::OPTIMAL:  // double check that we are at optimum
         case lp_status::INFEASIBLE: