Merge branch '1.0.x'

Conflicts:
	src/theory/quantifiers/theory_quantifiers.cpp

3 files changed, 19 insertions, 5 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index b353ec5dc..f5df63f8c 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -654,6 +654,11 @@ public:
         l = options::defaultExprDepth();
       }
       if(l == 0) {
+        // 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, but
+        // don't set "l" since that would make it "sticky" for this
+        // stream.
         return s_defaultPrintDepth;
       }
     }
@@ -797,7 +802,17 @@ public:
     if(l == 0) {
       // set the default dag setting on this ostream
       // (offset by one to detect whether default has been set yet)
-      l = s_defaultDag + 1;
+      if(&Options::current() != NULL) {
+        l = options::defaultDagThresh() + 1;
+      }
+      if(l == 0) {
+        // 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, but
+        // don't set "l" since that would make it "sticky" for this
+        // stream.
+        return s_defaultDag + 1;
+      }
     }
     return static_cast<size_t>(l - 1);
   }
diff --git a/src/expr/options b/src/expr/options
index cd59e4875..223189d1b 100644
--- a/src/expr/options
+++ b/src/expr/options
@@ -5,9 +5,9 @@
 
 module EXPR "expr/options.h" Expression package
 
-option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
+option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
  print exprs to depth N (0 == default, -1 == no limit)
-option - default-dag-thresh --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h"
+option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h"
  dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
 option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
  print types with variables when printing exprs
diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h
index 7a1d73c36..57c4d1aa4 100644
--- a/src/expr/options_handlers.h
+++ b/src/expr/options_handlers.h
@@ -39,8 +39,7 @@ inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) {
   // intentionally exclude Dump stream from this list
 }
 
-inline void setDefaultDagThresh(std::string option, std::string optarg, SmtEngine* smt) {
-  int dag = atoi(optarg.c_str());
+inline void setDefaultDagThresh(std::string option, int dag, SmtEngine* smt) {
   if(dag < 0) {
     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
   }