diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-17 15:23:53 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-17 15:23:53 +0000 |
commit | 5a05b2c0204384032ddced67f743f48d4004f9b7 (patch) | |
tree | 6f59f5a54feb25d678139de2332f894d4b7ebfed /src/util | |
parent | d0186bbce6187def699545d072bf2f95211398cc (diff) |
Fix for the bug introduced in 1477. The stuff that was added to CVC4ostream::operator<< should only be executed when d_os != NULL. This was the cause of the NULL pointer dereference in debug builds.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/output.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/util/output.h b/src/util/output.h index dd5007747..9efb4110e 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -169,10 +169,11 @@ public: CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { if(d_os != NULL) { d_os = &(*d_os << pf); - } - if (pf == d_endl) { - for (unsigned i = 0; i < d_indent; ++ i) { - d_os = &(*d_os << '\t'); + + if (pf == d_endl) { + for (unsigned i = 0; i < d_indent; ++ i) { + d_os = &(*d_os << '\t'); + } } } return *this; |