diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/output.h | 2 |
1 files changed, 2 insertions, 0 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; |