Fix to compile out Debug(...) << ... statements in optimized mode. Someone please...

diff --git a/src/util/output.h b/src/util/output.h
index 8ba1ea26b527c0483593d53301ddf6c017d413a7..f897fd1cac8a901b530962e82d65536ceb9e6cc5 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -90,7 +90,12 @@ public:
 };/* class Debug */
 
 /** The debug output singleton */
-extern DebugC Debug CVC4_PUBLIC;
+extern DebugC DebugOut CVC4_PUBLIC;
+#ifdef CVC4_DEBUG
+  #define Debug DebugOut
+#else
+  #define Debug if(0) DebugOut
+#endif
 
 /** The warning output class */
 class CVC4_PUBLIC WarningC {