diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp
index 2b5e7e006..c7b110dff 100644
--- a/src/ast/rewriter/rewriter.cpp
+++ b/src/ast/rewriter/rewriter.cpp
@@ -173,6 +173,7 @@ void rewriter_core::elim_reflex_prs(unsigned spos) {
 rewriter_core::rewriter_core(ast_manager & m, bool proof_gen):
     m_manager(m),
     m_proof_gen(proof_gen),
+    m_cancel_check(true),
     m_result_stack(m),
     m_result_pr_stack(m),
     m_num_qvars(0) {
diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index 44f436fa8..401d00d89 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -48,6 +48,7 @@ protected:
     };
     ast_manager &              m_manager;
     bool                       m_proof_gen; 
+    bool                       m_cancel_check;
     typedef act_cache          cache;
     ptr_vector<cache>          m_cache_stack;
     cache *                    m_cache; // current cache.
@@ -114,6 +115,7 @@ public:
     ast_manager & m() const { return m_manager; }
     void reset();
     void cleanup();
+    void set_cancel_check(bool f) { m_cancel_check = f; }
 #ifdef _TRACE
     void display_stack(std::ostream & out, unsigned pp_depth);
 #endif
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 4d55632d3..eaf5713ee 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -595,7 +595,7 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
-    if (m().canceled()) {
+    if (m_cancel_check && m().canceled()) {
         throw rewriter_exception(m().limit().get_cancel_msg());
     }
     SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
@@ -629,7 +629,7 @@ template<bool ProofGen>
 void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
     SASSERT(!frame_stack().empty());
     while (!frame_stack().empty()) {
-        if (m().canceled()) {
+        if (m_cancel_check && m().canceled()) {
             throw rewriter_exception(m().limit().get_cancel_msg());
         }
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index ebb5e00c8..4f6741989 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -342,6 +342,7 @@ public:
                     else
                         cls1.push_back(cls2[j]);
                 }
+                (void)found_pivot2;
                 assert(found_pivot2);
                 return;
             }
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index f20f16a08..95d66f617 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -362,6 +362,7 @@ public:
                     else
                         cls1.push_back(cls2[j]);
                 }
+                (void)found_pivot2;
                 assert(found_pivot2);
                 return;
             }
diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 2bf4d5ba3..0c96dfde3 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -249,6 +249,7 @@ void grobner::update_order() {
 }
 
 bool grobner::var_lt::operator()(expr * v1, expr * v2) const {
+    if (v1 == v2) return false;
     int w1 = 0;
     int w2 = 0;
     m_var2weight.find(v1, w1);
@@ -268,6 +269,8 @@ bool grobner::monomial_lt::operator()(monomial * m1, monomial * m2) const {
     for (; it1 != end1; ++it1, ++it2) {
         expr * v1 = *it1;
         expr * v2 = *it2;
+        if (v1 == v2)
+            continue;
         if (m_var_lt(v1, v2))
             return true;
         if (v1 != v2)
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index a5b900ab7..74f6a18c1 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -259,6 +259,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
+        return BR_FAILED;
+        // disabled until made more efficient
         if (a == b) {
             result = m().mk_true();
             return BR_DONE;
@@ -271,6 +273,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             conj.push_back(m().mk_eq(else1, else2));
             args1.push_back(a);
             args2.push_back(b);
+            // TBD: this is too inefficient.
             for (unsigned i = 0; i < stores.size(); ++i) {
                 args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr());
                 args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr());
@@ -362,6 +365,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
                                     false, // no proofs for evaluator
                                     m_cfg),
         m_cfg(md.get_manager(), md, p) {
+        set_cancel_check(false);
     }
 };
 
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index e8e93dafc..049c34343 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -300,6 +300,7 @@ public:
                 break;
 
             case datalog::OK: 
+                (void)query_exn;
                 SASSERT(query_exn);
                 break;
 
diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp
index 3b9198dc6..0baa297bc 100644
--- a/src/muz/rel/karr_relation.cpp
+++ b/src/muz/rel/karr_relation.cpp
@@ -173,6 +173,7 @@ namespace datalog {
                 else {
                     processed = false;
                 }
+                (void)processed;
                 TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";
                       if (processed) matrix::display_ineq(tout, row, M.b.back(), M.eq.back());
                       );
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index f8f78835c..8822f4e77 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -137,81 +137,12 @@ public:
     }
 };
 
-class alternate_min_max_cmd : public cmd {
-    app_ref_vector*      m_vars;
-    svector<bool>        m_is_max;
-    unsigned             m_position;
-
-    app_ref_vector& vars(cmd_context& ctx) {
-        if (!m_vars) {
-            m_vars = alloc(app_ref_vector, ctx.m());
-        }
-        return *m_vars;
-    }
-public:
-    alternate_min_max_cmd():
-        cmd("min-max"),
-        m_vars(0),
-        m_position(0)
-    {}
-    
-    virtual void reset(cmd_context & ctx) { 
-        dealloc(m_vars);
-        m_vars = 0;
-        m_is_max.reset();
-        m_position = 0;
-    }
-    virtual char const * get_usage() const { return "(min | max | var)+ <term>"; }
-    virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo alternating min-max objectives";}
-    virtual unsigned get_arity() const { return 2; }
-    virtual void prepare(cmd_context & ctx) {}
-    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
-        switch (m_position) {
-        case 0: return CPK_SYMBOL_LIST;
-        case 1: return CPK_EXPR;
-        default: return CPK_SYMBOL;
-        }
-    }
-
-    virtual void set_next_arg(cmd_context & ctx, unsigned num, symbol const * slist) {
-        bool is_max = false;
-        for (unsigned i = 0; i < num; ++i) {
-            if (slist[i] == symbol("max")) {
-                is_max = true;
-            }
-            else if (slist[i] == symbol("min")) {
-                is_max = false;
-            }
-            else {
-                m_is_max.push_back(is_max);
-                vars(ctx).push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
-            }
-        }
-        ++m_position;
-    }
-
-    virtual void set_next_arg(cmd_context & ctx, expr * t) {
-        if (!is_app(t)) {
-            throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
-        }
-        ++m_position;
-        get_opt(ctx).min_max(to_app(t), vars(ctx), m_is_max);
-        reset(ctx);
-    }
-
-    virtual void failure_cleanup(cmd_context & ctx) {
-        reset(ctx);
-    }
-
-    virtual void execute(cmd_context & ctx) { }
-};
 
 
 void install_opt_cmds(cmd_context & ctx) {
     ctx.insert(alloc(assert_soft_cmd));
     ctx.insert(alloc(min_maximize_cmd, true));
     ctx.insert(alloc(min_maximize_cmd, false));
-    ctx.insert(alloc(alternate_min_max_cmd));
 }
 
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 0c19e7987..fccdf9b55 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -212,18 +212,6 @@ namespace opt {
         m_hard_constraints.append(s.m_hard);
     }
 
-    lbool context::min_max(app* t, app_ref_vector const& vars, svector<bool> const& is_max) {
-        clear_state();
-        init_solver(); 
-        import_scoped_state(); 
-        normalize();
-        internalize();
-        qe::max_min_opt max_min(m, m_params);
-        max_min.add(m_hard_constraints);
-        return max_min.check(is_max, vars, t);
-    }
-
-
     lbool context::optimize() {
         if (m_pareto) {
             return execute_pareto();
@@ -236,12 +224,12 @@ namespace opt {
         import_scoped_state(); 
         normalize();
         internalize();
+        update_solver();
 #if 0
         if (is_qsat_opt()) {
             return run_qsat_opt();
         }
 #endif
-        update_solver();
         solver& s = get_solver();
         s.assert_expr(m_hard_constraints);
         display_benchmark();
@@ -1473,6 +1461,7 @@ namespace opt {
             value.neg();
         }
         if (result != l_undef) {
+            m_optsmt.setup(*m_opt_solver.get());
             m_optsmt.update_lower(obj.m_index, value);
             m_optsmt.update_upper(obj.m_index, value);
         }
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index b7dceb674..3339dc37a 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -172,7 +172,6 @@ namespace opt {
         virtual ~context();
         unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
         unsigned add_objective(app* t, bool is_max);
-        lbool min_max(app* t, app_ref_vector const& vars, svector<bool> const& is_max);
         void add_hard_constraint(expr* f);
         
 
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index eff70e48e..fccc7fa1c 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -344,6 +344,10 @@ namespace opt {
     }
     
     expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
+		if (!val.is_finite())
+		{
+			return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
+		}
         smt::theory_opt& opt = get_optimizer();
         smt::theory_var v = m_objective_vars[var];
 
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 58a290c0b..48dacdbf4 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -24,9 +24,9 @@ Revision History:
 #include "ast_util.h"
 #include "arith_decl_plugin.h"
 #include "ast_pp.h"
+#include "model_v2_pp.h"
 #include "th_rewriter.h"
 #include "expr_functors.h"
-#include "model_v2_pp.h"
 #include "expr_safe_replace.h"
 #include "model_based_opt.h"
 
@@ -103,19 +103,19 @@ namespace qe {
             expr_ref t(m);
             opt::ineq_type ty = opt::t_le;
             expr* e1, *e2;
+            DEBUG_CODE(expr_ref val(m); VERIFY(model.eval(lit, val) && m.is_true(val)););
+
             bool is_not = m.is_not(lit, lit);
             if (is_not) {
                 mul.neg();
             }
             SASSERT(!m.is_not(lit));
             if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
-                if (is_not) mul.neg();
                 linearize(mbo, model, mul, e1, c, ts, tids);
                 linearize(mbo, model, -mul, e2, c, ts, tids);
                 ty = is_not ? opt::t_lt : opt::t_le;
             }
             else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
-                if (is_not) mul.neg();
                 linearize(mbo, model,  mul, e1, c, ts, tids);
                 linearize(mbo, model, -mul, e2, c, ts, tids);
                 ty = is_not ? opt::t_le: opt::t_lt;
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 73f6a9d4c..fe11de199 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -618,7 +618,7 @@ namespace qe {
         }
 
         kernel& get_kernel(unsigned j) {        
-            if (m_kernel_ex || is_exists(j)) {
+            if (is_exists(j)) {
                 return m_ex; 
             }
             else {
@@ -735,11 +735,7 @@ namespace qe {
         void display(std::ostream& out) const {
             out << "level: " << m_level << "\n";
             for (unsigned i = 0; i < m_vars.size(); ++i) {
-                for (unsigned j = 0; j < m_vars[i].size(); ++j) {
-                    expr* v = m_vars[i][j];
-                    out << mk_pp(v, m) << " ";
-                }
-                out << "\n";
+                out << m_vars[i] << "\n";
             }
             m_pred_abs.display(out);
         }
@@ -1070,8 +1066,7 @@ namespace qe {
             m_level(0),
             m_mode(mode),
             m_avars(m),
-            m_free_vars(m),
-            m_kernel_ex(false)
+            m_free_vars(m)
         {
             reset();
         }
@@ -1238,90 +1233,6 @@ namespace qe {
         }
 
 
-        bool         m_kernel_ex;
-
-        lbool max_min(expr_ref_vector const& fmls, svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
-            m_kernel_ex = true;
-            // Assume this is the only call to check.
-            expr_ref_vector defs(m);
-            app_ref_vector free_vars(m), vars1(m);
-            expr_ref fml = mk_and(fmls);
-            m_pred_abs.get_free_vars(fml, free_vars);
-            m_pred_abs.abstract_atoms(fml, defs);
-            fml = m_pred_abs.mk_abstract(fml);
-            get_kernel(0).k().assert_expr(mk_and(defs));
-            get_kernel(0).k().assert_expr(fml);
-            obj_hashtable<app> var_set;
-            for (unsigned i = 0; i < vars.size(); ++i) {
-                var_set.insert(vars[i]);
-            }
-            for (unsigned i = 0; i < free_vars.size(); ++i) {
-                app* v = free_vars[i].get();
-                if (!var_set.contains(v)) {
-                    vars1.push_back(v);
-                }
-            }
-            // 
-            // Insert all variables in alternating list of max/min objectives.
-            // By convention, the outer-most level is max.
-            //
-            bool is_m = true;
-            for (unsigned i = 0; i < vars.size(); ++i) {
-                if (is_m != is_max[i]) {
-                    m_vars.push_back(vars1);
-                    vars1.reset();       
-                    is_m = is_max[i];
-                }
-                vars1.push_back(vars[i]);
-            }
-            m_vars.push_back(vars1);
-            
-            return max_min();
-        }
-
-        lbool max_min() {
-            while (true) {
-                ++m_stats.m_num_rounds;
-                check_cancel();
-                expr_ref_vector asms(m_asms);
-                m_pred_abs.get_assumptions(m_model.get(), asms);
-                //
-                // TBD: add bound to asms.
-                // 
-                smt::kernel& k = get_kernel(m_level).k();
-                lbool res = k.check(asms);
-                switch (res) {
-                case l_true:
-                    k.get_model(m_model);
-                    SASSERT(validate_model(asms));
-                    TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
-                    // 
-                    // TBD: compute new bound on objective.
-                    // 
-                    push();
-                    break;
-                case l_false:
-                    switch (m_level) {
-                    case 0: return l_false;
-                    case 1:
-                        // TBD
-                        break;
-                    default:
-                        if (m_model.get()) {
-                            project(asms); 
-                        }
-                        else {
-                            pop(1);
-                        }
-                        break; 
-                    }
-                    break;
-                case l_undef:
-                    return res;
-                }
-            }
-            return l_undef;
-        }
 
     };
 
@@ -1331,49 +1242,6 @@ namespace qe {
         return qs.maximize(fmls, t, mdl, value);
     }    
 
-
-    struct max_min_opt::imp {
-
-        expr_ref_vector m_fmls;
-        qsat            m_qsat;
-
-        imp(ast_manager& m, params_ref const& p): 
-            m_fmls(m), 
-            m_qsat(m, p, qsat_maximize)
-        {}
-
-        void add(expr* e) {
-            m_fmls.push_back(e);
-        }
-
-        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
-            return m_qsat.max_min(m_fmls, is_max, vars, t);
-        }
-
-    };
-
-    max_min_opt::max_min_opt(ast_manager& m, params_ref const& p) {
-        m_imp = alloc(imp, m, p);
-    }
-
-    max_min_opt::~max_min_opt() {
-        dealloc(m_imp);
-    }
-
-    void max_min_opt::add(expr* e) {
-        m_imp->add(e);
-    }
-
-    void max_min_opt::add(expr_ref_vector const& fmls) {
-        for (unsigned i = 0; i < fmls.size(); ++i) {
-            add(fmls[i]);
-        }
-    }
-
-    lbool max_min_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
-        return m_imp->check(is_max, vars, t);
-    }
-
 };
 
 tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) {
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
index 59cf6d8a0..456711c4f 100644
--- a/src/qe/qsat.h
+++ b/src/qe/qsat.h
@@ -114,17 +114,6 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
-    class max_min_opt {
-        struct imp;
-        imp* m_imp;
-    public:
-        max_min_opt(ast_manager& m, params_ref const& p = params_ref());
-        ~max_min_opt();
-        void add(expr* e);
-        void add(expr_ref_vector const& fmls);
-        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
-    };
-
     lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p);
 
 }
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index 2881c03ae..eabc4fdb1 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -52,6 +52,7 @@ namespace sat {
 
     bool clause::check_approx() const {
         var_approx_set curr = m_approx;
+        (void)curr;
         const_cast<clause*>(this)->update_approx();
         SASSERT(may_eq(curr, m_approx));
         return true;
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index ac2a51c4d..c60fb86cb 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -159,7 +159,8 @@ namespace sat {
         for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
             literal l = ~to_literal(l_idx);            
             watch_list const & wlist = *it;
-            CTRACE("sat_bug", s.was_eliminated(l.var()) && !wlist.empty(),
+            CTRACE("sat_bug", 
+                   s.was_eliminated(l.var()) && !wlist.empty(),
                    tout << "l: " << l << "\n";
                    s.display_watches(tout);
                    s.display(tout););
@@ -179,7 +180,7 @@ namespace sat {
                            tout << "\n";
                            sat::display(tout, s.m_cls_allocator, s.get_wlist(~(it2->get_literal())));
                            tout << "\n";);
-                    SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
+                        SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
                     break;
                 case watched::TERNARY:
                     SASSERT(!s.was_eliminated(it2->get_literal1().var()));
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index daaed13ac..f55945ce4 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -739,6 +739,7 @@ public:
         if (idx2 < idx1) {
             std::swap(idx1,idx2);
         }        
+        (void) max_idx;
         SASSERT(idx1 < idx2 && idx2 < edges.size());
         SASSERT(max_idx < edges.size());
         dst = get_source(edges[idx2]);
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 88676b4d9..163452d47 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1342,6 +1342,7 @@ namespace smt {
               tout << "v" << x_i << " ";
               tout << (has_shared?"shared":"not shared") << "\n";);
 
+        (void) empty_column;
         SASSERT(!safe_gain(min_gain, max_gain) ||
                 empty_column ||
                 (unbounded_gain(max_gain) == (x_i == null_theory_var)));
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index ea8ba0f79..0268d2353 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -218,6 +218,7 @@ namespace smt {
             SASSERT(r && bv_sz == m_ebits);
             r = m_bu.is_numeral(values[2], sig_r, bv_sz);
             SASSERT(r && bv_sz == m_sbits - 1);
+            (void)r;
 
             SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
             SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 97189ce4c..8a1ee2946 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1820,22 +1820,16 @@ bool theory_seq::solve_ne(unsigned idx) {
             TRACE("seq", display_disequation(tout << "reduces to false: ", n););
             return true;
         }
+        else if (!change) {
+            TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";);
+            if (updated) {
+                new_ls.push_back(n.ls(i));
+                new_rs.push_back(n.rs(i));
+            }
+            continue;
+        }
         else {
 
-            // eliminate ite expressions.
-            reduce_ite(lhs, new_lits, num_undef_lits, change);
-            reduce_ite(rhs, new_lits, num_undef_lits, change);
-            reduce_ite(ls, new_lits, num_undef_lits, change);
-            reduce_ite(rs, new_lits, num_undef_lits, change);            
-
-            if (!change) {
-                TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";);
-                if (updated) {
-                    new_ls.push_back(n.ls(i));
-                    new_rs.push_back(n.rs(i));
-                }
-                continue;
-            }
 
             if (!updated) {
                 for (unsigned j = 0; j < i; ++j) {
@@ -1940,32 +1934,6 @@ bool theory_seq::solve_ne(unsigned idx) {
     return updated;
 }
 
-void theory_seq::reduce_ite(expr_ref_vector & ls, literal_vector& new_lits, unsigned& num_undef_lits, bool& change) {
-    expr* cond, *th, *el;
-    context& ctx = get_context();
-    for (unsigned i = 0; i < ls.size(); ++i) {
-        expr* e = ls[i].get();
-        if (m.is_ite(e, cond, th, el)) {
-            literal lit(mk_literal(cond));
-            switch (ctx.get_assignment(lit)) {
-            case l_true:
-                change = true;
-                new_lits.push_back(lit);
-                ls[i] = th;
-                break;
-            case l_false:
-                change = true;
-                new_lits.push_back(~lit);
-                ls[i] = el;
-                break;
-            case l_undef:
-                ++num_undef_lits;
-                break;
-            }
-        }
-    }
-}
-
 
 bool theory_seq::solve_nc(unsigned idx) {
     nc const& n = m_ncs[idx];
@@ -2613,6 +2581,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     }
     expr* e = m_rep.find(e0, deps);
     expr* e1, *e2, *e3;
+    context& ctx = get_context();
     if (m_util.str.is_concat(e, e1, e2)) {
         result = mk_concat(expand(e1, deps), expand(e2, deps));
     }
@@ -2637,11 +2606,26 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     else if (m_util.str.is_index(e, e1, e2, e3)) {
         result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3);
     }
+    else if (m.is_ite(e, e1, e2, e3)) {
+        literal lit(mk_literal(e1));
+        switch (ctx.get_assignment(lit)) {
+        case l_true:
+            deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
+            result = expand(e2, deps);
+            break;
+        case l_false:
+            deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit)));
+            result = expand(e3, deps);
+            break;
+        case l_undef:
+            result = e;
+            break;
+        }
+    }
     else if (m_util.str.is_itos(e, e1)) {
         rational val;
         if (get_value(e1, val)) {
             expr_ref num(m), res(m);
-            context& ctx = get_context();
             num = m_autil.mk_numeral(val, true);
             if (!ctx.e_internalized(num)) {
                 ctx.internalize(num, false);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 8c4de2111..4107f3d05 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -410,7 +410,6 @@ namespace smt {
         bool solve_nqs(unsigned i);
         bool solve_ne(unsigned i);
         bool solve_nc(unsigned i);
-        void reduce_ite(expr_ref_vector& ls, literal_vector& new_lits, unsigned& num_undef_lits, bool& change);
 
         struct cell {
             cell*       m_parent;
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 698128e26..eae3ab5e6 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -156,6 +156,7 @@ class fm_tactic : public tactic {
                     r = c;
                 }
             }
+            (void)found;
             SASSERT(found);
             return is_lower ? LOWER : UPPER;
         }
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index f36a93e6d..4c2e0dead 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -300,6 +300,7 @@ public:
     bool get_sum(expr* x, rational const& mul, expr_ref_vector& conds, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
         expr *y, *z, *u;
         rational r, q;
+        if (!is_app(x)) return false;
         app* f = to_app(x);
         bool ok = true;
         if (a.is_add(x)) {
diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp
index 0c1744a09..df69ce76d 100644
--- a/src/util/mpn.cpp
+++ b/src/util/mpn.cpp
@@ -274,13 +274,12 @@ void mpn_manager::div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom,
 
 bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
                         mpn_digit * quot) const {
-    mpn_double_digit q_hat, temp, r_hat, ms;
+    mpn_double_digit q_hat, temp, ms;
     mpn_digit borrow;
 
     for (size_t j = numer.size()-1; j > 0; j--) {
         temp = (((mpn_double_digit)numer[j]) << DIGIT_BITS) | ((mpn_double_digit)numer[j-1]);
         q_hat = temp / (mpn_double_digit) denom;
-        r_hat = temp % (mpn_double_digit) denom;
         if (q_hat >= BASE) {
             UNREACHABLE(); // is this reachable with normalized v?
         }
@@ -294,11 +293,13 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
             quot[j-1]--;
             numer[j] = numer[j-1] + denom;
         }
-        TRACE("mpn_div1", tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
-                          tout << " ms=" << ms;
-                          tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
-                          tout << " borrow=" << borrow;
-                          tout << std::endl; );
+        TRACE("mpn_div1", 
+              mpn_double_digit r_hat = temp % (mpn_double_digit) denom;
+              tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
+              tout << " ms=" << ms;
+              tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
+              tout << " borrow=" << borrow;
+              tout << std::endl; );
     }
 
     return true; // return rem != 0?