diff options
| -rw-r--r-- | examples/api/Makefile | 4 | ||||
| -rw-r--r-- | src/expr/expr_template.h | 14 |
2 files changed, 9 insertions, 9 deletions
diff --git a/examples/api/Makefile b/examples/api/Makefile new file mode 100644 index 000000000..8e5dcfd21 --- /dev/null +++ b/examples/api/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = examples/api + +include $(topdir)/Makefile.subdir 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); |