diff options
| author | Daniel Dunbar <daniel@zuster.org> | 2010-04-05 04:01:56 +0000 |
|---|---|---|
| committer | Daniel Dunbar <daniel@zuster.org> | 2010-04-05 04:01:56 +0000 |
| commit | 1efbeceedbb00267f38d0dfc9b24307ad3e1feca (patch) | |
| tree | d6b9ac96dd6331b48982b0afe9759fe1e06cafba /stp/AST | |
| parent | eaa01d355abd0e69bfec9d5b61f1330f42ff1fe8 (diff) | |
| download | klee-1efbeceedbb00267f38d0dfc9b24307ad3e1feca.tar.gz | |
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
Diffstat (limited to 'stp/AST')
| -rw-r--r-- | stp/AST/ToSAT.cpp | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp index 29635ec5..ed8f1761 100644 --- a/stp/AST/ToSAT.cpp +++ b/stp/AST/ToSAT.cpp @@ -121,15 +121,16 @@ namespace BEEV { return; double cpu_time = MINISAT::cpuTime(); MINISAT::int64 mem_used = MINISAT::memUsed(); - reportf("restarts : %"I64_fmt"\n", s.starts); - reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); - reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); - reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); - reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", - s.tot_literals, - (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); - if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); - reportf("CPU time : %g s\n", cpu_time); + printf("restarts : %"I64_fmt"\n", s.starts); + printf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); + printf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); + printf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); + printf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", + s.tot_literals, + (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); + if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used / 1048576.0); + printf("CPU time : %g s\n", cpu_time); + fflush(stdout); } // Prints Satisfying assignment directly, for debugging. |