diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp
index 89ed6da05..06302ab6f 100644
--- a/src/ast/simplifiers/bound_simplifier.cpp
+++ b/src/ast/simplifiers/bound_simplifier.cpp
@@ -208,6 +208,8 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
             assert_upper(x, n - k, true);
         
     }
+
+
     // x != k, k <= x -> k < x
     if (m.is_not(f, f) && m.is_eq(f, x, y)) {
         if (a.is_numeral(x))
@@ -222,6 +224,7 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
                 assert_upper(x, n, true);
         }
     }
+
 }
 
 void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
@@ -449,6 +452,7 @@ void bound_simplifier::reset() {
     bp.reset();
     m_var2expr.reset();
     m_expr2var.reset();
+    m_trail.reset();
 }
 
 #if 0
diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h
index 6977261c5..7950f418b 100644
--- a/src/ast/simplifiers/bound_simplifier.h
+++ b/src/ast/simplifiers/bound_simplifier.h
@@ -40,6 +40,7 @@ class bound_simplifier : public dependent_expr_simplifier {
     dep_intervals           m_interval;
     ptr_vector<expr>        m_var2expr;
     unsigned_vector         m_expr2var;
+    expr_ref_vector         m_trail;
     mpq_buffer              m_num_buffer;
     var_buffer              m_var_buffer;
     unsigned                m_num_reduced = 0;
@@ -71,6 +72,7 @@ class bound_simplifier : public dependent_expr_simplifier {
             if (e != core_e)
                 m_expr2var.setx(core_e->get_id(), v, UINT_MAX);
             m_var2expr.push_back(core_e);
+            m_trail.push_back(e);
         }
         return v;
     }
@@ -100,6 +102,7 @@ public:
         m_rewriter(m),
         bp(nm, m_alloc, p),
         m_interval(m.limit()),
+        m_trail(m),
         m_num_buffer(nm) {
         updt_params(p);
     }