diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index d3e780d33..8a771e07c 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -166,7 +166,7 @@ namespace opt {
         return true;
     }
 
-#define PASSERT(_e_) if (!(_e_)) { TRACE("opt", display(tout, r);); SASSERT(_e_); }
+#define PASSERT(_e_) if (!(_e_)) { TRACE("opt1", display(tout, r); display(tout);); SASSERT(_e_); }
 
     bool model_based_opt::invariant(unsigned index, row const& r) {
         vector<var> const& vars = r.m_vars;
@@ -539,7 +539,7 @@ namespace opt {
         rational slack = (abs_src_c - rational::one()) * (abs_dst_c - rational::one());
         rational dst_val = dst.m_value - x_val*dst_c;
         rational src_val = src.m_value - x_val*src_c;
-        rational distance = src_c * dst_val + dst_c * src_val + slack; 
+        rational distance = abs_src_c * dst_val + abs_dst_c * src_val + slack; 
         bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one();
 
 #if 0
@@ -655,7 +655,10 @@ namespace opt {
 
     void model_based_opt::normalize(unsigned row_id) {
         row& r = m_rows[row_id];
-        if (r.m_vars.empty()) return;
+        if (r.m_vars.empty()) {
+            retire_row(row_id);
+            return;
+        }
         if (r.m_type == t_mod) return;
         rational g(abs(r.m_vars[0].m_coeff));
         bool all_int = g.is_int();
@@ -1092,6 +1095,7 @@ namespace opt {
         for (unsigned idx : mod_rows) {
             replace_var(idx, x, u);            
             SASSERT(invariant(idx, m_rows[idx]));
+            normalize(idx);
         }
         TRACE("opt1", display(tout << "tableau after replace x under mod\n"););
         //
@@ -1113,6 +1117,7 @@ namespace opt {
                 // x |-> D*y + u
                 replace_var(row_id, x, D, y, u);
                 visited.insert(row_id);
+                normalize(row_id);
             }
         }
         TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index ca3c01189..a85e95b57 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -777,7 +777,11 @@ namespace smt {
         IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
         bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
         bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
-        switch(m_params.m_arith_mode) {
+        auto mode = m_params.m_arith_mode;
+        if (m_logic == "QF_LIA") {
+            mode = AS_NEW_ARITH;
+        }
+        switch(mode) {
         case AS_NO_ARITH:
             m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
             break;
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 46b766bd4..eed4e4425 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -60,6 +60,7 @@ probe * mk_is_quasi_pb_probe() {
 // Create SMT solver that does not use cuts
 static tactic * mk_no_cut_smt_tactic(unsigned rs) {
     params_ref solver_p;
+    solver_p.set_sym(symbol("smt.logic"), symbol("QF_LIA")); // force smt_setup to use the new solver
     solver_p.set_uint("arith.branch_cut_ratio", 10000000);
     solver_p.set_uint("random_seed", rs);
     return annotate_tactic("no-cut-smt-tactic", using_params(mk_smt_tactic_using(false), solver_p));
@@ -209,15 +210,8 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
     params_ref quasi_pb_p;
     quasi_pb_p.set_uint("lia2pb_max_bits", 64);
     
-    params_ref no_cut_p;
-    no_cut_p.set_uint("arith.branch_cut_ratio", 10000000);
-
-
 
     tactic * st = using_params(and_then(preamble_st,
-#if 0
-                                        mk_smt_tactic()),
-#else
                                         or_else(mk_ilp_model_finder_tactic(m),
                                                 mk_pb_tactic(m),
                                                 and_then(fail_if_not(mk_is_quasi_pb_probe()), 
@@ -225,7 +219,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
                                                          mk_fail_if_undecided_tactic()),
                                                 mk_bounded_tactic(m),
                                                 mk_smt_tactic())),
-#endif
                                main_p);
 
     
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index ff083162d..b094a5b66 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -366,8 +366,6 @@ Notes:
             if (cmp == LE || cmp == EQ || cmp == LE_FULL) {
                 last = k + 1;
             }
-            bool full = cmp == LE_FULL || cmp == GE_FULL;
-
             literal_vector carry;
             for (unsigned i = 0; i < last; ++i) {
                 carry.push_back(ctx.mk_false());