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

diff --git a/src/base/output.h b/src/base/output.h
index 4bffad85f83e0dcf933ce3ae03d96914fec1a5a3..9d1ab03ae51c50da7080e496f025a5ec91803a87 100644 (file)
--- 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 218691bd04ccabd0fd102690d8a8e38e000f7919..66cb6e3d118340aedfafea1f4f529f244777aab8 100644 (file)
--- 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) {