diff --git a/src/ast/simplifiers/dominator_simplifier.cpp b/src/ast/simplifiers/dominator_simplifier.cpp
index 12f2e2941..2ef4528ab 100644
--- a/src/ast/simplifiers/dominator_simplifier.cpp
+++ b/src/ast/simplifiers/dominator_simplifier.cpp
@@ -41,7 +41,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
             if (is_subexpr(child, t) && !is_subexpr(child, e)) 
                 simplify_rec(child);            
         
-        pop(scope_level() - old_lvl);
+        local_pop(scope_level() - old_lvl);
         expr_ref new_t = simplify_arg(t);
         reset_cache();
         if (!assert_expr(new_c, true)) {
@@ -50,7 +50,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
         for (expr * child : tree(ite)) 
             if (is_subexpr(child, e) && !is_subexpr(child, t)) 
                 simplify_rec(child);
-        pop(scope_level() - old_lvl);
+        local_pop(scope_level() - old_lvl);
         expr_ref new_e = simplify_arg(e);
 
         if (c == new_c && t == new_t && e == new_e) {
@@ -159,7 +159,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
         r = simplify_arg(arg);                              
         args.push_back(r);                                  
         if (!assert_expr(r, !is_and)) {                     
-            pop(scope_level() - old_lvl);                   
+            local_pop(scope_level() - old_lvl);                   
             r = is_and ? m.mk_false() : m.mk_true();        
             reset_cache();
             return true;
@@ -181,7 +181,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
         args.reverse();
     }
     
-    pop(scope_level() - old_lvl);
+    local_pop(scope_level() - old_lvl);
     reset_cache();
     return { is_and ? mk_and(args) : mk_or(args), m };
 }
@@ -191,7 +191,7 @@ expr_ref dominator_simplifier::simplify_not(app * e) {
     ENSURE(m.is_not(e, ee));
     unsigned old_lvl = scope_level();
     expr_ref t = simplify_rec(ee);
-    pop(scope_level() - old_lvl);
+    local_pop(scope_level() - old_lvl);
     reset_cache();
     return mk_not(t);
 }
@@ -245,7 +245,7 @@ void dominator_simplifier::reduce() {
             }
             m_fmls.update(i, dependent_expr(m, r, new_pr, d));
         }
-        pop(scope_level());
+        local_pop(scope_level());
 
         // go backwards
         m_forward = false;
@@ -268,7 +268,7 @@ void dominator_simplifier::reduce() {
             }
             m_fmls.update(i, dependent_expr(m, r, new_pr, d));
         }
-        pop(scope_level());
+        local_pop(scope_level());
     }
     SASSERT(scope_level() == 0);
 }
diff --git a/src/ast/simplifiers/dominator_simplifier.h b/src/ast/simplifiers/dominator_simplifier.h
index 562aeace1..b412f6db0 100644
--- a/src/ast/simplifiers/dominator_simplifier.h
+++ b/src/ast/simplifiers/dominator_simplifier.h
@@ -48,7 +48,7 @@ class dominator_simplifier : public dependent_expr_simplifier {
     expr* idom(expr *e) const { return m_dominators.idom(e); }
 
     unsigned scope_level() { return m_simplifier->scope_level(); }
-    void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
+    void local_pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
     bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); }
 
 
diff --git a/src/ast/substitution/demodulator_rewriter.cpp b/src/ast/substitution/demodulator_rewriter.cpp
index c25647c01..f174b1491 100644
--- a/src/ast/substitution/demodulator_rewriter.cpp
+++ b/src/ast/substitution/demodulator_rewriter.cpp
@@ -780,7 +780,6 @@ void demodulator_rewriter::operator()(expr_ref_vector const& exprs,
 
 
 demodulator_match_subst::demodulator_match_subst(ast_manager & m):
-    m(m),
     m_subst(m) {
 }
 
diff --git a/src/ast/substitution/demodulator_rewriter.h b/src/ast/substitution/demodulator_rewriter.h
index 3a1e442d5..8a1e6feb5 100644
--- a/src/ast/substitution/demodulator_rewriter.h
+++ b/src/ast/substitution/demodulator_rewriter.h
@@ -111,7 +111,6 @@ class demodulator_match_subst {
     typedef std::pair<expr *, expr *>      expr_pair;
     typedef obj_pair_hashtable<expr, expr> cache;
     
-    ast_manager &         m;
     substitution          m_subst;
     cache                 m_cache;
     svector<expr_pair>    m_todo;