diff options
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 6cbaae4cb..1ca0e9b35 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -654,7 +654,7 @@ public: l = options::defaultExprDepth(); } if(l == 0) { - l = s_defaultPrintDepth; + return s_defaultPrintDepth; } } return l; @@ -706,12 +706,6 @@ class CVC4_PUBLIC ExprPrintTypes { static const int s_iosIndex; /** - * The default printtypes setting, for ostreams that haven't yet had a - * printtypes() applied to them. - */ - static const int s_defaultPrintTypes = false; - - /** * When this manipulator is used, the setting is stored here. */ bool d_printTypes; @@ -882,8 +876,10 @@ public: if(l <= 0 || l > language::output::LANG_MAX) { // if called from outside the library, we may not have options // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable. - l = s_defaultOutputLanguage + 1; + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. + return OutputLanguage(s_defaultOutputLanguage); } } return OutputLanguage(l - 1); |