diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 4b9c6d246..1a4df0fb9 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1295,8 +1295,9 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
     } 
     if (get_divides(arg1, arg2, result)) { 
         expr_ref zero(m_util.mk_int(0), m); 
-        // TODO: non-deterministic parameter evaluation
-        result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
+        expr_ref eq_zero(m.mk_eq(zero, arg2), m);
+        expr_ref div_expr(m_util.mk_idiv(arg1, zero), m);
+        result = m.mk_ite(eq_zero, div_expr, result);
         return BR_REWRITE_FULL; 
     }
 #if 0
@@ -1429,8 +1430,9 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
 
     if (arg1 == arg2 && !is_num2) {
         expr_ref zero(m_util.mk_int(0), m);
-        // TODO: non-deterministic parameter evaluation
-        result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero);
+        expr_ref eq_zero(m.mk_eq(arg2, zero), m);
+        expr_ref mod_zero(m_util.mk_mod(zero, zero), m);
+        result = m.mk_ite(eq_zero, mod_zero, zero);
         return BR_DONE;
     }
 
@@ -1769,10 +1771,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
 
     if (is_num_y && y.is_minus_one()) {        
         result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1));
-        // TODO: non-deterministic parameter evaluation
-        result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
-                            m_util.mk_real(0),
-                            result);        
+        expr_ref zero_term(m_util.mk_numeral(rational(0), m_util.is_int(arg1)), m);
+        expr_ref eq_zero(m.mk_eq(arg1, zero_term), m);
+        expr_ref zero_real(m_util.mk_real(0), m);
+        result = m.mk_ite(eq_zero, zero_real, result);        
         return BR_REWRITE2;
     }
 
@@ -1780,10 +1782,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
         // (^ t -k) --> (^ (/ 1 t) k)
         result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1),
                                  m_util.mk_numeral(-y, false));
-        // TODO: non-deterministic parameter evaluation
-        result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
-                            m_util.mk_real(0),
-                            result);
+        expr_ref zero_term(m_util.mk_numeral(rational(0), m_util.is_int(arg1)), m);
+        expr_ref eq_zero(m.mk_eq(arg1, zero_term), m);
+        expr_ref zero_real(m_util.mk_real(0), m);
+        result = m.mk_ite(eq_zero, zero_real, result);
         return BR_REWRITE3;
     }
 
diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
index 43131c2c8..ef75cec4a 100644
--- a/src/ast/rewriter/bv2int_translator.cpp
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -320,8 +320,9 @@ void bv2int_translator::translate_bv(app* e) {
     case OP_BUDIV:
     case OP_BUDIV_I: {
         expr* x = umod(e, 0), * y = umod(e, 1);
-        // TODO: non-deterministic parameter evaluation
-        r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
+        expr_ref minus_one(a.mk_int(-1), m);
+        expr_ref div_expr(a.mk_idiv(x, y), m);
+        r = if_eq(y, 0, minus_one.get(), div_expr.get());
         break;
     }
     case OP_BUMUL_NO_OVFL: {
@@ -399,10 +400,12 @@ void bv2int_translator::translate_bv(app* e) {
         unsigned sz = bv.get_bv_size(e);
         IF_VERBOSE(4, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
         r = arg(0);
+        expr_ref two(a.mk_int(2), m);
         for (unsigned i = 1; i < args.size(); ++i) {
             expr* q = arg(i);
-            // TODO: non-deterministic parameter evaluation
-            r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
+            expr_ref band_expr(a.mk_band(sz, r, q), m);
+            expr_ref mul_expr(mul(two.get(), band_expr.get()), m);
+            r = a.mk_sub(add(r, q), mul_expr.get());
         }
         if (e->get_decl_kind() == OP_BXNOR)
             r = bnot(r);
@@ -440,8 +443,9 @@ void bv2int_translator::translate_bv(app* e) {
         expr* lhs = umod(bv_expr, 0);
         expr* rhs = umod(bv_expr, 1);
         expr* eq = m.mk_eq(lhs, rhs);
-        // TODO: non-deterministic parameter evaluation
-        r = m.mk_ite(eq, a.mk_int(1), a.mk_int(0));
+        expr_ref one(a.mk_int(1), m);
+        expr_ref zero(a.mk_int(0), m);
+        r = m.mk_ite(eq, one.get(), zero.get());
         break;
     }
     case OP_BSMOD_I:
@@ -460,7 +464,6 @@ void bv2int_translator::translate_bv(app* e) {
         r = a.mk_uminus(u);
         expr* pos_neg = m.mk_and(m.mk_not(signx), signy);
         expr* neg_pos = m.mk_and(signx, m.mk_not(signy));
-        // TODO: non-deterministic parameter evaluation
         expr* pos_pos = m.mk_and(m.mk_not(signx), m.mk_not(signy));
         expr_ref add_u_y(m);
         add_u_y = add(u, y);
@@ -489,9 +492,10 @@ void bv2int_translator::translate_bv(app* e) {
         y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
         expr* d = a.mk_idiv(x, y);
         r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
-        // TODO: non-deterministic parameter evaluation
-        expr* zero_case = m.mk_ite(signx, a.mk_int(1), a.mk_int(-1));
-        r = if_eq(y, 0, zero_case, r);
+        expr_ref pos_case(a.mk_int(1), m);
+        expr_ref neg_case(a.mk_int(-1), m);
+        expr_ref zero_case(m.mk_ite(signx, pos_case.get(), neg_case.get()), m);
+        r = if_eq(y, 0, zero_case.get(), r);
         break;
     }
     case OP_BSREM_I:
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 5dc48a5f7..2ef539c97 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -945,10 +945,11 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
     if (m_util.is_bv_shl(arg1, x, y)) {
         expr_ref sum(m_util.mk_bv_add(y, arg2), m);
         expr_ref cond(m_util.mk_ule(y, sum), m);
-        // TODO: non-deterministic parameter evaluation
+        expr_ref shl_expr(m_util.mk_bv_shl(x, sum), m);
+        expr* zero = mk_zero(bv_size);
         result = m.mk_ite(cond, 
-                            m_util.mk_bv_shl(x, sum),
-                            mk_zero(bv_size));
+                          shl_expr,
+                          zero);
         return BR_REWRITE3;
     }
 
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index 2d91c489b..71654508e 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -170,8 +170,9 @@ struct enum2bv_rewriter::imp {
                 ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s);
                 f_def = m.mk_const(cs[nc-1]);
                 for (unsigned i = nc - 1; i-- > 0; ) {
-                    // TODO: non-deterministic parameter evaluation
-                    f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def);
+                    expr_ref eq_expr(m.mk_eq(result, value2bv(i, s)), m);
+                    expr_ref ctor_expr(m.mk_const(cs[i]), m);
+                    f_def = m.mk_ite(eq_expr, ctor_expr, f_def);
                 }
                 m_imp.m_enum2def.insert(f, f_def);
                 m_imp.m_enum2bv.insert(f, f_fresh);
diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 364b66b26..e0400540a 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -747,34 +747,47 @@ namespace seq {
         VERIFY (seq.str.is_stoi(e, _s));
         expr_ref s(_s, m);
         m_rewrite(s);
-        // TODO: non-deterministic parameter evaluation
         auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; 
         auto digit = [&](unsigned j) { return mk_digit2int(mk_nth(s, j)); };
         auto is_digit_ = [&](unsigned j) { return is_digit(mk_nth(s, j)); };
         expr_ref len = mk_len(s);
         expr_ref ge0 = mk_ge(e, 0);
         expr_ref lek = mk_le(len, k);
-        add_clause(~lek, mk_eq(e, stoi2(k-1)));                                    // len(s) <= k  => stoi(s) = stoi(s, k-1)
-        // TODO: non-deterministic parameter evaluation
-        add_clause(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0)));       // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
-        // TODO: non-deterministic parameter evaluation
-        add_clause(mk_le(len, 0), is_digit_(0),  mk_eq(stoi2(0), a.mk_int(-1)));   // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
+        expr_ref stoi_k_1(stoi2(k-1), m);
+        add_clause(~lek, mk_eq(e, stoi_k_1));                                    // len(s) <= k  => stoi(s) = stoi(s, k-1)
+
+        expr_ref len_le0(mk_le(len, 0), m);
+        expr_ref digit0(digit(0), m);
+        expr_ref is_digit0(is_digit_(0), m);
+        expr_ref not_is_digit0(m.mk_not(is_digit0), m);
+        expr_ref stoi0(stoi2(0), m);
+        add_clause(len_le0, not_is_digit0, mk_eq(stoi0, digit0));       // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
+        expr_ref minus_one_int(a.mk_int(-1), m);
+        add_clause(len_le0, is_digit0,  mk_eq(stoi0, minus_one_int));   // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
         for (unsigned i = 1; i < k; ++i) {
 
             // len(s) <= i => stoi(s, i) = stoi(s, i - 1)
 
-            add_clause(~mk_le(len, i),  mk_eq(stoi2(i), stoi2(i-1)));
+            expr_ref len_le_i(mk_le(len, i), m);
+            expr_ref stoi_i(stoi2(i), m);
+            expr_ref stoi_prev(stoi2(i-1), m);
+            add_clause(~len_le_i,  mk_eq(stoi_i, stoi_prev));
 
             // len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(i)
             // len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1
             // len(s) > i, ~is_digit(nth(s, i)) => stoi(s, i) = -1
 
-            // TODO: non-deterministic parameter evaluation
-            add_clause(mk_le(len, i), ~mk_ge(stoi2(i-1), 0), ~is_digit_(i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i))));
-            // TODO: non-deterministic parameter evaluation
-            add_clause(mk_le(len, i), is_digit_(i),                         mk_eq(stoi2(i), a.mk_int(-1)));
-            // TODO: non-deterministic parameter evaluation
-            add_clause(mk_le(len, i), mk_ge(stoi2(i-1), 0),                 mk_eq(stoi2(i), a.mk_int(-1)));
+            expr_ref ge_stoi_prev(mk_ge(stoi_prev, 0), m);
+            expr_ref not_ge_stoi_prev(m.mk_not(ge_stoi_prev), m);
+            expr_ref is_digit_i(is_digit_(i), m);
+            expr_ref not_is_digit_i(m.mk_not(is_digit_i), m);
+            expr_ref digit_i(digit(i), m);
+            expr_ref ten(a.mk_int(10), m);
+            expr_ref mul_expr(a.mk_mul(ten, stoi_prev), m);
+            expr_ref sum_expr(a.mk_add(mul_expr, digit_i), m);
+            add_clause(len_le_i, not_ge_stoi_prev, not_is_digit_i, mk_eq(stoi_i, sum_expr));
+            add_clause(len_le_i, is_digit_i, mk_eq(stoi_i, minus_one_int));
+            add_clause(len_le_i, ge_stoi_prev, mk_eq(stoi_i, minus_one_int));
 
             // stoi(s) >= 0, i < len(s) => is_digit(nth(s, i))
 
@@ -912,17 +925,21 @@ namespace seq {
         expr* e = nullptr;
         VERIFY(seq.str.is_itos(s, e));
         expr_ref len = mk_len(s);
-        // TODO: non-deterministic parameter evaluation
-        add_clause(mk_ge(e, 10), mk_le(len, 1));
-        // TODO: non-deterministic parameter evaluation
-        add_clause(mk_le(e, -1), mk_ge(len, 1));
+        expr_ref ge_e_10(mk_ge(e, 10), m);
+        expr_ref len_le1(mk_le(len, 1), m);
+        add_clause(ge_e_10, len_le1);
+        expr_ref le_e_minus1(mk_le(e, -1), m);
+        expr_ref len_ge1(mk_ge(len, 1), m);
+        add_clause(le_e_minus1, len_ge1);
         rational lo(1);
         for (unsigned i = 1; i <= k; ++i) {
             lo *= rational(10);
-            // TODO: non-deterministic parameter evaluation
-            add_clause(mk_ge(e, lo), mk_le(len, i));
-            // TODO: non-deterministic parameter evaluation
-            add_clause(mk_le(e, lo - 1), mk_ge(len, i + 1));
+            expr_ref ge_e_lo(mk_ge(e, lo), m);
+            expr_ref len_le_i(mk_le(len, i), m);
+            add_clause(ge_e_lo, len_le_i);
+            expr_ref le_e_lo_minus(mk_le(e, lo - 1), m);
+            expr_ref len_ge_ip1(mk_ge(len, i + 1), m);
+            add_clause(le_e_lo_minus, len_ge_ip1);
         }
     }
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 4ba515d2c..ee01c5d36 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1640,13 +1640,17 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
             return BR_DONE;
         }
         break;
-    case same_length_c:
-        result = m().mk_ite(m_autil.mk_le(c, minus_one()), minus_one(), 
-                            // TODO: non-deterministic parameter evaluation
-                            m().mk_ite(m().mk_eq(c, zero()), 
-                                       m().mk_ite(m().mk_eq(a, b), zero(), minus_one()),
-                                       minus_one()));
+    case same_length_c: {
+        expr* zero_ptr = zero();
+        expr* minus_one_ptr = minus_one();
+        expr* cond_le = m_autil.mk_le(c, minus_one_ptr);
+        expr* cond_eq_c = m().mk_eq(c, zero_ptr);
+        expr* cond_eq_ab = m().mk_eq(a, b);
+        expr* inner = m().mk_ite(cond_eq_ab, zero_ptr, minus_one_ptr);
+        expr* middle = m().mk_ite(cond_eq_c, inner, minus_one_ptr);
+        result = m().mk_ite(cond_le, minus_one_ptr, middle);
         return BR_REWRITE_FULL;
+    }
     default:
         break;
     }
@@ -2996,8 +3000,12 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
             else if (neq_char(e, h))
                 result = nothing();
             else
-                // TODO: non-deterministic parameter evaluation
-                result = re().mk_ite_simplify(m().mk_eq(e, h), re().mk_to_re(t), nothing());
+            {
+                expr_ref cond(m().mk_eq(e, h), m());
+                expr_ref to_re_expr(re().mk_to_re(t), m());
+                expr_ref nothing_expr = nothing();
+                result = re().mk_ite_simplify(cond, to_re_expr, nothing_expr);
+            }
         }
         else {
             // observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first
@@ -4069,8 +4077,9 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence
             // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else []))
             hd = mk_seq_first(r1);
-            // TODO: non-deterministic parameter evaluation
-            m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
+            expr_ref not_empty(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m());
+            expr_ref eq_head(m().mk_eq(hd, ele), m());
+            m_br.mk_and(not_empty, eq_head, result);
             tl = re().mk_to_re(mk_seq_rest(r1));
             return re_and(result, tl);
         }
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index cab60dc7e..de4001d11 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -258,25 +258,25 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     template<bool SWAP>
     br_status pull_ite_core(func_decl * p, app * ite, app * value, expr_ref & result) {
         if (m().is_eq(p)) {
-            // TODO: non-deterministic parameter evaluation
-            result = m().mk_ite(ite->get_arg(0),
-                                mk_eq_value(ite->get_arg(1), value),
-                                mk_eq_value(ite->get_arg(2), value));
+            expr* cond = ite->get_arg(0);
+            expr* then_branch = mk_eq_value(ite->get_arg(1), value);
+            expr* else_branch = mk_eq_value(ite->get_arg(2), value);
+            result = m().mk_ite(cond, then_branch, else_branch);
             return BR_REWRITE2;
         }
         else {
             if (SWAP) {
-                // TODO: non-deterministic parameter evaluation
-                result = m().mk_ite(ite->get_arg(0),
-                                    m().mk_app(p, value, ite->get_arg(1)),
-                                    m().mk_app(p, value, ite->get_arg(2)));
+                expr* cond = ite->get_arg(0);
+                expr* then_branch = m().mk_app(p, value, ite->get_arg(1));
+                expr* else_branch = m().mk_app(p, value, ite->get_arg(2));
+                result = m().mk_ite(cond, then_branch, else_branch);
                 return BR_REWRITE2;
             }
             else {
-                // TODO: non-deterministic parameter evaluation
-                result = m().mk_ite(ite->get_arg(0),
-                                    m().mk_app(p, ite->get_arg(1), value),
-                                    m().mk_app(p, ite->get_arg(2), value));
+                expr* cond = ite->get_arg(0);
+                expr* then_branch = m().mk_app(p, ite->get_arg(1), value);
+                expr* else_branch = m().mk_app(p, ite->get_arg(2), value);
+                result = m().mk_ite(cond, then_branch, else_branch);
                 return BR_REWRITE2;
             }
         }
@@ -320,10 +320,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                     return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
                 if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) {
                     // (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2))
-                    // TODO: non-deterministic parameter evaluation
-                    result = m().mk_ite(to_app(args[0])->get_arg(0),
-                                        m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1)),
-                                        m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2)));
+                    expr* cond = to_app(args[0])->get_arg(0);
+                    expr* then_branch = m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1));
+                    expr* else_branch = m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2));
+                    result = m().mk_ite(cond,
+                                        then_branch,
+                                        else_branch);
                     return BR_REWRITE2;
                 }
             }
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 4f187b1e6..73b4d5408 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -714,9 +714,11 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
     m_extend_lit0(m), m_extend_lit(m),
     m_all_init(false), m_has_quantified_frame(false)
 {
-    // TODO: non-deterministic parameter evaluation
-    m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(),
-                     ctx.get_params(), head->get_name());
+    solver* solver0 = ctx.mk_solver0();
+    solver* solver1 = ctx.mk_solver1();
+    auto const& params = ctx.get_params();
+    m_solver = alloc(prop_solver, m, solver0, solver1,
+                     params, head->get_name());
     init_sig ();
 
     m_extend_lit = mk_extend_lit();
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 3b20a7865..c870e3aca 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -751,8 +751,9 @@ namespace arith {
         reset_evidence();
         m_explanation.clear();
         auto& dm = lp().dep_manager();
-        // TODO: non-deterministic parameter evaluation
-        auto* d = dm.mk_join(dm.mk_join(ci1, ci2), dm.mk_join(ci3, ci4));
+        auto* join12 = dm.mk_join(ci1, ci2);
+        auto* join34 = dm.mk_join(ci3, ci4);
+        auto* d = dm.mk_join(join12, join34);
         for (auto ci : lp().flatten(d))
             consume(rational::one(), ci);
         enode* x = var2enode(v1);
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index eef3690ef..c31ce7805 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -487,8 +487,9 @@ namespace smt {
         expr_ref emp(re().mk_empty(r->get_sort()), m);
         expr_ref n(m.mk_fresh_const("re.char", seq_sort), m);
         expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n);
-        // TODO: non-deterministic parameter evaluation
-        th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty));
+        literal eq_lit = th.mk_eq(r1, r2, false);
+        literal non_empty_lit = th.mk_literal(is_non_empty);
+        th.add_axiom(eq_lit, non_empty_lit);
     }
 
     bool seq_regex::is_member(expr* r, expr* u) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index fc43c83fd..f9418d8de 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -573,8 +573,8 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
 void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
     m_sk.decompose(e, head, tail);
     add_axiom(~mk_eq_empty(e), mk_eq_empty(tail));;
-    // TODO: non-deterministic parameter evaluation
-    add_axiom(mk_eq_empty(e), mk_eq(e, mk_concat(head, tail), false));
+    expr_ref concat_expr(mk_concat(head, tail), m);
+    add_axiom(mk_eq_empty(e), mk_eq(e, concat_expr, false));
 }
 
 /*
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 655c4ab50..9243e01d0 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -171,8 +171,11 @@ namespace smt {
         struct var_value_eq {
             theory_utvpi & m_th;
             var_value_eq(theory_utvpi & th):m_th(th) {}
-            // TODO: non-deterministic parameter evaluation
-            bool operator()(theory_var v1, theory_var v2) const { return m_th.mk_value(v1, false) == m_th.mk_value(v2, false) && m_th.is_int(v1) == m_th.is_int(v2); }
+            bool operator()(theory_var v1, theory_var v2) const {
+                auto value1 = m_th.mk_value(v1, false);
+                auto value2 = m_th.mk_value(v2, false);
+                return value1 == value2 && m_th.is_int(v1) == m_th.is_int(v2);
+            }
         };
 
         typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
@@ -363,4 +366,3 @@ namespace smt {
 
 
 
-
diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp
index 2b6d0d5d7..096bbbca3 100644
--- a/src/tactic/core/special_relations_tactic.cpp
+++ b/src/tactic/core/special_relations_tactic.cpp
@@ -77,11 +77,11 @@ void special_relations_tactic::initialize() {
     expr* pats[1] = { pat };
     expr* pats0[1] = { pat0 };
 
-    // TODO: non-deterministic parameter evaluation
     fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz);
     q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
     register_pattern(m_pm.initialize(q), sr_transitive);
-    fml = m.mk_or(mk_not(Rxy & Ryz), Rxz);
+    expr_ref trans_cond(mk_not(Rxy & Ryz), m);
+    fml = m.mk_or(trans_cond, Rxz);
     q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
     register_pattern(m_pm.initialize(q), sr_transitive);
 
@@ -92,7 +92,8 @@ void special_relations_tactic::initialize() {
     fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y));
     q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
     register_pattern(m_pm.initialize(q), sr_antisymmetric);
-    fml = m.mk_or(mk_not(Rxy & Ryx), m.mk_eq(x, y));
+    expr_ref antisym_cond(mk_not(Rxy & Ryx), m);
+    fml = m.mk_or(antisym_cond, m.mk_eq(x, y));
     q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
     register_pattern(m_pm.initialize(q), sr_antisymmetric);
 
@@ -179,4 +180,3 @@ void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer &
 tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p) {
     return alloc(special_relations_tactic, m, p);
 }
-
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 07b88a02b..5a74b6e29 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -86,15 +86,21 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
     // dynamic psm seems to work well.
     solver_p.set_sym("gc", symbol("dyn_psm"));
     
-    // TODO: non-deterministic parameter evaluation
-    return using_params(and_then(mk_simplify_tactic(m),
-                                 mk_propagate_values_tactic(m),
-                                 mk_solve_eqs_tactic(m),
-                                 mk_max_bv_sharing_tactic(m),
-                                 mk_bit_blaster_tactic(m),
-                                 mk_aig_tactic(),
-                                 mk_sat_tactic(m, solver_p)),
-                        solver_p);
+    tactic* simplify = mk_simplify_tactic(m);
+    tactic* propagate = mk_propagate_values_tactic(m);
+    tactic* solve_eqs = mk_solve_eqs_tactic(m);
+    tactic* max_sharing = mk_max_bv_sharing_tactic(m);
+    tactic* bit_blaster = mk_bit_blaster_tactic(m);
+    tactic* aig = mk_aig_tactic();
+    tactic* sat = mk_sat_tactic(m, solver_p);
+    tactic* core = and_then(simplify,
+                            propagate,
+                            solve_eqs,
+                            max_sharing,
+                            bit_blaster,
+                            aig,
+                            sat);
+    return using_params(core, solver_p);
 }
 
 #define SMALL_SIZE 80000
@@ -106,19 +112,31 @@ static tactic * mk_pb_tactic(ast_manager & m) {
     params_ref bv2sat_p;
     bv2sat_p.set_bool("ite_extra", true);
     
-    return annotate_tactic(
-        "pb-tactic",
-        and_then(fail_if_not(mk_is_pb_probe()),
-                 fail_if(mk_produce_proofs_probe()),
-                 fail_if(mk_produce_unsat_cores_probe()),
-                 // TODO: non-deterministic parameter evaluation
-                 or_else(and_then(fail_if(mk_ge(mk_num_exprs_probe(), mk_const_probe(SMALL_SIZE))),
-                                  fail_if_not(mk_is_ilp_probe()),
-                                  // try_for(mk_mip_tactic(m), 8000),
-                                  mk_fail_if_undecided_tactic()),
-                         and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
-                                  fail_if_not(mk_is_qfbv_probe()),
-                                  using_params(mk_bv2sat_tactic(m), bv2sat_p)))));
+    probe* num_exprs = mk_num_exprs_probe();
+    probe* size_limit = mk_const_probe(SMALL_SIZE);
+    probe* too_large = mk_ge(num_exprs, size_limit);
+    tactic* fail_large = fail_if(too_large);
+    tactic* fail_not_ilp = fail_if_not(mk_is_ilp_probe());
+    tactic* fail_undecided = mk_fail_if_undecided_tactic();
+    tactic* branch1 = and_then(fail_large,
+                               fail_not_ilp,
+                               fail_undecided);
+
+    tactic* pb2bv = mk_pb2bv_tactic(m);
+    tactic* pb2bv_with_params = using_params(pb2bv, pb2bv_p);
+    tactic* fail_not_qfbv = fail_if_not(mk_is_qfbv_probe());
+    tactic* bv2sat = mk_bv2sat_tactic(m);
+    tactic* bv2sat_with_params = using_params(bv2sat, bv2sat_p);
+    tactic* branch2 = and_then(pb2bv_with_params,
+                               fail_not_qfbv,
+                               bv2sat_with_params);
+
+    tactic* core = and_then(fail_if_not(mk_is_pb_probe()),
+                            fail_if(mk_produce_proofs_probe()),
+                            fail_if(mk_produce_unsat_cores_probe()),
+                            or_else(branch1, branch2));
+
+    return annotate_tactic("pb-tactic", core);
 }
 
 
@@ -129,18 +147,29 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) {
     params_ref bv2sat_p;
     bv2sat_p.set_bool("ite_extra", true);
     
-    return annotate_tactic(
-        "lia2sat-tactic",
-        // TODO: non-deterministic parameter evaluation
-        and_then(fail_if(mk_is_unbounded_probe()),
-                 fail_if(mk_produce_proofs_probe()),
-                 fail_if(mk_produce_unsat_cores_probe()),
-                 mk_propagate_ineqs_tactic(m),
-                 mk_normalize_bounds_tactic(m),
-                 mk_lia2pb_tactic(m),
-                 using_params(mk_pb2bv_tactic(m), pb2bv_p),
-                 fail_if_not(mk_is_qfbv_probe()),                    
-                 using_params(mk_bv2sat_tactic(m), bv2sat_p)));
+    tactic* fail_unbounded = fail_if(mk_is_unbounded_probe());
+    tactic* fail_proofs = fail_if(mk_produce_proofs_probe());
+    tactic* fail_unsat = fail_if(mk_produce_unsat_cores_probe());
+    tactic* propagate_ineqs = mk_propagate_ineqs_tactic(m);
+    tactic* normalize_bounds = mk_normalize_bounds_tactic(m);
+    tactic* lia2pb = mk_lia2pb_tactic(m);
+    tactic* pb2bv = mk_pb2bv_tactic(m);
+    tactic* pb2bv_with_params = using_params(pb2bv, pb2bv_p);
+    tactic* fail_not_qfbv = fail_if_not(mk_is_qfbv_probe());
+    tactic* bv2sat = mk_bv2sat_tactic(m);
+    tactic* bv2sat_with_params = using_params(bv2sat, bv2sat_p);
+
+    tactic* core = and_then(fail_unbounded,
+                            fail_proofs,
+                            fail_unsat,
+                            propagate_ineqs,
+                            normalize_bounds,
+                            lia2pb,
+                            pb2bv_with_params,
+                            fail_not_qfbv,
+                            bv2sat_with_params);
+
+    return annotate_tactic("lia2sat-tactic", core);
 }
 
 // Try to find a model for an unbounded ILP problem.
@@ -153,24 +182,41 @@ static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
     add_bounds_p2.set_rat("add_bound_lower", rational(-32));
     add_bounds_p2.set_rat("add_bound_upper", rational(31));
 
-    return annotate_tactic(
-        "ilp-model-finder-tactic",
-        // TODO: non-deterministic parameter evaluation
-        // TODO: non-deterministic parameter evaluation
-        and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())),
-                 fail_if(mk_produce_proofs_probe()),
-                 fail_if(mk_produce_unsat_cores_probe()),
-                 mk_propagate_ineqs_tactic(m),
-                 or_else(// try_for(mk_mip_tactic(m), 5000),
-                     try_for(mk_no_cut_smt_tactic(m, 100), 2000),
-                     and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p1),
-                              try_for(mk_lia2sat_tactic(m), 5000)),
-                     try_for(mk_no_cut_smt_tactic(m, 200), 5000),
-                     and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p2),
-                              try_for(mk_lia2sat_tactic(m), 10000))
-                     // , mk_mip_tactic(m)
-                         ),
-                 mk_fail_if_undecided_tactic()));
+    probe* is_ilp = mk_is_ilp_probe();
+    probe* is_unbounded = mk_is_unbounded_probe();
+    probe* ilp_unbounded = mk_and(is_ilp, is_unbounded);
+    tactic* fail_not_ilp_unbounded = fail_if_not(ilp_unbounded);
+    tactic* fail_proofs = fail_if(mk_produce_proofs_probe());
+    tactic* fail_unsat = fail_if(mk_produce_unsat_cores_probe());
+    tactic* propagate_ineqs = mk_propagate_ineqs_tactic(m);
+
+    tactic* add_bounds1 = mk_add_bounds_tactic(m);
+    tactic* add_bounds1_params = using_params(add_bounds1, add_bounds_p1);
+    tactic* lia2sat1 = try_for(mk_lia2sat_tactic(m), 5000);
+    tactic* branch_bounds1 = and_then(add_bounds1_params, lia2sat1);
+
+    tactic* add_bounds2 = mk_add_bounds_tactic(m);
+    tactic* add_bounds2_params = using_params(add_bounds2, add_bounds_p2);
+    tactic* lia2sat2 = try_for(mk_lia2sat_tactic(m), 10000);
+    tactic* branch_bounds2 = and_then(add_bounds2_params, lia2sat2);
+
+    tactic* branch_no_cut1 = try_for(mk_no_cut_smt_tactic(m, 100), 2000);
+    tactic* branch_no_cut2 = try_for(mk_no_cut_smt_tactic(m, 200), 5000);
+    tactic* or_branch = or_else(branch_no_cut1,
+                                branch_bounds1,
+                                branch_no_cut2,
+                                branch_bounds2);
+
+    tactic* fail_undecided = mk_fail_if_undecided_tactic();
+
+    tactic* core = and_then(fail_not_ilp_unbounded,
+                            fail_proofs,
+                            fail_unsat,
+                            propagate_ineqs,
+                            or_branch,
+                            fail_undecided);
+
+    return annotate_tactic("ilp-model-finder-tactic", core);
 }
 
 static tactic * mk_bounded_tactic(ast_manager & m) {
@@ -202,16 +248,24 @@ tactic * mk_preamble_tactic(ast_manager& m) {
     lia2card_p.set_uint("lia2card.max_range", 1);
     lia2card_p.set_uint("lia2card.max_ite_nesting", 1);
 
-    return
-        // TODO: non-deterministic parameter evaluation
-        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_lia2card_tactic(m, lia2card_p),
-            mk_elim_uncnstr_tactic(m));
+    tactic* simplify = 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 = using_params(simplify2, pull_ite_p);
+    tactic* solve_eqs = mk_solve_eqs_tactic(m);
+    tactic* lia2card = mk_lia2card_tactic(m, lia2card_p);
+    tactic* elim_unc = mk_elim_uncnstr_tactic(m);
+
+    return and_then(
+        simplify,
+        propagate,
+        ctx_simplify_with_params,
+        simplify_with_pull,
+        solve_eqs,
+        lia2card,
+        elim_unc);
 }
 
 tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
@@ -230,22 +284,34 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & 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),
-            // TODO: non-deterministic parameter evaluation
-            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);
+    tactic* preamble = mk_preamble_tactic(m);
+    tactic* simplify_lhs = using_params(mk_simplify_tactic(m), lhs_p);
+
+    tactic* ilp_finder = mk_ilp_model_finder_tactic(m);
+    tactic* pb_tac = mk_pb_tactic(m);
+    tactic* fail_not_quasi = fail_if_not(mk_is_quasi_pb_probe());
+    tactic* lia2sat = mk_lia2sat_tactic(m);
+    tactic* lia2sat_with_params = using_params(lia2sat, quasi_pb_p);
+    tactic* fail_undecided = mk_fail_if_undecided_tactic();
+    tactic* quasi_branch = and_then(fail_not_quasi,
+                                    lia2sat_with_params,
+                                    fail_undecided);
+    tactic* bounded = mk_bounded_tactic(m);
+    tactic* smt = mk_smt_tactic(m);
+
+    tactic* branches = or_else(ilp_finder,
+                               pb_tac,
+                               quasi_branch,
+                               bounded,
+                               smt);
+
+    tactic* core = and_then(preamble,
+                            simplify_lhs,
+                            branches);
+
+    tactic* st = using_params(core, main_p);
 
     
     st->updt_params(p);
     return st;
 }
-