diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 4d90ccfb0..cc50c1a8c 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -363,7 +363,7 @@ public:
         return expr_has_bounds(t);
     }
 
-    virtual void push() {
+    void push() {
         TRACE("bv", tout << "push\n";);
         unsigned sz = m_scopes.size();
         m_scopes.resize(sz + 1);
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index f127614aa..1cda9cc6f 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -36,7 +36,7 @@ public:
     virtual ~ctx_propagate_assertions() {}
     virtual bool assert_expr(expr * t, bool sign);
     virtual bool simplify(expr* t, expr_ref& result);
-    virtual void push();
+    void push();
     virtual void pop(unsigned num_scopes);
     virtual unsigned scope_level() const { return m_scopes.size(); }
     virtual simplifier * translate(ast_manager & m);
@@ -260,10 +260,6 @@ struct ctx_simplify_tactic::imp {
         return m_simp->scope_level();
     }
 
-    void push() { 
-        m_simp->push();
-    }
-
     void restore_cache(unsigned lvl) {
         if (lvl >= m_cache_undo.size())
             return;
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index 7b1507f67..d6ebf5cbd 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -31,7 +31,6 @@ public:
         virtual bool assert_expr(expr * t, bool sign) = 0;
         virtual bool simplify(expr* t, expr_ref& result) = 0;
         virtual bool may_simplify(expr* t) { return true; }
-        virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
         virtual simplifier * translate(ast_manager & m) = 0;
         virtual unsigned scope_level() const = 0;