diff options
Diffstat (limited to 'src/util/output.cpp')
| -rw-r--r-- | src/util/output.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/output.cpp b/src/util/output.cpp index 48a7d51fd..5acee360f 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -45,7 +45,7 @@ DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout); #ifndef CVC4_MUZZLE -# ifdef CVC4_DEBUG +# if defined(CVC4_DEBUG) && defined(CVC4_TRACING) int DebugC::printf(const char* tag, const char* fmt, ...) { if(d_tags.find(string(tag)) == d_tags.end()) { @@ -77,7 +77,7 @@ int DebugC::printf(std::string tag, const char* fmt, ...) { return retval; } -# endif /* CVC4_DEBUG */ +# endif /* CVC4_DEBUG && CVC4_TRACING */ int WarningC::printf(const char* fmt, ...) { // chop off output after 1024 bytes |