build fix

diff --git a/src/util/output.cpp b/src/util/output.cpp
index 01a485136ca4f697ff5501d03f05dffbe7b5e438..fdc54d9b5a640c02c64009d71fe5fd587b98c3db 100644 (file)
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -25,7 +25,7 @@ namespace CVC4 {
 null_streambuf null_sb;
 std::ostream null_os(&null_sb);
 
-DebugC   Debug  (&std::cout);
+DebugC   DebugOut  (&std::cout);
 WarningC Warning(&std::cerr);
 MessageC Message(&std::cout);
 NoticeC  Notice (&std::cout);