diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index de4d3732f..596ba011d 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -61,7 +61,7 @@ extern "C" {
     }
 
     void solver2smt2_pp::push() {
-        m_out << "(push)\n";
+        m_out << "(push 1)\n";
         m_pp_util.push();
         m_tracked_lim.push_back(m_tracked.size());
     }
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index c9252eece..707167e17 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -1231,14 +1231,14 @@ namespace datalog {
         }
         else {
             for (unsigned i = 0; i < queries.size(); ++i) {
-                if (queries.size() > 1) out << "(push)\n";
+                if (queries.size() > 1) out << "(push 1)\n";
                 out << "(assert ";
                 expr_ref q(m);
                 q = m.mk_not(queries[i].get());
                 PP(q);
                 out << ")\n";
                 out << "(check-sat)\n";
-                if (queries.size() > 1) out << "(pop)\n";
+                if (queries.size() > 1) out << "(pop 1)\n";
             }
         }
     }
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index 61fd9447d..f560ef4dd 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -141,12 +141,12 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector<datalog::
 
     out << to_string() << "\n";
     for (auto* r : rules) {
-        out << "(push)\n";
+        out << "(push 1)\n";
         out << "(assert (not\n";
         rm.display_smt2(*r, out);
         out << "))\n";
         out << "(check-sat)\n";
-        out << "(pop)\n";
+        out << "(pop 1)\n";
     }
 }
 
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 5fd77f8cb..68974fb56 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -124,13 +124,13 @@ namespace spacer {
         out << "(define-fun mbp_benchmark_fml () Bool\n  ";
         out << mk_pp(fml, m) << ")\n\n";
 
-        out << "(push)\n"
+        out << "(push 1)\n"
             << "(assert mbp_benchmark_fml)\n"
             << "(check-sat)\n"
             << "(mbp mbp_benchmark_fml (";
         for (auto v : vars) {out << mk_pp(v, m) << " ";}
         out << "))\n"
-            << "(pop)\n"
+            << "(pop 1)\n"
             << "(exit)\n";
     }
 
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index b033e6767..88009358d 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1208,9 +1208,9 @@ namespace qe {
                 fml = mk_not(m, m.mk_iff(q, fml));
                 ast_smt_pp pp(m);
                 out << "; eliminate " << mk_pp(m_var, m) << "\n";
-                out << "(push)\n";
+                out << "(push 1)\n";
                 pp.display_smt2(out, fml);                
-                out << "(pop)\n\n";      
+                out << "(pop 1)\n\n";
 #if 0
                 DEBUG_CODE(
                     smt_params params;
diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp
index bff5c3809..3188b1a6a 100644
--- a/src/test/theory_pb.cpp
+++ b/src/test/theory_pb.cpp
@@ -90,7 +90,7 @@ private:
     void fuzz_round(unsigned& num_rounds, unsigned lvl) {
         unsigned num_rounds2 = 0;
         lbool is_sat = l_true;    
-        std::cout << "(push)\n";
+        std::cout << "(push 1)\n";
         ctx.push();
         unsigned r = 0;
         while (is_sat == l_true && r <= num_rounds + 1) {
@@ -105,7 +105,7 @@ private:
         num_rounds = r;
         std::cout << "; number of rounds: " << num_rounds << " level: " << lvl << "\n";
         ctx.pop(1);
-        std::cout << "(pop)\n";
+        std::cout << "(pop 1)\n";
     }
 
 };