diff options
| author | Tim King <taking@google.com> | 2016-02-01 11:25:29 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-02-01 11:25:29 -0800 |
| commit | 52685068705546798b0a4d8204b10b848213975a (patch) | |
| tree | 0e3de3d9959c8c6c4c3b780b5028e3bfb379f2a9 /src | |
| parent | cbfd4e87765b716e8d21bd115f5917edef63f8a4 (diff) | |
Fixing a potentially malformed template expansion when Dump() is disabled.
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/output.h | 2 | ||||
| -rw-r--r-- | src/smt_util/dump.cpp | 6 |
2 files changed, 5 insertions, 3 deletions
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) { |