From: Tim King <taking@google.com>
Date: Mon, 1 Feb 2016 19:25:29 +0000 (-0800)
Subject: Fixing a potentially malformed template expansion when Dump() is disabled.
X-Git-Tag: cvc5-1.0.0~6094
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52685068705546798b0a4d8204b10b848213975a;p=cvc5.git

Fixing a potentially malformed template expansion when Dump() is disabled.
---

diff --git a/src/base/output.h b/src/base/output.h
index 4bffad85f..9d1ab03ae 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -110,6 +110,8 @@ public:
   bool isConnected() { return d_os != NULL; }
   operator std::ostream&() { return isConnected() ? *d_os : null_os; }
 
+  std::ostream* getStreamPointer() { return d_os; }
+
   template <class T>
   CVC4ostream& operator<<(T const& t) CVC4_PUBLIC;
 
diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp
index 218691bd0..66cb6e3d1 100644
--- a/src/smt_util/dump.cpp
+++ b/src/smt_util/dump.cpp
@@ -22,11 +22,11 @@ namespace CVC4 {
 DumpC DumpChannel CVC4_PUBLIC;
 
 std::ostream& DumpC::setStream(std::ostream* os) {
-  DumpOut.setStream(os);
+  ::CVC4::DumpOutChannel.setStream(os);
   return *os;
 }
-std::ostream& DumpC::getStream() { return DumpOut.getStream(); }
-std::ostream* DumpC::getStreamPointer() { return DumpOut.getStreamPointer(); }
+std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); }
+std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); }
 
 
 void DumpC::setDumpFromString(const std::string& optarg) {