Fix for the bug introduced in 1477. The stuff that was added to CVC4ostream::operato...
authorTim King <taking@cs.nyu.edu>
Thu, 17 Mar 2011 15:23:53 +0000 (15:23 +0000)
committerTim King <taking@cs.nyu.edu>
Thu, 17 Mar 2011 15:23:53 +0000 (15:23 +0000)
commit5a05b2c0204384032ddced67f743f48d4004f9b7
tree6f59f5a54feb25d678139de2332f894d4b7ebfed
parentd0186bbce6187def699545d072bf2f95211398cc
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.
src/util/output.h