diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp
index e8d75f461..61bd9370c 100644
--- a/src/ast/expr_substitution.cpp
+++ b/src/ast/expr_substitution.cpp
@@ -65,8 +65,8 @@ std::ostream& expr_substitution::display(std::ostream& out) {
 }
 
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
-    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); 
-    if (entry->get_data().m_value == 0) {
+    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr); 
+    if (entry->get_data().m_value == nullptr) {
         // new entry
         m_manager.inc_ref(c);
         m_manager.inc_ref(def);
@@ -89,14 +89,14 @@ void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_depend
         entry->get_data().m_value = def;
         if (proofs_enabled()) {
             obj_map<expr, proof*>::obj_map_entry * entry_pr = m_subst_pr->find_core(c);
-            SASSERT(entry_pr != 0);
+            SASSERT(entry_pr != nullptr);
             m_manager.inc_ref(def_pr);
             m_manager.dec_ref(entry_pr->get_data().m_value);
             entry_pr->get_data().m_value = def_pr;
         }
         if (unsat_core_enabled()) {
             obj_map<expr, expr_dependency*>::obj_map_entry * entry_dep = m_subst_dep->find_core(c);
-            SASSERT(entry_dep != 0);
+            SASSERT(entry_dep != nullptr);
             m_manager.inc_ref(def_dep);
             m_manager.dec_ref(entry_dep->get_data().m_value);
             entry_dep->get_data().m_value = def_dep;
diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp
index f28864e27..114bc69b9 100644
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@@ -342,7 +342,7 @@ namespace spacer {
                     
                     proof_ref pr2(m);
                     {
-                        scoped_watch _t_ (m_hyp_reduce2_sw);
+                        // scoped_watch _t_ (m_hyp_reduce2_sw);
                         hypothesis_reducer hyp_reducer(m);
                         pr2 = hyp_reducer.reduce(pr1);
                     }
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 80a81ba3a..eb766a1ba 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -233,7 +233,8 @@ namespace opt {
         get_model(m_model);
         inf_eps val2;
         m_valid_objectives[i] = true;
-        TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << "\n";);
+        has_shared = true;
+        TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";);
         if (!m_models[i]) {
             set_model(i);
         }
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 4a35acd02..462c9855a 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -215,7 +215,7 @@ namespace opt {
                     ++num_scopes;
                     bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
                 }
-                TRACE("opt", tout << delta_per_step << " " << bound << "\n";);
+                TRACE("opt", tout << "delta: " << delta_per_step << " " << bound << "\n";);
                 m_s->assert_expr(bound);
             }
             else if (is_sat == l_false && delta_per_step > rational::one()) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1a63b97fb..774dc09f3 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -236,7 +236,6 @@ class theory_lra::imp {
     expr*                  m_not_handled;
     ptr_vector<app>        m_underspecified;
     ptr_vector<expr>       m_idiv_terms;
-    unsigned               m_idiv_bound_calls;
     unsigned_vector        m_var_trail;
     vector<ptr_vector<lp_api::bound> > m_use_list;        // bounds where variables are used.
 
@@ -308,7 +307,6 @@ class theory_lra::imp {
         if (m_solver) return;
 
         reset_variable_values();
-        m_idiv_bound_calls;
         m_theory_var2var_index.reset();
         m_solver = alloc(lp::lar_solver); 
         lp_params lp(ctx().get_params());
@@ -1103,24 +1101,6 @@ public:
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
 
-    // create axiom for 
-    //    u = v + r*w,
-    ///   abs(r) > r >= 0
-    void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) {
-        app_ref term(m);
-        term = a.mk_sub(get_enode(u)->get_owner(), 
-                        a.mk_add(get_enode(v)->get_owner(),
-                                 a.mk_mul(a.mk_numeral(r, true), 
-                                          get_enode(w)->get_owner())));
-        theory_var z = internalize_def(term);
-        lp::var_index vi = get_var_index(z);
-        add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero()));
-        add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero()));
-        add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::GE, rational::zero()));
-        add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::LT, abs(r)));
-        TRACE("arith", m_solver->print_constraints(tout << term << "\n"););
-    }
-
     void mk_idiv_mod_axioms(expr * p, expr * q) {
         if (a.is_zero(q)) {
             return;
@@ -1681,16 +1661,31 @@ public:
      * 0 < q => (v(p)/v(q) <= p/q => v(p)/v(q) - 1 < n) 
      * 
      */
+
+    bool is_bounded(expr* n) {
+        expr* x = nullptr, *y = nullptr;
+        while (true) {
+            if (a.is_idiv(n, x, y) && a.is_numeral(y)) {
+                n = x;
+            }
+            else if (a.is_mod(n, x, y) && a.is_numeral(y)) {
+                return true;
+            }
+            else if (a.is_numeral(n)) {
+                return true;
+            }
+            else {
+                return false;
+            }
+        }
+    }
+
     bool check_idiv_bounds() {
         if (m_idiv_terms.empty()) {
             return true;
         }
-        ++m_idiv_bound_calls;
-        if ((m_idiv_bound_calls % 10) != 0) {
-            return true;
-        }
-        bool all_divs_valid = true;        
         init_variable_values();
+        bool all_divs_valid = true;        
         for (expr* n : m_idiv_terms) {
             expr* p = nullptr, *q = nullptr;
             VERIFY(a.is_idiv(n, p, q));
@@ -1709,9 +1704,11 @@ public:
                 continue;
             }
 
-            if (a.is_numeral(q, r2) && r2.is_pos()) {
-                if (get_value(v) == div(r1, r2)) continue;
+            if (a.is_numeral(q, r2) && r2.is_pos() && is_bounded(n)) {
+                rational val_v = get_value(v);
+                if (val_v == div(r1, r2)) continue;
             
+                TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
                 rational div_r = div(r1, r2);
                 // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2)
                 // p >= q * div(r1, q) => div(r1, q) <= div(p, q)
@@ -1853,14 +1850,17 @@ public:
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
+
+        lbool lia_check = l_undef;
         if (!check_idiv_bounds()) {
-            TRACE("arith", tout << "idiv bounds check\n";);
             return l_false;
         }
         m_explanation.reset();
         switch (m_lia->check()) {
         case lp::lia_move::sat:
-            return l_true;
+            lia_check = l_true;
+            break;
+
         case lp::lia_move::branch: {
             TRACE("arith", tout << "branch\n";);
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
@@ -1876,7 +1876,8 @@ public:
             // TBD: ctx().force_phase(ctx().get_literal(b));
             // at this point we have a new unassigned atom that the 
             // SAT core assigns a value to
-            return l_false;
+            lia_check = l_false;
+            break;
         }
         case lp::lia_move::cut: {
             TRACE("arith", tout << "cut\n";);
@@ -1902,24 +1903,27 @@ public:
                   ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
                   display(tout););
             assign(lit);
-            return l_false;
+            lia_check = l_false;
+            break;
         }
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
             m_explanation = m_lia->get_explanation().m_explanation;
             set_conflict1();
-            return l_false;
+            lia_check = l_false;
+            break;
         case lp::lia_move::undef:
             TRACE("arith", tout << "lia undef\n";);
-            return l_undef;
+            lia_check = l_undef;
+            break;
         case lp::lia_move::continue_with_check:
-            return l_undef;
+            lia_check = l_undef;
+            break;
         default:
             UNREACHABLE();
         }
-        UNREACHABLE();
-        return l_undef;
+        return lia_check;
     }
 
     lbool check_nra() {
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 879dfd32f..5db041218 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -346,13 +346,12 @@ void lar_solver::shrink_inf_set_after_pop(unsigned n, int_set & set) {
 
     
 void lar_solver::pop(unsigned k) {
-    TRACE("arith_int", tout << "pop" << std::endl;);
+    TRACE("int_solver", tout << "pop" << std::endl;);
     TRACE("lar_solver", tout << "k = " << k << std::endl;);
 
     m_infeasible_column_index.pop(k);
     unsigned n = m_columns_to_ul_pairs.peek_size(k);
     m_var_register.shrink(n);
-    TRACE("arith_int", tout << "pop" << std::endl;);
     if (m_settings.use_tableau()) {
         pop_tableau();
     }
@@ -453,6 +452,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: "););
     auto & rslv = m_mpq_lar_core_solver.m_r_solver;
     rslv.m_using_infeas_costs = false;
     lp_assert(costs_are_zeros_for_r_solver());
@@ -473,6 +473,7 @@ bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term,
                                                      impq &term_max) {
     settings().backup_costs = false;
     bool ret = false;
+    TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n"; print_constraints(tout););
     switch (settings().simplex_strategy()) {
     case simplex_strategy_enum::tableau_rows:
         prepare_costs_for_r_solver(term);
@@ -506,8 +507,9 @@ bool lar_solver::remove_from_basis(unsigned j) {
 }
 
 lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const {
-    if (is_term(j_or_term))
+    if (is_term(j_or_term)) {
         return get_term(j_or_term);
+    }
     if (j_or_term < m_mpq_lar_core_solver.m_r_x.size()) {
         lar_term r;
         r.add_monomial(one_of_type<mpq>(), j_or_term);
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 1135c893e..da1a3deaa 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -60,7 +60,7 @@ public:
     }
 
     void stop() {
-        SASSERT(m_running);
+        // SASSERT(m_running);
         DEBUG_CODE(m_running = false;);
         m_elapsed += get() - m_start;
     }