From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Fri, 12 Feb 2010 20:26:56 +0000 (+0000)
Subject: Fix to compile out Debug(...) << ... statements in optimized mode. Someone please... 
X-Git-Tag: cvc5-1.0.0~9257
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42bd7611c9a09b4458fbc1076606850628880f3a;p=cvc5.git

Fix to compile out Debug(...) << ... statements in optimized mode. Someone please look to see if it makes sense.
---

diff --git a/src/util/output.h b/src/util/output.h
index 8ba1ea26b..f897fd1ca 100644
--- 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 {