diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index 3b0902160..4a87b4036 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -80,8 +80,9 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende
     
     if (!c().is_monic_var(j)) {
         c().insert_to_active_var_set(j);
-        // TODO: non-deterministic parameter evaluation
-        return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
+        nex* coeff_term = cn.mk_scalar(coeff);
+        nex* var_term = cn.mk_var(j);
+        return cn.mk_mul(coeff_term, var_term);
     }
     const monic& m = c().emons()[j];
     nex_creator::mul_factory mf(cn);
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 55862411e..9fb1a4d15 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -43,19 +43,29 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
         solve_eqs = mk_skip_tactic();
     }
     else {
-        // TODO: non-deterministic parameter evaluation
-        solve_eqs = when(mk_not(mk_has_pattern_probe()), mk_solve_eqs_tactic(m));
+        probe* has_pattern = mk_has_pattern_probe();
+        probe* no_pattern = mk_not(has_pattern);
+        tactic* solve_eqs_core = mk_solve_eqs_tactic(m);
+        solve_eqs = when(no_pattern, solve_eqs_core);
     }
  
     // remark: investigate if gaussian elimination is useful when patterns are not provided.
-    // TODO: non-deterministic parameter evaluation
-    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),
+    tactic* simplify1 = mk_simplify_tactic(m);
+    tactic* propagate = mk_propagate_values_tactic(m);
+    tactic* ctx_simplify = mk_ctx_simplify_tactic(m);
+    tactic* ctx_simplify_with_params = using_params(ctx_simplify, ctx_simp_p);
+    tactic* simplify2 = mk_simplify_tactic(m);
+    tactic* simplify_with_pull_ite = using_params(simplify2, pull_ite_p);
+    tactic* elim_unc = mk_elim_uncnstr_tactic(m);
+    tactic* simplify3 = mk_simplify_tactic(m);
+
+    return and_then(simplify1, 
+                    propagate,
+                    ctx_simplify_with_params,
+                    simplify_with_pull_ite,
                     solve_eqs,
-                    mk_elim_uncnstr_tactic(m),
-                    mk_simplify_tactic(m));    
+                    elim_unc,
+                    simplify3);    
 }
 
 static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
@@ -63,18 +73,21 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
 }
 
 tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
-    // TODO: non-deterministic parameter evaluation
-    tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
-                           mk_qe_lite_tactic(m, p),
-                           mk_smt_tactic(m));
+    tactic* preprocessor = mk_no_solve_eq_preprocessor(m);
+    tactic* qe = mk_qe_lite_tactic(m, p);
+    tactic* smt = mk_smt_tactic(m);
+    tactic * st = and_then(preprocessor,
+                           qe,
+                           smt);
     st->updt_params(p);
     return st;
 }
 
 tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) {
-    // TODO: non-deterministic parameter evaluation
-    tactic * st = and_then(mk_quant_preprocessor(m),
-                           mk_smt_tactic(m));
+    tactic* preprocessor = mk_quant_preprocessor(m);
+    tactic* smt = mk_smt_tactic(m);
+    tactic * st = and_then(preprocessor,
+                           smt);
     st->updt_params(p);
     return st;
 }
@@ -83,44 +96,59 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) {
     params_ref qi_p;
     qi_p.set_str("qi.cost", "0");
     TRACE(qi_cost, qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "<null>") << "\n";);
-    tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
-                           // TODO: non-deterministic parameter evaluation
-                           or_else(and_then(fail_if(mk_gt(mk_num_exprs_probe(), mk_const_probe(static_cast<double>(128)))),
-                                            using_params(mk_smt_tactic(m), qi_p),
-                                            mk_fail_if_undecided_tactic()),
-                                   mk_smt_tactic(m)));
+    tactic* preprocessor = mk_no_solve_eq_preprocessor(m);
+    probe* num_exprs = mk_num_exprs_probe();
+    probe* limit_probe = mk_const_probe(static_cast<double>(128));
+    probe* gt_probe = mk_gt(num_exprs, limit_probe);
+    tactic* fail_guard = fail_if(gt_probe);
+    tactic* smt_with_params = using_params(mk_smt_tactic(m), qi_p);
+    tactic* fail_undecided = mk_fail_if_undecided_tactic();
+    tactic* guarded_branch = and_then(fail_guard, smt_with_params, fail_undecided);
+    tactic* default_smt = mk_smt_tactic(m);
+    tactic* branch = or_else(guarded_branch, default_smt);
+    tactic * st = and_then(preprocessor, branch);
     st->updt_params(p);
     return st;
 }
 
 tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p) {
-    // TODO: non-deterministic parameter evaluation
-    tactic * st = and_then(mk_quant_preprocessor(m),
-                           mk_smt_tactic(m));
+    tactic* preprocessor = mk_quant_preprocessor(m);
+    tactic* smt = mk_smt_tactic(m);
+    tactic * st = and_then(preprocessor,
+                           smt);
     st->updt_params(p);
     return st;
 }
 
 tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
-    // TODO: non-deterministic parameter evaluation
-    tactic * st = and_then(mk_quant_preprocessor(m),
-                           mk_smt_tactic(m));
+    tactic* preprocessor = mk_quant_preprocessor(m);
+    tactic* smt = mk_smt_tactic(m);
+    tactic * st = and_then(preprocessor,
+                           smt);
     st->updt_params(p);
     return st;
 }
 
 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
-    // TODO: non-deterministic parameter evaluation
-    tactic * st = and_then(mk_quant_preprocessor(m),
-                           mk_qe_lite_tactic(m, p),
-                           // TODO: non-deterministic parameter evaluation
-                           cond(mk_has_quantifier_probe(), 
-                                // TODO: non-deterministic parameter evaluation
-                                cond(mk_is_lira_probe(),
-                                     // TODO: non-deterministic parameter evaluation
-                                     or_else(mk_qsat_tactic(m, p), mk_smt_tactic(m)),
-                                     mk_smt_tactic(m)),
-                                mk_smt_tactic(m)));
+    tactic* preprocessor = mk_quant_preprocessor(m);
+    tactic* qe = mk_qe_lite_tactic(m, p);
+
+    probe* has_quant_probe = mk_has_quantifier_probe();
+    probe* is_lira_probe = mk_is_lira_probe();
+
+    tactic* qsat = mk_qsat_tactic(m, p);
+    tactic* smt_for_qsat = mk_smt_tactic(m);
+    tactic* qsat_branch = or_else(qsat, smt_for_qsat);
+
+    tactic* smt_after_lira = mk_smt_tactic(m);
+    tactic* lira_branch = cond(is_lira_probe, qsat_branch, smt_after_lira);
+
+    tactic* smt_no_quant = mk_smt_tactic(m);
+    tactic* quant_branch = cond(has_quant_probe, lira_branch, smt_no_quant);
+
+    tactic * st = and_then(preprocessor,
+                           qe,
+                           quant_branch);
     st->updt_params(p);
     return st;
 }
@@ -132,4 +160,3 @@ tactic * mk_lia_tactic(ast_manager & m, params_ref const & p) {
 tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) {
     return mk_lra_tactic(m, p);
 }
-