change detection/handling of output language more reasonably; fixes a nagging bug Tim found in API examples

(this commit was certified error- and warning-free by the test-and-commit script.)

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);