diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 1cfc1f678..6f200680a 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -80,7 +80,7 @@ namespace q {
         unsigned num_patterns = q->get_num_patterns();
         for (unsigned i = 0; i < num_patterns; i++) 
             ensure_ground_enodes(q->get_pattern(i));
-        for (auto lit : c.m_lits) {
+        for (auto const& lit : c.m_lits) {
             ensure_ground_enodes(lit.lhs);
             ensure_ground_enodes(lit.rhs);
         }
@@ -186,7 +186,7 @@ namespace q {
 
     void ematch::init_watch(clause& c) {
         unsigned idx = c.index();
-        for (auto lit : c.m_lits) {
+        for (auto const& lit : c.m_lits) {
             if (!is_ground(lit.lhs))
                 init_watch(lit.lhs, idx);
             if (!is_ground(lit.rhs))
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 8673b6380..b8ebbd8a9 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -190,22 +190,14 @@ tactic * mk_preamble_tactic(ast_manager& m) {
     ctx_simp_p.set_uint("max_depth", 30);
     ctx_simp_p.set_uint("max_steps", 5000000);
 
-    params_ref lhs_p;
-    lhs_p.set_bool("arith_lhs", true);
-
-    tactic * preamble_st = and_then(mk_simplify_tactic(m),
-                                    mk_propagate_values_tactic(m),
-                                    using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
-                                    using_params(mk_simplify_tactic(m), pull_ite_p)
-                                    );
-
-    preamble_st = and_then(preamble_st,
-                           mk_solve_eqs_tactic(m),
-                           mk_elim_uncnstr_tactic(m),
-                           using_params(mk_simplify_tactic(m), lhs_p) 
-                           );
-
-    return preamble_st;
+    return
+        and_then(
+            mk_simplify_tactic(m),
+            mk_propagate_values_tactic(m),
+            using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
+            using_params(mk_simplify_tactic(m), pull_ite_p),
+            mk_solve_eqs_tactic(m),
+            mk_elim_uncnstr_tactic(m));
 }
 
 tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
@@ -215,23 +207,25 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
     main_p.set_bool("blast_distinct", true);
     main_p.set_uint("blast_distinct_threshold", 128);
     // main_p.set_bool("push_ite_arith", true);
-    
-
-
+   
     params_ref quasi_pb_p;
     quasi_pb_p.set_uint("lia2pb_max_bits", 64);
-    
-    tactic * preamble_st = mk_preamble_tactic(m);
 
-    tactic * st = using_params(and_then(preamble_st,
-                                        or_else(mk_ilp_model_finder_tactic(m),
-                                                mk_pb_tactic(m),
-                                                and_then(fail_if_not(mk_is_quasi_pb_probe()), 
-                                                         using_params(mk_lia2sat_tactic(m), quasi_pb_p),
-                                                         mk_fail_if_undecided_tactic()),
-                                                mk_bounded_tactic(m),
-                                                mk_smt_tactic(m))),
-                               main_p);
+    params_ref lhs_p;
+    lhs_p.set_bool("arith_lhs", true);
+
+    tactic* st = using_params(
+        and_then(
+            mk_preamble_tactic(m),
+            using_params(mk_simplify_tactic(m), lhs_p),
+            or_else(mk_ilp_model_finder_tactic(m),
+                mk_pb_tactic(m),
+                and_then(fail_if_not(mk_is_quasi_pb_probe()),
+                    using_params(mk_lia2sat_tactic(m), quasi_pb_p),
+                    mk_fail_if_undecided_tactic()),
+                mk_bounded_tactic(m),
+                mk_smt_tactic(m))),
+        main_p);
 
     
     st->updt_params(p);