fix to production build

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 03678e30e5c5fcebbfff1031f9de61bfe382172e..096c99c0633f4e7887a986749c451899ef593e8c 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -416,8 +416,8 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
        * in the cache to make sure they are the same.  This is
        * especially necessary if a theory post-rewrites something into
        * a term of another theory. */
-      if(Debug.isOn("extra-checking") &&
-         !Debug.isOn("$extra-checking:inside-rewrite")) {
+      if(debugTagIsOn("extra-checking") &&
+         !debugTagIsOn("$extra-checking:inside-rewrite")) {
         ScopedDebug d("$extra-checking:inside-rewrite");
         Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel);
         Assert(rewrittenAgain == rse.d_node,

diff --git a/src/util/output.h b/src/util/output.h
index 87b7f69a61bba262a6602b9c26090a84a365a8c3..851868c15e5bd8c1478f114fdf4a46928ae1ca81 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -127,41 +127,6 @@ extern DebugC DebugOut CVC4_PUBLIC;
 #  define Debug if(0) debugNullCvc4Stream
 #endif /* CVC4_DEBUG */
 
-class CVC4_PUBLIC ScopedDebug {
-  std::string d_tag;
-  bool d_oldSetting;
-
-public:
-
-  ScopedDebug(std::string tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Debug.isOn(d_tag);
-    if(newSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-
-  ScopedDebug(const char* tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Debug.isOn(d_tag);
-    if(newSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-
-  ~ScopedDebug() {
-    if(d_oldSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-};/* class ScopedDebug */
-
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
   std::ostream *d_os;
@@ -321,6 +286,55 @@ extern TraceC TraceOut CVC4_PUBLIC;
 #  define Trace if(0) debugNullCvc4Stream
 #endif /* CVC4_TRACING */
 
+#ifdef CVC4_DEBUG
+
+class CVC4_PUBLIC ScopedDebug {
+  std::string d_tag;
+  bool d_oldSetting;
+
+public:
+
+  ScopedDebug(std::string tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = DebugOut.isOn(d_tag);
+    if(newSetting) {
+      DebugOut.on(d_tag);
+    } else {
+      DebugOut.off(d_tag);
+    }
+  }
+
+  ScopedDebug(const char* tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Debug.isOn(d_tag);
+    if(newSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+
+  ~ScopedDebug() {
+    if(d_oldSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+};/* class ScopedDebug */
+
+#else /* CVC4_DEBUG */
+
+class CVC4_PUBLIC ScopedDebug {
+public:
+  ScopedDebug(std::string tag, bool newSetting = true) {}
+  ScopedDebug(const char* tag, bool newSetting = true) {}
+};/* class ScopedDebug */
+
+#endif /* CVC4_DEBUG */
+
+#ifdef CVC4_TRACING
+
 class CVC4_PUBLIC ScopedTrace {
   std::string d_tag;
   bool d_oldSetting;
@@ -356,6 +370,16 @@ public:
   }
 };/* class ScopedTrace */
 
+#else /* CVC4_TRACING */
+
+class CVC4_PUBLIC ScopedTrace {
+public:
+  ScopedTrace(std::string tag, bool newSetting = true) {}
+  ScopedTrace(const char* tag, bool newSetting = true) {}
+};/* class ScopedTrace */
+
+#endif /* CVC4_TRACING */
+
 #else /* ! CVC4_MUZZLE */
 
 #  define Debug if(0) debugNullCvc4Stream