STP: Eliminate use of non-standard variadic macro.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100392 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 10 insertions, 11 deletions

diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp
index 13a9ae08..9761c719 100644
--- a/stp/sat/Solver.cpp
+++ b/stp/sat/Solver.cpp
@@ -768,24 +768,26 @@ bool Solver::solve(const vec<Lit>& assumps)
     assumps.copyTo(assumptions);
 
     if (verbosity >= 1){
-        reportf("==================================[MINISAT]====================================\n");
-        reportf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
-        reportf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
-        reportf("===============================================================================\n");
+        printf("==================================[MINISAT]====================================\n");
+        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
+        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
+        printf("===============================================================================\n");
     }
 
     // Search:
     while (status == l_Undef){
         if (verbosity >= 1)
-            //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
-            reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+            //printf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+            printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
         status = search((int)nof_conflicts, (int)nof_learnts);
         nof_conflicts *= params.restart_inc;
         nof_learnts   *= params.learntsize_inc;
     }
 
-    if (verbosity >= 1)
-        reportf("==============================================================================\n");
+    if (verbosity >= 1) {
+        printf("==============================================================================\n");
+        fflush(stdout);
+    }
 
     if (status == l_True){
         // Copy model:
diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h
index 8826fac7..0a6dc87e 100644
--- a/stp/sat/Solver.h
+++ b/stp/sat/Solver.h
@@ -24,9 +24,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "VarOrder.h"
 
 namespace MINISAT {
-// Redfine if you want output to go somewhere else:
-#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) )
-
 
 //=================================================================================================
 // Solver -- the main class: