diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp
index af96c2106..06cee481b 100644
--- a/src/nlsat/tactic/goal2nlsat.cpp
+++ b/src/nlsat/tactic/goal2nlsat.cpp
@@ -125,8 +125,9 @@ struct goal2nlsat::imp {
         m_qm.div(lcm, d2, d2);
         m_qm.neg(d2);
         polynomial_ref p(m_pm);
-        // TODO: non-deterministic parameter evaluation
-        p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2);
+        polynomial::monomial * unit1 = m_pm.mk_unit();
+        polynomial::monomial * unit2 = m_pm.mk_unit();
+        p = m_pm.addmul(d1, unit1, p1, d2, unit2, p2);
         TRACE(goal2nlsat_bug, tout << mk_pp(f, m) << " p: " << p << "\nk: " << k << "\n";);
         if (is_const(p)) {
             int sign;
@@ -444,4 +445,3 @@ expr_ref nlsat2goal::operator()(nlsat::solver& s, u_map<expr*> const& b2a, u_map
     return (*m_imp)(s, b2a, x2t, l);
 }
 
-
diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
index 930ce0b21..5a983b0bd 100644
--- a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
+++ b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
@@ -42,30 +42,47 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
     else
         factor = mk_skip_tactic();
 
-    return and_then(
-        mk_report_verbose_tactic("(qfnra-nlsat-tactic)", 10),
-        // TODO: non-deterministic parameter evaluation
-        and_then(using_params(mk_simplify_tactic(m, p),
-                              main_p),
-                 using_params(mk_purify_arith_tactic(m, p),
-                              purify_p),
-                 mk_propagate_values_tactic(m, p),
-                 mk_solve_eqs_tactic(m, p),
-                 mk_elim_uncnstr_tactic(m, p),
-                 mk_elim_term_ite_tactic(m, p),
-                 using_params(mk_purify_arith_tactic(m, p),
-                              purify_p)),
-        // TODO: non-deterministic parameter evaluation
-        and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
-            factor,
-            mk_solve_eqs_tactic(m, p),
-            using_params(mk_purify_arith_tactic(m, p),
-                         purify_p),
-            using_params(mk_simplify_tactic(m, p),
-                         main_p),
-            mk_tseitin_cnf_core_tactic(m, p),
-            using_params(mk_simplify_tactic(m, p),
-                         main_p),
-            mk_nlsat_tactic(m, p)));
-}
+    tactic * report = mk_report_verbose_tactic("(qfnra-nlsat-tactic)", 10);
 
+    tactic * simplify_base1 = mk_simplify_tactic(m, p);
+    tactic * simplify_main1 = using_params(simplify_base1, main_p);
+    tactic * purify_base1 = mk_purify_arith_tactic(m, p);
+    tactic * purify_main1 = using_params(purify_base1, purify_p);
+    tactic * propagate_values = mk_propagate_values_tactic(m, p);
+    tactic * solve_eqs1 = mk_solve_eqs_tactic(m, p);
+    tactic * elim_unc = mk_elim_uncnstr_tactic(m, p);
+    tactic * elim_term_ite = mk_elim_term_ite_tactic(m, p);
+    tactic * purify_base2 = mk_purify_arith_tactic(m, p);
+    tactic * purify_main2 = using_params(purify_base2, purify_p);
+
+    tactic * preprocessing = and_then(
+        simplify_main1,
+        purify_main1,
+        propagate_values,
+        solve_eqs1,
+        elim_unc,
+        elim_term_ite,
+        purify_main2);
+
+    tactic * solve_eqs2 = mk_solve_eqs_tactic(m, p);
+    tactic * purify_base3 = mk_purify_arith_tactic(m, p);
+    tactic * purify_main3 = using_params(purify_base3, purify_p);
+    tactic * simplify_base2 = mk_simplify_tactic(m, p);
+    tactic * simplify_main2 = using_params(simplify_base2, main_p);
+    tactic * tseitin = mk_tseitin_cnf_core_tactic(m, p);
+    tactic * simplify_base3 = mk_simplify_tactic(m, p);
+    tactic * simplify_main3 = using_params(simplify_base3, main_p);
+    tactic * nlsat = mk_nlsat_tactic(m, p);
+
+    tactic * post = and_then(
+        /* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
+        factor,
+        solve_eqs2,
+        purify_main3,
+        simplify_main2,
+        tseitin,
+        simplify_main3,
+        nlsat);
+
+    return and_then(report, preprocessing, post);
+}
diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp
index db9474a4a..5b78038dd 100644
--- a/src/tactic/arith/bv2real_rewriter.cpp
+++ b/src/tactic/arith/bv2real_rewriter.cpp
@@ -585,8 +585,9 @@ br_status bv2real_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result)
         u().align_divisors(s1, s2, t1, t2, d1, d2);
         u().align_sizes(s1, t1);
         u().align_sizes(s2, t2);
-        // TODO: non-deterministic parameter evaluation
-        if (u().mk_bv2real(m().mk_ite(c, s1, t1), m().mk_ite(c, s2, t2), d1, r1, result)) {
+        expr_ref ite_s1(m().mk_ite(c, s1, t1), m());
+        expr_ref ite_s2(m().mk_ite(c, s2, t2), m());
+        if (u().mk_bv2real(ite_s1.get(), ite_s2.get(), d1, r1, result)) {
             return BR_DONE;
         }
     }
@@ -615,8 +616,9 @@ br_status bv2real_rewriter::mk_uminus(expr * s, expr_ref & result) {
     if (u().is_bv2real(s, s1, s2, d1, r1)) {
         s1 = u().mk_extend(1, s1);
         s2 = u().mk_extend(1, s2);
-        // TODO: non-deterministic parameter evaluation
-        if (u().mk_bv2real(m_bv.mk_bv_neg(s1), m_bv.mk_bv_neg(s2), d1, r1, result)) {
+        expr_ref neg_s1(m_bv.mk_bv_neg(s1), m());
+        expr_ref neg_s2(m_bv.mk_bv_neg(s2), m());
+        if (u().mk_bv2real(neg_s1.get(), neg_s2.get(), d1, r1, result)) {
             return BR_DONE;
         }
     }
@@ -638,8 +640,9 @@ br_status bv2real_rewriter::mk_add(expr* s, expr* t, expr_ref& result) {
     rational d1, d2, r1, r2;
     if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
         u().align_divisors(s1, s2, t1, t2, d1, d2);
-        // TODO: non-deterministic parameter evaluation
-        if (u().mk_bv2real(u().mk_bv_add(s1, t1), u().mk_bv_add(t2, s2), d1, r1, result)) {
+        expr_ref sum1(u().mk_bv_add(s1, t1), m());
+        expr_ref sum2(u().mk_bv_add(t2, s2), m());
+        if (u().mk_bv2real(sum1.get(), sum2.get(), d1, r1, result)) {
             return BR_DONE;
         }
     }
@@ -699,8 +702,9 @@ br_status bv2real_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
     rational d1, d2, r1, r2;
     if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
         u().align_divisors(s1, s2, t1, t2, d1, d2);
-        // TODO: non-deterministic parameter evaluation
-        if (u().mk_bv2real(u().mk_bv_sub(s1, t1), u().mk_bv_sub(s2, t2), d1, r1, result)) {
+        expr_ref diff1(u().mk_bv_sub(s1, t1), m());
+        expr_ref diff2(u().mk_bv_sub(s2, t2), m());
+        if (u().mk_bv2real(diff1.get(), diff2.get(), d1, r1, result)) {
             return BR_DONE;
         }
     }
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 48acb09c3..1f1347ff6 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -157,8 +157,10 @@ class factor_tactic : public tactic {
                 }
             }
             else {
-                // TODO: non-deterministic parameter evaluation
-                args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.data()), mk_zero_for(odd_factors[0])));
+                expr_ref odd_product(mk_mul(odd_factors.size(), odd_factors.data()), m);
+                expr* zero = mk_zero_for(odd_factors[0]);
+                expr_ref comparison(m.mk_app(m_util.get_family_id(), k, odd_product, zero), m);
+                args.push_back(comparison);
             }
             SASSERT(!args.empty());
             if (args.size() == 1)
@@ -186,11 +188,12 @@ class factor_tactic : public tactic {
             scoped_mpz lcm(m_qm);
             m_qm.lcm(d1, d2, lcm);
             m_qm.div(lcm, d1, d1);
-            m_qm.div(lcm, d2, d2);
-            m_qm.neg(d2);
-            polynomial_ref p(m_pm);
-            // TODO: non-deterministic parameter evaluation
-            p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2);
+        m_qm.div(lcm, d2, d2);
+        m_qm.neg(d2);
+        polynomial_ref p(m_pm);
+        polynomial::monomial* unit1 = m_pm.mk_unit();
+        polynomial::monomial* unit2 = m_pm.mk_unit();
+        p = m_pm.addmul(d1, unit1, p1, d2, unit2, p2);
             if (is_const(p))
                 return BR_FAILED;
             polynomial::factors fs(m_pm);
@@ -337,4 +340,3 @@ tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) {
     return clean(alloc(factor_tactic, m, p));
 }
 
-
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 497ca7924..855446b05 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -244,23 +244,35 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p, bool add_nnf)
     // conservative gaussian elimination. 
     gaussian_p.set_uint("gaussian_max_occs", 2); 
 
-    return and_then(
-        // TODO: non-deterministic parameter evaluation
-        and_then(mk_simplify_tactic(m, p),
-            mk_propagate_values_tactic(m),
-            using_params(mk_solve_eqs_tactic(m), gaussian_p),
-            mk_elim_uncnstr_tactic(m),
-            mk_bv_size_reduction_tactic(m),
-            using_params(mk_simplify_tactic(m), simp2_p)),
-        using_params(mk_simplify_tactic(m), hoist_p),
-        mk_max_bv_sharing_tactic(m),
-        add_nnf ? mk_nnf_tactic(m, p) : mk_skip_tactic()
-    );
+    tactic* simplify_primary = mk_simplify_tactic(m, p);
+    tactic* propagate_values = mk_propagate_values_tactic(m);
+    tactic* solve_eqs_base = mk_solve_eqs_tactic(m);
+    tactic* solve_eqs_gaussian = using_params(solve_eqs_base, gaussian_p);
+    tactic* elim_unc = mk_elim_uncnstr_tactic(m);
+    tactic* size_reduction = mk_bv_size_reduction_tactic(m);
+    tactic* simplify_secondary_base = mk_simplify_tactic(m);
+    tactic* simplify_secondary = using_params(simplify_secondary_base, simp2_p);
+
+    tactic* inner = and_then(
+        simplify_primary,
+        propagate_values,
+        solve_eqs_gaussian,
+        elim_unc,
+        size_reduction,
+        simplify_secondary);
+
+    tactic* simplify_hoist_base = mk_simplify_tactic(m);
+    tactic* simplify_hoist = using_params(simplify_hoist_base, hoist_p);
+    tactic* max_sharing = mk_max_bv_sharing_tactic(m);
+    tactic* nnf = add_nnf ? mk_nnf_tactic(m, p) : mk_skip_tactic();
+
+    return and_then(inner, simplify_hoist, max_sharing, nnf);
 }
 
 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
-    // TODO: non-deterministic parameter evaluation
-    tactic * t = and_then(mk_preamble(m, p, true), mk_sls_tactic(m, p));
+    tactic * preamble = mk_preamble(m, p, true);
+    tactic * sls = mk_sls_tactic(m, p);
+    tactic * t = and_then(preamble, sls);
     t->updt_params(p);
     return t;
 }