Ensure that Z3 uses the correct SMT-LIB2 syntax for push and pop (#4495)

* When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'push'

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

* When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'pop'

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

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());
     }

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";
             }
         }
     }

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";
     }
 }
 

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";
     }
 

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;

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";
     }
 
 };