diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 429a7ec2b..4add216ce 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Theory plugins
+    Theory plugin base classes
 
 Author:
 
@@ -26,12 +26,30 @@ namespace euf {
         ctx(ctx)
     {}
 
+    theory_var th_euf_solver::mk_var(enode * n) {
+        SASSERT(!is_attached_to_var(n));
+        euf::theory_var v = m_var2enode.size();
+        m_var2enode.push_back(n);
+        return v;
+    }
+
+    bool th_euf_solver::is_attached_to_var(enode* n) const {
+        theory_var v = n->get_th_var(get_id());
+        return v != null_theory_var && get_enode(v) == n;
+    }
+
     theory_var th_euf_solver::get_th_var(expr* e) const {
         return get_th_var(ctx.get_enode(e));
     }
     
+    void th_euf_solver::push() {
+        m_var2enode_lim.push_back(m_var2enode.size());
+    }
 
-
-
+    void th_euf_solver::pop(unsigned num_scopes) {
+        unsigned new_lvl = m_var2enode_lim.size() - num_scopes;
+        m_var2enode.shrink(m_var2enode_lim[new_lvl]);
+        m_var2enode_lim.shrink(new_lvl);
+    }
 
 }
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index fe5650db5..03617bc63 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -93,28 +93,17 @@ namespace euf {
         euf::enode_vector   m_var2enode;
         unsigned_vector     m_var2enode_lim;
     public:
+        th_euf_solver(euf::solver& ctx, euf::theory_id id);
         virtual ~th_euf_solver() {}
-
-        th_euf_solver(euf::solver& ctx, euf::theory_id id);           
-
-        virtual euf::theory_var mk_var(enode * n) {
-            SASSERT(!is_attached_to_var(n));
-            euf::theory_var v = m_var2enode.size();
-            m_var2enode.push_back(n);
-            return v;
-        }
-
+        virtual theory_var mk_var(enode * n);
         unsigned get_num_vars() const { return m_var2enode.size();}
         enode* get_enode(theory_var v) const { return m_var2enode[v]; }
         expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); }
         theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
         theory_var get_th_var(expr* e) const;
-
-        bool is_attached_to_var(enode* n) const {
-            theory_var v = n->get_th_var(get_id());
-            return v != null_theory_var && get_enode(v) == n;
-        }
-
+        bool is_attached_to_var(enode* n) const;
+        void push() override;
+        void pop(unsigned n) override;
     };