diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 98c3b7962..89af8bd3e 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1002,14 +1002,6 @@ class smt2_printer {
         reset_stacks();
         SASSERT(&(r.get_manager()) == &(fm()));
         m_soccs(n);
-        TRACE("smt2_pp_shared",
-              tout << "shared terms for:\n" << mk_pp(n, m()) << "\n";
-              tout << "------>\n";
-              shared_occs::iterator it  = m_soccs.begin_shared();
-              shared_occs::iterator end = m_soccs.end_shared();
-              for (; it != end; ++it) {
-                  tout << mk_pp(*it, m()) << "\n";
-              });
         m_root = n;
         push_frame(n, true);
         while (!m_frame_stack.empty()) {
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 0f7c8f5ea..5df54855b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -551,13 +551,13 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     // case 1: pos<0 or len<0
     // rewrite to ""
     if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) {
-        result = m_util.str.mk_string(symbol(""));
+        result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
     // case 1.1: pos >= length(base)
     // rewrite to ""
     if (constantBase && constantPos && pos.get_unsigned() >= s.length()) {
-        result = m_util.str.mk_string(symbol(""));
+        result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
 
@@ -663,20 +663,21 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
 br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
     zstring c;
     rational r;
-    if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) {
+    if (m_autil.is_numeral(b, r)) {
         if (r.is_neg()) {
-            result = m_util.str.mk_string(symbol(""));
+            result = m_util.str.mk_empty(m().get_sort(a));
+            return BR_DONE;
+        } 
+        unsigned len = 0;
+        bool bounded = min_length(1, &a, len);
+        if (bounded && r >= rational(len)) {
+            result = m_util.str.mk_empty(m().get_sort(a));
             return BR_DONE;
-        } else if (r.is_unsigned()) {
-            unsigned j = r.get_unsigned();
-            if (j < c.length()) {
-                result = m_util.str.mk_string(c.extract(j, 1));
-                return BR_DONE;
-            } else {
-                result = m_util.str.mk_string(symbol(""));
-                return BR_DONE;
-            }
         }
+        if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) {
+            result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1));
+            return BR_DONE;
+        } 
     }
     return BR_FAILED;
 }
@@ -734,6 +735,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     bool isc2 = m_util.str.is_string(b, s2);
     if (isc1 && isc2) {
         result = m().mk_bool_val(s1.prefixof(s2));
+        TRACE("seq", tout << result << "\n";);
         return BR_DONE;
     }
     if (m_util.str.is_empty(a)) {
@@ -747,6 +749,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     expr_ref_vector as(m()), bs(m());
 
     if (a1 != b1 && isc1 && isc2) {
+        TRACE("seq", tout << s1 << " " << s2 << "\n";);
         if (s1.length() <= s2.length()) {
             if (s1.prefixof(s2)) {
                 if (a == a1) {
@@ -791,26 +794,27 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     m_util.str.get_concat(a, as);
     m_util.str.get_concat(b, bs);
     unsigned i = 0;
-    bool all_values = true;    
     expr_ref_vector eqs(m());
     for (; i < as.size() && i < bs.size(); ++i) {
         expr* a = as[i].get(), *b = bs[i].get();
         if (a == b) {
             continue;
         }
-        all_values &= m().is_value(a) && m().is_value(b);
-        if (all_values) {
-            result = m().mk_false();
-            return BR_DONE;
-        }
         if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
             eqs.push_back(m().mk_eq(a, b));
             continue;
         }
+        if (m().is_value(a) && m().is_value(b) && m_util.str.is_string(a) && m_util.str.is_string(b)) {
+            TRACE("seq", tout << mk_pp(a, m()) << " != " << mk_pp(b, m()) << "\n";);
+            result = m().mk_false();
+            return BR_DONE;
+        }
+
         break;
     }
     if (i == as.size()) {
         result = mk_and(eqs);
+        TRACE("seq", tout << result << "\n";);
         if (m().is_true(result)) {
             return BR_DONE;
         }
@@ -822,6 +826,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
             eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
         }
         result = mk_and(eqs);
+        TRACE("seq", tout << result << "\n";);
         return BR_REWRITE3;
     }
     if (i > 0) {
@@ -829,6 +834,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
         a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
         b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i); 
         result = m_util.str.mk_prefix(a, b);
+        TRACE("seq", tout << result << "\n";);
         return BR_DONE;
     }
     else {
diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp
index 11ed1b9e0..a72e7e117 100644
--- a/src/ast/simplifier/bv_simplifier_plugin.cpp
+++ b/src/ast/simplifier/bv_simplifier_plugin.cpp
@@ -1517,13 +1517,24 @@ void bv_simplifier_plugin::mk_bv2int(expr * arg, sort* range, expr_ref & result)
         result = m_arith.mk_add(tmp1, tmp2);        
     }
     // commented out to reproduce bug in reduction of int2bv/bv2int
-    else if (m_util.is_concat(arg)) {
-        expr_ref tmp1(m_manager), tmp2(m_manager);
-        unsigned sz2 = get_bv_size(to_app(arg)->get_arg(1));
-        mk_bv2int(to_app(arg)->get_arg(0), range, tmp1);
-        mk_bv2int(to_app(arg)->get_arg(1), range, tmp2);
-        tmp1 = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz2), true), tmp1);
-        result = m_arith.mk_add(tmp1, tmp2);
+    else if (m_util.is_concat(arg) && to_app(arg)->get_num_args() > 0) {
+        expr_ref_vector args(m_manager);        
+        unsigned num_args = to_app(arg)->get_num_args();
+        for (unsigned i = 0; i < num_args; ++i) {
+            expr_ref tmp(m_manager);
+            mk_bv2int(to_app(arg)->get_arg(i), range, tmp);
+            args.push_back(tmp);
+        }
+        unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1));
+        for (unsigned i = num_args - 1; i > 0; ) {
+            expr_ref tmp(m_manager);
+            --i;
+            tmp = args[i].get();
+            tmp = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz), true), tmp);
+            args[i] = tmp;
+            sz += get_bv_size(to_app(arg)->get_arg(i));
+        }
+        result = m_arith.mk_add(args.size(), args.c_ptr());
     }
     else {
         parameter parameter(range);
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 82d351113..031c5098e 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -126,6 +126,12 @@ namespace datalog {
         app* s;
         var* v;
 
+        // disable Ackerman reduction if head contains a non-variable or non-constant argument.
+        for (unsigned i = 0; i < to_app(head)->get_num_args(); ++i) {
+            expr* arg = to_app(head)->get_arg(i);            
+            if (!is_var(arg) && !m.is_value(arg)) return false;
+        }
+
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* e = conjs[i].get();
             if (is_select_eq_var(e, s, v)) {
@@ -281,6 +287,7 @@ namespace datalog {
         m_rewriter(body);
         sub(head);
         m_rewriter(head);
+        TRACE("dl", tout << body << " => " << head << "\n";);
         change = ackermanize(r, body, head);
         if (!change) {
             rules.add_rule(&r);
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index ea0e6c887..455b06d3d 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -394,10 +394,6 @@ namespace datalog {
         m_simp(a, simp1_res);
         (*m_rw)(simp1_res.get(), res);
 
-        /*if (simp1_res.get()!=res.get()) {
-            std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
-        }*/
-
         m_simp(res.get(), res);
     }
 
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 351141a3f..8ae4e467f 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -50,6 +50,7 @@ namespace opt {
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
             m_params.m_relevancy_lvl = 0;
         }
+        // m_params.m_auto_config = false;
     }
 
     unsigned opt_solver::m_dump_count = 0;
diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 8a761ea3a..cca0c5c1b 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -96,7 +96,6 @@ namespace sat {
                 if (!process(c))
                     continue; // clause was removed
                 *it2 = *it;
-                // throw exception to test bug fix: if (it2 != it) throw solver_exception("trigger bug");
                 ++it2;
             }
             s.m_clauses.set_end(it2);
@@ -129,14 +128,14 @@ namespace sat {
         // check if the clause is already satisfied
         for (i = 0; i < sz; i++) {
             if (s.value(c[i]) == l_true) {
-                s.dettach_clause(c);
+                s.detach_clause(c);
                 s.del_clause(c);
                 return false;
             }
         }
         // try asymmetric branching
         // clause must not be used for propagation
-        s.dettach_clause(c);
+        solver::scoped_detach scoped_d(s, c);
         s.push();
         for (i = 0; i < sz - 1; i++) {
             literal l = c[i];
@@ -154,7 +153,6 @@ namespace sat {
         SASSERT(s.m_qhead == s.m_trail.size());
         if (i == sz - 1) {
             // clause size can't be reduced.
-            s.attach_clause(c);
             return true;
         }
         // clause can be reduced 
@@ -188,19 +186,18 @@ namespace sat {
         case 1:
             TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
             s.assign(c[0], justification());
-            s.del_clause(c);
             s.propagate_core(false); 
+            scoped_d.del_clause();
             SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
             return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
         case 2:
             SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
             s.mk_bin_clause(c[0], c[1], false);
-            s.del_clause(c);
+            scoped_d.del_clause();
             SASSERT(s.m_qhead == s.m_trail.size());
             return false;
         default:
             c.shrink(new_sz);
-            s.attach_clause(c);
             SASSERT(s.m_qhead == s.m_trail.size());
             return true;
         }
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 6a7ca6280..b7f83df6c 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -94,7 +94,7 @@ namespace sat {
                 continue;
             }
             if (!c.frozen())
-                m_solver.dettach_clause(c);
+                m_solver.detach_clause(c);
             // apply substitution
             for (i = 0; i < sz; i++) {
                 SASSERT(!m_solver.was_eliminated(c[i].var()));
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index bd975115b..007751220 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -168,14 +168,13 @@ namespace sat {
         m_need_cleanup = false;
         m_use_list.init(s.num_vars());
         init_visited();
-        bool learned_in_use_lists = false;
+        m_learned_in_use_lists = false;
         if (learned) {
             register_clauses(s.m_learned);
-            learned_in_use_lists = true;
+            m_learned_in_use_lists = true;
         }
         register_clauses(s.m_clauses);
 
-
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
             elim_blocked_clauses();
 
@@ -184,7 +183,9 @@ namespace sat {
 
         m_sub_counter  = m_subsumption_limit;
         m_elim_counter = m_res_limit;
-        unsigned old_num_elim_vars = m_num_elim_vars;
+        m_old_num_elim_vars = m_num_elim_vars;
+
+        scoped_finalize _scoped_finalize(*this);
 
         do {
             if (m_subsumption)
@@ -199,20 +200,22 @@ namespace sat {
                 break;
         }
         while (!m_sub_todo.empty());
+    }
 
-        bool vars_eliminated = m_num_elim_vars > old_num_elim_vars;
+    void simplifier::scoped_finalize_fn() {
+        bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
 
         if (m_need_cleanup) {
             TRACE("after_simplifier", tout << "cleanning watches...\n";);
             cleanup_watches();
-            cleanup_clauses(s.m_learned, true, vars_eliminated,  learned_in_use_lists);
+            cleanup_clauses(s.m_learned, true, vars_eliminated,  m_learned_in_use_lists);
             cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
         }
         else {
             TRACE("after_simplifier", tout << "skipping cleanup...\n";);
             if (vars_eliminated) {
                 // must remove learned clauses with eliminated variables
-                cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
+                cleanup_clauses(s.m_learned, true, true, m_learned_in_use_lists);
             }
         }
         CASSERT("sat_solver", s.check_invariant());
@@ -279,7 +282,10 @@ namespace sat {
             unsigned sz = c.size();
             if (sz == 0) {
                 s.set_conflict(justification());
-                return;
+                for (; it != end; ++it, ++it2) {
+                    *it2 = *it;
+                }
+                break;
             }
             if (sz == 1) {
                 s.assign(c[0], justification());
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 9ee239083..d26d0041f 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -91,6 +91,9 @@ namespace sat {
         unsigned               m_num_sub_res;
         unsigned               m_num_elim_lits;
 
+        bool                   m_learned_in_use_lists;
+        unsigned               m_old_num_elim_vars;
+
         struct size_lt {
             bool operator()(clause const * c1, clause const * c2) const { return c1->size() > c2->size(); }
         };
@@ -170,6 +173,14 @@ namespace sat {
         struct subsumption_report;
         struct elim_var_report;
 
+        class scoped_finalize {
+            simplifier& s;
+        public:
+            scoped_finalize(simplifier& s) : s(s) {}
+            ~scoped_finalize() { s.scoped_finalize_fn(); }
+        };
+        void scoped_finalize_fn();
+
     public:
         simplifier(solver & s, params_ref const & p);
         ~simplifier();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 57cdc2fb4..a66f82486 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -462,25 +462,25 @@ namespace sat {
             return simplify_clause_core<false>(num_lits, lits);
     }
 
-    void solver::dettach_bin_clause(literal l1, literal l2, bool learned) {
+    void solver::detach_bin_clause(literal l1, literal l2, bool learned) {
         get_wlist(~l1).erase(watched(l2, learned));
         get_wlist(~l2).erase(watched(l1, learned));
     }
 
-    void solver::dettach_clause(clause & c) {
+    void solver::detach_clause(clause & c) {
         if (c.size() == 3)
-            dettach_ter_clause(c);
+            detach_ter_clause(c);
         else
-            dettach_nary_clause(c);
+            detach_nary_clause(c);
     }
 
-    void solver::dettach_nary_clause(clause & c) {
+    void solver::detach_nary_clause(clause & c) {
         clause_offset cls_off = get_offset(c);
         erase_clause_watch(get_wlist(~c[0]), cls_off);
         erase_clause_watch(get_wlist(~c[1]), cls_off);
     }
 
-    void solver::dettach_ter_clause(clause & c) {
+    void solver::detach_ter_clause(clause & c) {
         erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
         erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
         erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
@@ -1493,7 +1493,7 @@ namespace sat {
         for (unsigned i = new_sz; i < sz; i++) {
             clause & c = *(m_learned[i]);
             if (can_delete(c)) {
-                dettach_clause(c);
+                detach_clause(c);
                 del_clause(c);
             }
             else {
@@ -1551,7 +1551,7 @@ namespace sat {
                     else {
                         c.inc_inact_rounds();
                         if (c.inact_rounds() > m_config.m_gc_k) {
-                            dettach_clause(c);
+                            detach_clause(c);
                             del_clause(c);
                             m_stats.m_gc_clause++;
                             deleted++;
@@ -1562,7 +1562,7 @@ namespace sat {
                     if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) {
                         // move to frozen;
                         TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";);
-                        dettach_clause(c);
+                        detach_clause(c);
                         c.reset_inact_rounds();
                         c.freeze();
                         m_num_frozen++;
@@ -2595,7 +2595,7 @@ namespace sat {
             }
             else {
                 clause & c = *(cw.get_clause());
-                dettach_clause(c);
+                detach_clause(c);
                 attach_clause(c, reinit);
                 if (scope_lvl() > 0 && reinit) {
                     // clause propagated literal, must keep it in the reinit stack.
@@ -2628,7 +2628,7 @@ namespace sat {
         for (unsigned i = 0; i < clauses.size(); ++i) {
             clause & c = *(clauses[i]);
             if (c.contains(lit)) {
-                dettach_clause(c);
+                detach_clause(c);
                 del_clause(c);
             }
             else {
@@ -2646,7 +2646,7 @@ namespace sat {
             literal l1 = m_user_bin_clauses[i].first;
             literal l2 = m_user_bin_clauses[i].second;
             if (nlit == l1 || nlit == l2) {
-                dettach_bin_clause(l1, l2, learned);
+                detach_bin_clause(l1, l2, learned);
             }
         }
     }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index f910e374f..6c91565aa 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -195,15 +195,34 @@ namespace sat {
         bool attach_nary_clause(clause & c);
         void attach_clause(clause & c, bool & reinit);
         void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
+        class scoped_detach {
+            solver& s;
+            clause& c;
+            bool m_deleted;
+        public:
+            scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
+                s.detach_clause(c);
+            }            
+            ~scoped_detach() {
+                if (!m_deleted) s.attach_clause(c);
+            }
+
+            void del_clause() {
+                if (!m_deleted) {
+                    s.del_clause(c);
+                    m_deleted = true;
+                }
+            }
+        };
         unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
         unsigned select_learned_watch_lit(clause const & cls) const;
         bool simplify_clause(unsigned & num_lits, literal * lits) const;
         template<bool lvl0>
         bool simplify_clause_core(unsigned & num_lits, literal * lits) const;
-        void dettach_bin_clause(literal l1, literal l2, bool learned);
-        void dettach_clause(clause & c);
-        void dettach_nary_clause(clause & c);
-        void dettach_ter_clause(clause & c);
+        void detach_bin_clause(literal l1, literal l2, bool learned);
+        void detach_clause(clause & c);
+        void detach_nary_clause(clause & c);
+        void detach_ter_clause(clause & c);
         void push_reinit_stack(clause & c);
 
         // -----------------------
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 81ceb114c..7864955a4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -40,7 +40,7 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
         if (!m_found_underspecified_op) {
-            TRACE("arith", tout << "found non underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
+            TRACE("arith", tout << "found underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
             get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
             m_found_underspecified_op = true;
         }
@@ -395,6 +395,7 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_div(app * n) {
+        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
         found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
@@ -418,7 +419,7 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_mod(app * n) {
         TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
-        found_underspecified_op(n);
+        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         if (!ctx.relevancy())
@@ -428,7 +429,7 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
-        found_underspecified_op(n);
+        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
         if (!ctx.relevancy()) {
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index c06f82c8b..e6e9e863c 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -206,7 +206,8 @@ namespace smt {
         numeral k     = ceil(get_value(v));
         rational _k   = k.to_rational();
         expr_ref bound(get_manager());
-        bound  = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
+        expr* e = get_enode(v)->get_owner();
+        bound  = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
         TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
         context & ctx = get_context();
         ctx.internalize(bound, true);
@@ -371,7 +372,7 @@ namespace smt {
         
         ctx.mk_th_axiom(get_id(), l1, l2);
        
-        TRACE("theory_arith_int", 
+        TRACE("arith_int", 
               tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n";
               );
 
@@ -1407,6 +1408,7 @@ namespace smt {
             if (m_params.m_arith_int_eq_branching && branch_infeasible_int_equality()) {
                 return FC_CONTINUE;
             }
+
             theory_var int_var = find_infeasible_int_base_var();
             if (int_var != null_theory_var) {
                 TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index a886c8a1e..ae2aa95e2 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -607,12 +607,13 @@ namespace smt {
         }
         expr_ref sum(m);
         arith_simp().mk_add(sz, args.c_ptr(), sum);
+        literal l(mk_eq(n, sum, false));
         TRACE("bv", 
               tout << mk_pp(n, m) << "\n";
               tout << mk_pp(sum, m) << "\n";
+              ctx.display_literal_verbose(tout, l); 
+              tout << "\n";
               );
-
-        literal l(mk_eq(n, sum, false));
        
         ctx.mark_as_relevant(l);
         ctx.mk_th_axiom(get_id(), 1, &l);
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 877d4f659..628eeea83 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -901,7 +901,7 @@ namespace smt {
         objective_term const& objective = m_objectives[v];
         has_shared = false;
         
-        IF_VERBOSE(1,
+        IF_VERBOSE(4,
                    for (unsigned i = 0; i < objective.size(); ++i) {
                        verbose_stream() << objective[i].second 
                                         << " * v" << objective[i].first << " ";
@@ -991,9 +991,12 @@ namespace smt {
                 if (num_nodes <= v && v < num_nodes + num_edges) {
                     unsigned edge_id = v - num_nodes;
                     literal lit = m_edges[edge_id].m_justification;
-                    get_context().literal2expr(lit, tmp);
-                    core.push_back(tmp);
+                    if (lit != null_literal) {
+                        get_context().literal2expr(lit, tmp);
+                        core.push_back(tmp);
+                    }
                 }
+                TRACE("opt", tout << core << "\n";);
             }
             for (unsigned i = 0; i < num_nodes; ++i) {
                 mpq_inf const& val = S.get_value(i);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index d5251c56b..daf5e3702 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2719,7 +2719,9 @@ bool theory_seq::can_propagate() {
 
 expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
     expr_ref result = expand(e, eqs);
+    TRACE("seq", tout << mk_pp(e, m) << " expands to " << result << "\n";);
     m_rewrite(result);
+    TRACE("seq", tout << mk_pp(e, m) << " rewrites to " << result << "\n";);
     return result;
 }
 
@@ -4469,10 +4471,11 @@ bool theory_seq::canonizes(bool sign, expr* e) {
     context& ctx = get_context();
     dependency* deps = 0;
     expr_ref cont = canonize(e, deps);
-    TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";
+          if (deps) display_deps(tout, deps););
     if ((m.is_true(cont) && !sign) ||
         (m.is_false(cont) && sign)) {
-        TRACE("seq", display(tout););
+        TRACE("seq", display(tout); tout << ctx.get_assignment(ctx.get_literal(e)) << "\n";);
         propagate_lit(deps, 0, 0, ctx.get_literal(e));
         return true;
     }
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index bd8d4958d..f84f7fe40 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -52,6 +52,7 @@ Revision History:
 
 #ifdef USE_INTRINSICS
 #include <emmintrin.h>
+#include <smmintrin.h>
 #endif
 
 hwf_manager::hwf_manager() :
diff --git a/src/util/hwf.h b/src/util/hwf.h
index cf0c9b7ea..8816e5b37 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -88,9 +88,6 @@ public:
     bool is_pzero(hwf const & x);
 
     bool is_one(hwf const & x);
-    
-    // structural eq
-    bool eq_core(hwf const & x, hwf const & y);
 
     bool eq(hwf const & x, hwf const & y);
     bool lt(hwf const & x, hwf const & y);
diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index aee84c1f0..60c85b660 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -70,6 +70,7 @@ void small_object_allocator::reset() {
 
 void small_object_allocator::deallocate(size_t size, void * p) {
     if (size == 0) return;
+
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     memory::deallocate(p);
@@ -93,6 +94,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
 
 void * small_object_allocator::allocate(size_t size) {
     if (size == 0) return 0;
+
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     return memory::allocate(size);