fix #6530

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/format.cpp

@@ -149,15 +149,11 @@ namespace format_ns {
     }
 
     format * mk_int(ast_manager & m, int i) {
-        char buffer[128];
+        return mk_string(m, std::to_string(i));         
-        SPRINTF_D(buffer, i);
-        return mk_string(m, buffer); 
     }
     
     format * mk_unsigned(ast_manager & m, unsigned u) {
-        char buffer[128];
+        return mk_string(m, std::to_string(u));         
-        SPRINTF_U(buffer, u);
-        return mk_string(m, buffer); 
     }
     
     format * mk_indent(ast_manager & m, unsigned i, format * f) {

src/ast/proofs/proof_checker.cpp

@@ -1245,12 +1245,8 @@ void proof_checker::dump_proof(proof const* pr) {
 }
 
 void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent) {
-    char buffer[128];
+    std::string buffer;
-#ifdef _WINDOWS
+    buffer = "proof_lemma_" + std::to_string(m_proof_lemma_id) + ".smt2";
-    sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "proof_lemma_%d.smt2", m_proof_lemma_id);
-#else
-    sprintf(buffer, "proof_lemma_%d.smt2", m_proof_lemma_id);
-#endif
     std::ofstream out(buffer);
     ast_smt_pp pp(m);
     pp.set_benchmark_name("lemma");

src/sat/smt/q_mbi.cpp

@@ -170,7 +170,9 @@ namespace q {
             add_universe_restriction(*qb);
             assert_expr(qb->mbody);
             ++m_stats.m_num_checks;
+            IF_VERBOSE(2, verbose_stream() << "(mbqi.check)\n");
             lbool r = m_solver->check_sat(0, nullptr);
+            IF_VERBOSE(2, verbose_stream() << "(mbqi.check " << r << ")\n");
             if (r == l_undef)
                 return r;
             if (r == l_true) {
@@ -212,7 +214,10 @@ namespace q {
         add_domain_eqs(mdl0, qb);
         for (; i < m_max_cex; ++i) {
             ++m_stats.m_num_checks;
-            if (l_true != m_solver->check_sat(0, nullptr))
+            IF_VERBOSE(2, verbose_stream() << "(mbqi.check)\n");
+            lbool r = m_solver->check_sat(0, nullptr);
+            IF_VERBOSE(2, verbose_stream() << "(mbqi.check " << r << ")\n");
+            if (l_true != r)
                 break;
             m_solver->get_model(mdl1);
             auto proj = solver_project(*mdl1, qb, eqs, true);

src/smt/theory_arith_pp.h

@@ -516,13 +516,8 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::display_bounds_in_smtlib() const {
-        char buffer[128];
         static int id = 0;
-#ifdef _WINDOWS
+        std::string buffer = "arith_" + std::to_string(id) + ".smt2";
-        sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "arith_%d.smt", id);
-#else
-        sprintf(buffer, "arith_%d.smt", id);
-#endif
         std::ofstream out(buffer);
         display_bounds_in_smtlib(out);
         out.close();

src/util/debug.cpp

@@ -77,7 +77,7 @@ bool is_debug_enabled(const char * tag) {
 
 #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
 void invoke_gdb() {
-    char buffer[1024];
+    std::string buffer;
     int * x = nullptr;
     for (;;) {
         std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
@@ -101,9 +101,9 @@ void invoke_gdb() {
             throw default_exception("assertion violation");
         case 'G':
         case 'g':
-            sprintf(buffer, "gdb -nw /proc/%d/exe %d", getpid(), getpid());
+            buffer = "gdb -nw /proc/" + std::to_string(getpid()) + "/exe " + std::to_string(getpid());
             std::cerr << "invoking GDB...\n";
-            if (system(buffer) == 0) {
+            if (system(buffer.c_str()) == 0) {
                 std::cerr << "continuing the execution...\n";
             }
             else {