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/options.h | |
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/options.h')
0 files changed, 0 insertions, 0 deletions