diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp
index 572d5e8d5..c8a489d69 100644
--- a/src/muz/rel/karr_relation.cpp
+++ b/src/muz/rel/karr_relation.cpp
@@ -111,8 +111,8 @@ namespace datalog {
 
         void filter_interpreted(app* cond) {
             rational one(1), mone(-1);
-            expr* e1, *e2, *en;
-            var* v, *w;
+            expr* e1 = 0, *e2 = 0, *en = 0;
+            var* v = 0, *w = 0;
             rational n1, n2;
             expr_ref_vector conjs(m);
             flatten_and(cond, conjs);
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index 30505a5e8..7bd35b4ef 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -398,8 +398,8 @@ namespace datalog {
     }
 
     bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) {
-      if (!m_context.get_params ().xform_tail_simplifier_pve ())
-        return false;
+        if (!m_context.get_params ().xform_tail_simplifier_pve ())
+            return false;
         unsigned u_len = r->get_uninterpreted_tail_size();
         unsigned len = r->get_tail_size();
         if (u_len == len) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0bb76cd90..7fec6f836 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -721,7 +721,7 @@ namespace smt {
             SASSERT(!ctx().b_internalized(atom));
             bool_var bv = ctx().mk_bool_var(atom);
             ctx().set_var_theory(bv, get_id());
-            expr* n1, *n2;
+            expr* n1 = 0, *n2 = 0;
             rational r;
             lra_lp::bound_kind k;
             theory_var v = null_theory_var;
@@ -862,7 +862,7 @@ namespace smt {
 
         void relevant_eh(app* n) {
             TRACE("arith", tout << mk_pp(n, m) << "\n";);
-            expr* n1, *n2;
+            expr* n1 = 0, *n2 = 0;
             if (a.is_mod(n, n1, n2))
                 mk_idiv_mod_axioms(n1, n2);
             else if (a.is_rem(n, n1, n2))
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index bba27cf46..17262a9d6 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -90,8 +90,8 @@ void expr_dominators::compute_dominators() {
     bool change = true;
     while (change) {
         change = false;
-        SASSERT(m_post2expr.back() == e);
-        for (unsigned i = 0; i < m_post2expr.size() - 1; ++i) {
+        SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
+        for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
             expr * child = m_post2expr[i];
             ptr_vector<expr> const& p = m_parents[child];
             SASSERT(!p.empty());
@@ -167,7 +167,6 @@ void dom_simplify_tactic::operator()(
 void dom_simplify_tactic::cleanup() {
     m_trail.reset();
     m_args.reset();
-    m_args2.reset();
     m_result.reset();
     m_dominators.reset();
 }
@@ -180,9 +179,11 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
     expr_ref new_c = simplify(c);
     if (m.is_true(new_c)) {
         r = simplify(t);
-    } else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
+    } 
+    else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
         r = simplify(e);
-    } else {
+    } 
+    else {
         for (expr * child : tree(ite)) {
             if (is_subexpr(child, t) && !is_subexpr(child, e)) {
                 simplify(child);
@@ -254,6 +255,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
     cache(e0, r);
     TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
     --m_depth;
+    m_subexpr_cache.reset();
     return r;
 }
 
@@ -361,7 +363,7 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
             return true;
         }
     }
-    m_subexpr_cache.insert(a, b, false);
+    m_subexpr_cache.insert(a, b, false);   
     return false;
 }
 
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 825a173bf..c62651c5c 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -88,7 +88,7 @@ private:
     ast_manager&         m;
     dom_simplifier*      m_simplifier;
     params_ref           m_params;
-    expr_ref_vector      m_trail, m_args, m_args2;
+    expr_ref_vector      m_trail, m_args;
     obj_map<expr, expr*> m_result;
     expr_dominators      m_dominators;
     unsigned             m_scope_level;
@@ -120,7 +120,7 @@ private:
 public:
     dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
         m(m), m_simplifier(s), m_params(p), 
-        m_trail(m), m_args(m), m_args2(m), 
+        m_trail(m), m_args(m), 
         m_dominators(m), 
         m_scope_level(0), m_depth(0), m_max_depth(1024) {}