1 files changed, 2 insertions, 90 deletions
diff --git a/src/base/output.h b/src/base/output.h
index 7bfae7bca..9ae5ad8db 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -357,82 +357,6 @@ class __cvc5_true
   inline operator bool() { return true; }
 }; /* __cvc5_true */
 
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-
-class 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() {
-    if(d_oldSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-}; /* class ScopedDebug */
-
-#else /* CVC5_DEBUG && CVC5_TRACING */
-
-class ScopedDebug
-{
- public:
-  ScopedDebug(std::string tag, bool newSetting = true) {}
-}; /* class ScopedDebug */
-
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-
-#ifdef CVC5_TRACING
-
-class ScopedTrace
-{
-  std::string d_tag;
-  bool d_oldSetting;
-
-public:
-
-  ScopedTrace(std::string tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Trace.isOn(d_tag);
-    if(newSetting) {
-      Trace.on(d_tag);
-    } else {
-      Trace.off(d_tag);
-    }
-  }
-
-  ~ScopedTrace() {
-    if(d_oldSetting) {
-      Trace.on(d_tag);
-    } else {
-      Trace.off(d_tag);
-    }
-  }
-}; /* class ScopedTrace */
-
-#else /* CVC5_TRACING */
-
-class ScopedTrace
-{
- public:
-  ScopedTrace(std::string tag, bool newSetting = true) {}
-}; /* class ScopedTrace */
-
-#endif /* CVC5_TRACING */
-
 /**
  * Pushes an indentation level on construction, pop on destruction.
  * Useful for tracing recursive functions especially, but also can be
@@ -442,23 +366,11 @@ class ScopedTrace
 class IndentedScope
 {
   Cvc5ostream d_out;
-
  public:
-  inline IndentedScope(Cvc5ostream out);
-  inline ~IndentedScope();
+  inline IndentedScope(Cvc5ostream out) : d_out(out) { d_out << push; }
+  inline ~IndentedScope() { d_out << pop; }
 }; /* class IndentedScope */
 
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-inline IndentedScope::IndentedScope(Cvc5ostream out) : d_out(out)
-{
-  d_out << push;
-}
-inline IndentedScope::~IndentedScope() { d_out << pop; }
-#else  /* CVC5_DEBUG && CVC5_TRACING */
-inline IndentedScope::IndentedScope(Cvc5ostream out) {}
-inline IndentedScope::~IndentedScope() {}
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-
 }  // namespace cvc5
 
 #endif /* CVC5__OUTPUT_H */