diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 075aea1c5..3c149aefd 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -82,6 +82,13 @@ namespace opt {
             ~toggle_objective();
         };
 
+        class scoped_push {
+            opt_solver& s;
+        public:
+            scoped_push(opt_solver& s):s(s) { s.push();  }
+            ~scoped_push() { s.pop(1); }
+        };
+
         smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat.
         
     private:
diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp
index 6d2d7168e..8ae2cd0a4 100644
--- a/src/opt/optimize_objectives.cpp
+++ b/src/opt/optimize_objectives.cpp
@@ -46,17 +46,6 @@ Notes:
 
 namespace opt {
 
-    class scoped_push {
-        opt_solver& s;
-    public:
-        scoped_push(opt_solver& s):s(s) {
-            s.push();
-        }
-        ~scoped_push() {
-            s.pop(1);
-        }
-    };
-
     void optimize_objectives::set_cancel(bool f) {
         m_cancel = true;
     }
@@ -86,7 +75,7 @@ namespace opt {
             return is_sat;
         }
 
-        scoped_push _push(s);
+        opt_solver::scoped_push _push(s);
 
         opt_solver::toggle_objective _t(s, true);
 
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 449c79ee1..cfb49bf2d 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -216,6 +216,7 @@ namespace opt {
             ctx.register_plugin(wth);
         }
         
+        opt_solver::scoped_push _s(s);
         for (unsigned i = 0; i < soft_constraints.size(); ++i) {
             wth->assert_weighted(soft_constraints[i].get(), weights[i]);
         }