diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp
index 7d54e714e..d021708fc 100644
--- a/src/smt/smt_implied_equalities.cpp
+++ b/src/smt/smt_implied_equalities.cpp
@@ -284,7 +284,7 @@ namespace smt {
         }
 
         lbool reduce_cond(model_ref& model, expr* e) {
-            expr* e1, *e2;
+            expr* e1 = 0, *e2 = 0;
             if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) {
                 if (e1 == e2) {
                     return l_true;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 7fec6f836..292d2ab0d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -689,7 +689,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;
diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index d2cd0d66c..1f0bb8473 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -70,11 +70,13 @@ struct interval {
         if (is_wrapped()) {
             // l >= b.l >= b.h >= h
             return b.is_wrapped() && h <= b.h && l >= b.l;
-        } else if (b.is_wrapped()) {
+        } 
+        else if (b.is_wrapped()) {
             // b.l > b.h >= h >= l
             // h >= l >= b.l > b.h
             return h <= b.h || l >= b.l;
-        } else {
+        } 
+        else {
             // 
             return l >= b.l && h <= b.h;
         }
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 17262a9d6..08037fe18 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -430,6 +430,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) {
     if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
         compute_depth(lhs);
         compute_depth(rhs);
+        m_trail.push_back(lhs);
+        m_trail.push_back(rhs);
         if (is_gt(lhs, rhs)) {
             TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
             m_scoped_substitution.insert(lhs, rhs, pr);
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index c62651c5c..25fb7c24f 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -146,6 +146,7 @@ class expr_substitution_simplifier : public dom_simplifier {
     expr_substitution        m_subst;
     scoped_expr_substitution m_scoped_substitution;
     obj_map<expr, unsigned>  m_expr2depth;
+    expr_ref_vector          m_trail;
 
     // move from asserted_formulas to here..
     void compute_depth(expr* e);
@@ -153,7 +154,7 @@ class expr_substitution_simplifier : public dom_simplifier {
     unsigned depth(expr* e) { return m_expr2depth[e]; }
 
 public:
-    expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {}
+    expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
     virtual ~expr_substitution_simplifier() {}
     virtual bool assert_expr(expr * t, bool sign);