Bugs resolved by this commit: #314, #322, #359, #364, #365.

See below for details.

* Fix the "assert" name-collision bug (resolves bug #364).

  Our identifiers should never be named "assert", as that's a preprocessor
  definition in <assert.h>, which is often #included indirectly (so simply
  having a policy of not including <assert.h> isn't good enough---one of
  our dependences might include it).  It was once the case that we didn't
  have anything named "assert", but "assert()" has now crept back in.
  Instead, name things "assertFoo()" or similar.  Thanks to Tim for the
  report.

  To fix this, I've changed some of Dejan's circuit-propagator code from
  "assert()" to "assertTrue()".  Ditto for Andy's explanation manager.
  Guys, if you prefer a different name in your code, please change it.

* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
  Inner lets now shadow outer lets (previously, they incorrectly gave an
  error).  Additionally, while looking at this, I found that a sequential let
  was implemented rather than a parallel let.  This is now fixed.  Thanks to
  Liana for the report.

* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).

* There were a lot of Debug lines in bitvectors that had embedded toString()
  calls.  This wasted a LOT of time in debug builds for BV benchmarks
  (like in "make regress").  Added if(Debug.isOn(...)) guards; much faster
  now.

* Support for building public-facing interface documentation only (as opposed
  to all internals documentation).  Now "make doc" does the public-facing and
  "make doc-internals" does documentation of everything.  (Along with changes
  to the nightly build script---which will now build and publish both types
  of Doxygen documentation---this resolves bug #359).

* Fix the lambda typechecking bug (resolves bug #322).  Thanks to Andy for the
  report (a long long time ago--sorry).

* The default output language for all streams is now based on the current set
  of Options (if there is one).  This has been a constant annoyance, especially
  when stringstreams are used to construct output.  However, it doesn't work
  for calls from outside the library, so it's mainly an annoyance-fixer for
  CVC4 library code itself.

* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
  are used only in assertions-enabled builds (and thus give warnings in
  production builds).  This was briefly discussed at the meeting this week.

31 files changed, 256 insertions, 102 deletions

diff --git a/Makefile b/Makefile
index 5b1acecbd..86a04dc3e 100644
--- a/Makefile
+++ b/Makefile
@@ -34,8 +34,9 @@ distclean maintainerclean:
 .PHONY: test
 test: check
 
-.PHONY: doc
+.PHONY: doc doc-internals
 doc: doc-builds
+doc-internals: doc-internals-builds
 
 .PHONY: examples
 examples: all
diff --git a/Makefile.builds.in b/Makefile.builds.in
index 96dc8d3cf..dd2a394ae 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -22,6 +22,8 @@ include current
 @SET_MAKE@
 
 # Set up some basic autoconf make vars
+srcdir = @srcdir@
+builddir = @builddir@
 install_sh = @install_sh@
 mkinstalldirs = $(install_sh) -d
 exec_prefix = @exec_prefix@
@@ -213,7 +215,9 @@ TAGS tags:
 
 .PHONY: doc-builds doc-prereq
 doc-builds: doc-prereq
-	+(cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc)
+	+(cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc CVC4_DOXYGEN_INPUT="`builddir="$(builddir)" srcdir="$(srcdir)" "$(srcdir)/doc/find_public_interface.sh"`")
+doc-internals-builds: doc-prereq
+	+(cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc CVC4_DOXYGEN_INPUT="$(srcdir)/src src")
 doc-prereq:
 	+(cd $(CURRENT_BUILD) && for dir in `find . -name Makefile | xargs grep -l BUILT_SOURCES`; do (cd `dirname "$$dir"`; (cat Makefile; echo 'doc-prereq: $$(BUILT_SOURCES)') | $(MAKE) -f- doc-prereq); done)
 
diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index 78014290d..71d434959 100644
--- a/config/doxygen.cfg
+++ b/config/doxygen.cfg
@@ -568,8 +568,7 @@ WARN_LOGFILE           =
 # directories like "/usr/src/myproject". Separate the files or directories
 # with spaces.
 
-INPUT                  = $(SRCDIR)/src \
-			 src
+INPUT                  = $(CVC4_DOXYGEN_INPUT)
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
diff --git a/doc/find_public_interface.sh b/doc/find_public_interface.sh
new file mode 100644
index 000000000..4609846f7
--- /dev/null
+++ b/doc/find_public_interface.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+#
+# Enumerates public interface headers, so that public-only documentation
+# can be produced.
+#
+
+cd "$(dirname "$0")"
+
+echo -n "\"$srcdir/src/include/cvc4.h\" "
+echo -n "\"$srcdir/src/include/cvc4_public.h\" "
+( (find "$builddir" -name '*.h' | xargs grep -l '^# *include  *"cvc4.*_public\.h"'); \
+  (find "$srcdir" -name '*.h' | xargs grep -l '^# *include  *"cvc4.*_public\.h"'); \
+) | \
+while read f; do
+  if expr "$f" : ".*_\(template\|private\|test_utils\)\.h$" &>/dev/null; then
+    continue
+  fi
+  echo -n "\"$f\" "
+done
+
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 5129cd73a..dc82daec4 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -36,12 +36,13 @@ ${includes}
 #include "util/exception.h"
 #include "util/language.h"
 #include "util/hash.h"
+#include "util/options.h"
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 45 "${template}"
+#line 46 "${template}"
 
 namespace CVC4 {
 
@@ -682,7 +683,12 @@ public:
     long& l = out.iword(s_iosIndex);
     if(l == 0) {
       // set the default print depth on this ostream
-      l = s_defaultPrintDepth;
+      if(Options::current() != NULL) {
+        l = Options::current()->defaultExprDepth;
+      }
+      if(l == 0) {
+        l = s_defaultPrintDepth;
+      }
     }
     return l;
   }
@@ -877,9 +883,10 @@ class CVC4_PUBLIC ExprSetLanguage {
 
   /**
    * The default language to use, for ostreams that haven't yet had a
-   * setlanguage() applied to them.
+   * setlanguage() applied to them and where the current Options
+   * information isn't available.
    */
-  static const int s_defaultLanguage = language::output::LANG_AST;
+  static const int s_defaultOutputLanguage = language::output::LANG_AST;
 
   /**
    * When this manipulator is used, the setting is stored here.
@@ -902,7 +909,15 @@ public:
     if(l == 0) {
       // set the default language on this ostream
       // (offset by one to detect whether default has been set yet)
-      l = s_defaultLanguage + 1;
+      if(Options::current() != NULL) {
+        l = Options::current()->outputLanguage + 1;
+      }
+      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;
+      }
     }
     return OutputLanguage(l - 1);
   }
@@ -942,7 +957,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 946 "${template}"
+#line 961 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a2fddadfc..1abcf398b 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -336,8 +336,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
   if(! tn.isPredicateLike() ||
      tn.getArgTypes().size() != 1) {
     std::stringstream ss;
-    ss << Expr::setlanguage(Options::current()->outputLanguage)
-       << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
+    ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
     throw TypeCheckingExceptionPrivate(lambdan, ss.str());
   }
 
@@ -357,8 +356,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
   if(! tn.isPredicateLike() ||
      tn.getArgTypes().size() != 1) {
     std::stringstream ss;
-    ss << Expr::setlanguage(Options::current()->outputLanguage)
-       << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
+    ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
     throw TypeCheckingExceptionPrivate(lambdan, ss.str());
   }
 
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 28aa2f884..1e983e86c 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -71,8 +71,6 @@ ${type_cardinalities}
 #line 72 "${template}"
   default: {
     std::stringstream ss;
-    ss << Expr::setlanguage(language::toOutputLanguage
-                            ( Options::current()->inputLanguage ));
     ss << "A theory kinds file did not provide a cardinality "
        << "or cardinality computer for type:\n" << typeNode
        << "\nof kind " << k;
@@ -84,7 +82,7 @@ ${type_cardinalities}
 inline bool isWellFounded(TypeConstant tc) {
   switch(tc) {
 ${type_constant_wellfoundednesses}
-#line 88 "${template}"
+#line 86 "${template}"
   default: {
     std::stringstream ss;
     ss << "No well-foundedness status known for type constant: " << tc;
@@ -99,11 +97,9 @@ inline bool isWellFounded(TypeNode typeNode) {
   case TYPE_CONSTANT:
     return isWellFounded(typeNode.getConst<TypeConstant>());
 ${type_wellfoundednesses}
-#line 103 "${template}"
+#line 101 "${template}"
   default: {
     std::stringstream ss;
-    ss << Expr::setlanguage(language::toOutputLanguage
-                            ( Options::current()->inputLanguage ));
     ss << "A theory kinds file did not provide a well-foundedness "
        << "or well-foundedness computer for type:\n" << typeNode
        << "\nof kind " << k;
@@ -115,7 +111,7 @@ ${type_wellfoundednesses}
 inline Node mkGroundTerm(TypeConstant tc) {
   switch(tc) {
 ${type_constant_groundterms}
-#line 119 "${template}"
+#line 115 "${template}"
   default: {
     std::stringstream ss;
     ss << "No ground term known for type constant: " << tc;
@@ -130,11 +126,9 @@ inline Node mkGroundTerm(TypeNode typeNode) {
   case TYPE_CONSTANT:
     return mkGroundTerm(typeNode.getConst<TypeConstant>());
 ${type_groundterms}
-#line 134 "${template}"
+#line 130 "${template}"
   default: {
     std::stringstream ss;
-    ss << Expr::setlanguage(language::toOutputLanguage
-                            ( Options::current()->inputLanguage ));
     ss << "A theory kinds file did not provide a ground term "
        << "or ground term computer for type:\n" << typeNode
        << "\nof kind " << k;
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index 958175030..eda5df2ca 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -153,25 +153,9 @@ int runCvc4(int argc, char* argv[], Options& options) {
     }
   }
 
-  // Create the expression manager
-  ExprManager exprMgr(options);
-
-  // Create the SmtEngine
-  SmtEngine smt(&exprMgr);
-
-  // signal handlers need access
-  pStatistics = smt.getStatisticsRegistry();
-
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
-  // Timer statistic
-  RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
-
-  // Filename statistics
-  ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
-
   if(options.inputLanguage == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
@@ -228,6 +212,15 @@ int runCvc4(int argc, char* argv[], Options& options) {
                      << Expr::printtypes(false);
   }
 
+  // important even for muzzled builds (to get result output right)
+  *options.out << Expr::setlanguage(options.outputLanguage);
+
+  // Create the expression manager
+  ExprManager exprMgr(options);
+
+  // Create the SmtEngine
+  SmtEngine smt(&exprMgr);
+
   Parser* replayParser = NULL;
   if( options.replayFilename != "" ) {
     ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
@@ -245,8 +238,15 @@ int runCvc4(int argc, char* argv[], Options& options) {
     *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
   }
 
-  // important even for muzzled builds (to get result output right)
-  *options.out << Expr::setlanguage(options.outputLanguage);
+  // signal handlers need access
+  pStatistics = smt.getStatisticsRegistry();
+
+  // Timer statistic
+  RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
+
+  // Filename statistics
+  ReferenceStat< const char* > s_statFilename("filename", filename);
+  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
 
   // Parse and execute commands until we are done
   Command* cmd;
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 21f82f638..55e10724b 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -942,7 +942,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
             i != i_end;
             ++i) {
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
-          Expr func = EXPR_MANAGER->mkVar(*i, f.getType());
+          Expr func = EXPR_MANAGER->mkVar(*i, t);
           PARSER_STATE->defineFunction(*i, f);
           Command* decl = new DefineFunctionCommand(*i, func, f);
           seq->addCommand(decl);
@@ -2094,6 +2094,12 @@ NUMBER_OR_RANGEOP
     )
   ;
 
+// these empty fragments remove "no lexer rule corresponding to token" warnings
+fragment INTEGER_LITERAL:;
+fragment DECIMAL_LITERAL:;
+fragment DOT:;
+fragment DOTDOT:;
+
 /**
  * Matches the hexidecimal digits (0-9, a-f, A-F)
  */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 07998b58f..84d75ceac 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -115,7 +115,11 @@ namespace CVC4 {
 #include "util/integer.h"
 #include "util/output.h"
 #include "util/rational.h"
+#include "util/hash.h"
 #include <vector>
+#include <set>
+#include <string>
+#include <sstream>
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -439,6 +443,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   std::string attr;
   Expr attexpr;
   std::vector<Expr> attexprs;
+  std::hash_set<std::string, StringHashFunction> names;
+  std::vector< std::pair<std::string, Expr> > binders;
 }
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -540,8 +546,22 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
     { PARSER_STATE->pushScope(); }
-    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
-      { PARSER_STATE->defineVar(name,expr); } )+
+    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
+      // this is a parallel let, so we have to save up all the contributions
+      // of the let and define them only later on
+      { if(names.count(name) == 1) {
+          std::stringstream ss;
+          ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones";
+          PARSER_STATE->warning(ss.str());
+        } else {
+          names.insert(name);
+        }
+        binders.push_back(std::make_pair(name, expr)); } )+
+    { // now implement these bindings
+      for(std::vector< std::pair<std::string, Expr> >::iterator i = binders.begin(); i != binders.end(); ++i) {
+        PARSER_STATE->defineVar((*i).first, (*i).second);
+      }
+    }
     RPAREN_TOK
     term[expr, f2]
     RPAREN_TOK
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 668b57b40..10d2aee8c 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -25,7 +25,8 @@
 #include "theory/rewriter.h"
 #include "expr/expr_stream.h"
 #include "decision/decision_engine.h"
-
+#include "util/lemma_input_channel.h"
+#include "util/lemma_output_channel.h"
 
 namespace CVC4 {
 namespace prop {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 97046a1ae..ddc45228e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -802,17 +802,32 @@ void SmtEngine::defineFunction(Expr func,
   Type formulaType = formula.getType(Options::current()->typeChecking);
 
   Type funcType = func.getType();
-  Type rangeType = funcType.isFunction() ?
-    FunctionType(funcType).getRangeType() : funcType;
-  if(formulaType != rangeType) {
-    stringstream ss;
-    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
-       << "Defined function's declared type does not match that of body\n"
-       << "The function  : " << func << "\n"
-       << "Its range type: " << rangeType << "\n"
-       << "The body      : " << formula << "\n"
-       << "Body type     : " << formulaType;
-    throw TypeCheckingException(func, ss.str());
+  // We distinguish here between definitions of constants and functions,
+  // because the type checking for them is subtly different.  Perhaps we
+  // should instead have SmtEngine::defineFunction() and
+  // SmtEngine::defineConstant() for better clarity, although then that
+  // doesn't match the SMT-LIBv2 standard...
+  if(formals.size() > 0) {
+    Type rangeType = FunctionType(funcType).getRangeType();
+    if(formulaType != rangeType) {
+      stringstream ss;
+      ss << "Type of defined function does not match its declaration\n"
+         << "The function  : " << func << "\n"
+         << "Declared type : " << rangeType << "\n"
+         << "The body      : " << formula << "\n"
+         << "Body type     : " << formulaType;
+      throw TypeCheckingException(func, ss.str());
+    }
+  } else {
+    if(formulaType != funcType) {
+      stringstream ss;
+      ss << "Declared type of defined constant does not match its definition\n"
+         << "The constant   : " << func << "\n"
+         << "Declared type  : " << funcType << "\n"
+         << "The definition : " << formula << "\n"
+         << "Definition type: " << formulaType;
+      throw TypeCheckingException(func, ss.str());
+    }
   }
   TNode funcNode = func.getTNode();
   vector<Node> formalsNodes;
@@ -954,7 +969,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
     Assert(Rewriter::rewrite(d_assertionsToPreprocess[i]) == d_assertionsToPreprocess[i]);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl;
-    d_propagator.assert(d_assertionsToPreprocess[i]);
+    d_propagator.assertTrue(d_assertionsToPreprocess[i]);
   }
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1353,8 +1368,7 @@ bool SmtEnginePrivate::simplifyAssertions()
     // well-typed, and we don't want the C++ runtime to abort our
     // process without any error notice.
     stringstream ss;
-    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
-       << "A bad expression was produced.  Original exception follows:\n"
+    ss << "A bad expression was produced.  Original exception follows:\n"
        << tcep;
     InternalError(ss.str().c_str());
   }
@@ -1573,8 +1587,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) {
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
     stringstream ss;
-    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
-       << "Expected " << boolType << "\n"
+    ss << "Expected " << boolType << "\n"
        << "The assertion : " << e << "\n"
        << "Its type      : " << type;
     throw TypeCheckingException(e, ss.str());
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 188f73c78..390ac280b 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1441,7 +1441,7 @@ void TheoryArith::check(Effort effortLevel){
   while(!done()){
     Constraint curr = constraintFromFactQueue();
     if(curr != NullConstraint){
-      bool res = assertionCases(curr);
+      bool res CVC4_UNUSED = assertionCases(curr);
       Assert(!res || inConflict());
     }
     if(inConflict()){ break; }
@@ -1453,7 +1453,7 @@ void TheoryArith::check(Effort effortLevel){
       d_learnedBounds.pop();
       Debug("arith::learned") << curr << endl;
 
-      bool res = assertionCases(curr);
+      bool res CVC4_UNUSED = assertionCases(curr);
       Assert(!res || inConflict());
 
       if(inConflict()){ break; }
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 5f3f964de..63b44f7ca 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -29,11 +29,11 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-void CircuitPropagator::assert(TNode assertion)
+void CircuitPropagator::assertTrue(TNode assertion)
 {
   if (assertion.getKind() == kind::AND) {
     for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) {
-      assert(assertion[i]);
+      assertTrue(assertion[i]);
     }
   } else {
     // Analyze the assertion for back-edges and all that
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 04934b1fa..147a5927f 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -260,7 +260,7 @@ public:
   { d_context.pop(); }
 
   /** Assert for propagation */
-  void assert(TNode assertion);
+  void assertTrue(TNode assertion);
 
   /**
    * Propagate through the asserted circuit propagator. New information discovered by the propagator
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 52d0defd1..9b0611ed8 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -51,7 +51,6 @@ class ApplyTypeRule {
         for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
           if((*argument_it).getType() != *argument_type_it) {
             std::stringstream ss;
-            ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
             ss << "argument types do not match the function type:\n"
                << "argument:  " << *argument_it << "\n"
                << "has type:  " << (*argument_it).getType() << "\n"
@@ -81,7 +80,6 @@ class EqualityTypeRule {
 
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
-        ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
         ss << "Subtypes must have a common type:" << std::endl;
         ss << "Equation: " << n << std::endl;
         ss << "Type 1: " << lhsType << std::endl;
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index bb6dfe40b..8cfdab5af 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -345,8 +345,10 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     bits.push_back(utils::mkBitOf(node, i));
   }
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
-  BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+    BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
+  }
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
@@ -363,7 +365,9 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
       bits.push_back(utils::mkTrue()); 
     }
   }
-  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  }
 }
 
 
@@ -391,7 +395,9 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
     }
   }
   Assert (bits.size() == utils::getSize(node)); 
-  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  }
 }
 
 void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
@@ -512,7 +518,9 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
     shiftAddMultiplier(res, current, newres);
     res = newres;
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
@@ -709,7 +717,9 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
@@ -740,7 +750,9 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
@@ -773,8 +785,9 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
-
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
@@ -791,9 +804,10 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
   Assert (bits.size() == high - low + 1);   
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
-  BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
-       
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+    BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
+  }
 }
 
 
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index e43479381..1f15bffa8 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -72,8 +72,10 @@ class BacktrackableSetCollection {
     while (d_nodesInserted < d_memory.size()) {
       const tree_entry_type& node = d_memory.back();
 
-      BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
-                                 << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
+      if(Debug.isOn("cd_set_collection")) {
+        BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
+                                     << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
+      }
 
       if (node.hasParent()) {
         if (node.isLeft()) {
@@ -278,7 +280,9 @@ public:
 
     // Find the biggest node smaleer than value (it must exist)
     while (set != null) {
-      BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+      if(Debug.isOn("set_collection")) {
+        BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+      }
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() >= value) {
         // If the node is bigger than the value, we need a smaller one
@@ -305,7 +309,9 @@ public:
 
     // Find the smallest node bigger than value (it must exist)
     while (set != null) {
-      BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+      if(Debug.isOn("set_collection")) {
+        BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+      }
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() <= value) {
         // If the node is smaller than the value, we need a bigger one
@@ -372,7 +378,9 @@ public:
     backtrack();
     Assert(isValid(set));
 
-    BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+    if(Debug.isOn("set_collection")) {
+      BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+    }
 
     // Empty set no elements
     if (set == null) {
diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h
index fa0d3f818..174b90ff5 100644
--- a/src/theory/datatypes/explanation_manager.h
+++ b/src/theory/datatypes/explanation_manager.h
@@ -104,7 +104,7 @@ class Explainer
 {
 public:
   /** assert that n is true */
-  virtual void assert( Node n ) = 0;
+  virtual void assertTrue( Node n ) = 0;
   /** get the explanation for n.  
       This should call pm->setExplanation( n1, jn1, r1 ) ... pm->setExplanation( nk, jnk, rk )
         for some set of Nodes n1...nk.
@@ -115,7 +115,7 @@ public:
           jni is the (at least informal) justification for ni.
       - Return value should be a (possibly empty) conjunction of nodes n'1...n'k, where each n'i occurs 
           (as a conjunct) in jn1...jnk, but not in n1...nk.  
-          For each of these literals n'i, assert( n'i ) was called.
+          For each of these literals n'i, assertTrue( n'i ) was called.
       - either pm->setExplanation( n, ... ) is called, or n is the return value.
   */
   virtual Node explain( Node n, ProofManager* pm ) = 0;
@@ -134,7 +134,7 @@ public:
    }
   ~CongruenceClosureExplainer(){}
   /** assert that n is true */
-  void assert( Node n ){
+  void assertTrue( Node n ){
     Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF );
     d_cc->addEquality( n );
   }
@@ -170,7 +170,7 @@ public:
   ~ExplanationManager(){}
 
   /** assert that n is true (n is an input) */
-  void assert( Node n ) { 
+  void assertTrue( Node n ) { 
     //TODO: this can be optimized: 
     //  if the previous explanation for n was empty (n is a tautology), 
     //  then we should not claim it to be an input.
@@ -219,4 +219,4 @@ public:
 }
 }
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 3b8efabb7..f9ef49c6b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -124,7 +124,7 @@ void TheoryDatatypes::check(Effort e) {
     if( !hasConflict() ){
       if( d_em.hasNode( assertion ) ){
         Debug("datatypes") << "Assertion has already been derived" << endl;
-        d_em.assert( assertion );
+        d_em.assertTrue( assertion );
       } else {
         switch(assertion.getKind()) {
         case kind::EQUAL:
@@ -949,7 +949,7 @@ void TheoryDatatypes::addEquality(TNode eq) {
     //setup merge pending list
     d_merge_pending.push_back( vector< pair< Node, Node > >() );
 
-    d_cce.assert(eq);
+    d_cce.assertTrue(eq);
     d_cc.addTerm(eq[0]);
     d_cc.addTerm(eq[1]);
 
@@ -979,7 +979,7 @@ void TheoryDatatypes::addEquality(TNode eq) {
     Debug("datatypes-ae") << "   Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl;
     //merge original nodes
     merge( eq[0], eq[1] );
-    d_cce.assert(eq);
+    d_cce.assertTrue(eq);
     d_cc.addTerm(eq[0]);
     d_cc.addTerm(eq[1]);
 #else
@@ -987,7 +987,7 @@ void TheoryDatatypes::addEquality(TNode eq) {
     Debug("datatypes-ae") << "   Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl;
     merge( eq[0], eq[1] );
     if( !hasConflict() ){
-      d_cce.assert(eq);
+      d_cce.assertTrue(eq);
       d_cc.addTerm(eq[0]);
       d_cc.addTerm(eq[1]);
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4ab2c779c..50682f647 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "util/options.h"
+#include "util/lemma_output_channel.h"
 
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 2856e6a01..34a8a805b 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -46,8 +46,7 @@ public:
         TypeNode currentArgumentType = *argument_type_it;
         if(!currentArgument.isSubtypeOf(currentArgumentType)) {
           std::stringstream ss;
-          ss << Expr::setlanguage(Options::current()->outputLanguage)
-             << "argument type is not a subtype of the function's argument type:\n"
+          ss << "argument type is not a subtype of the function's argument type:\n"
              << "argument:  " << *argument_it << "\n"
              << "has type:  " << (*argument_it).getType() << "\n"
              << "not subtype: " << *argument_type_it;
diff --git a/src/util/hash.h b/src/util/hash.h
index fdfbf4087..6fb20dab0 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -26,6 +26,7 @@
 namespace __gnu_cxx {}
 
 #include <ext/hash_map>
+#include <ext/hash_set>
 
 namespace __gnu_cxx {
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index a10aae83d..2352ae503 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -87,6 +87,7 @@ Options::Options() :
   strictParsing(false),
   lazyDefinitionExpansion(false),
   printWinner(false),
+  defaultExprDepth(0),
   simplificationMode(SIMPLIFICATION_MODE_BATCH),
   simplificationModeSetByUser(false),
   decisionMode(DECISION_STRATEGY_INTERNAL),
@@ -951,6 +952,7 @@ throw(OptionException) {
         Chat.getStream() << Expr::setdepth(depth);
         Message.getStream() << Expr::setdepth(depth);
         Warning.getStream() << Expr::setdepth(depth);
+        defaultExprDepth = depth;
       }
       break;
 
diff --git a/src/util/options.h b/src/util/options.h
index f3ae3b64e..f423260b0 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -27,8 +27,6 @@
 
 #include "util/exception.h"
 #include "util/language.h"
-#include "util/lemma_output_channel.h"
-#include "util/lemma_input_channel.h"
 #include "util/tls.h"
 #include "theory/theoryof_mode.h"
 
@@ -37,6 +35,8 @@
 namespace CVC4 {
 
 class ExprStream;
+class LemmaInputChannel;
+class LemmaOutputChannel;
 
 /** Class representing an option-parsing exception. */
 class CVC4_PUBLIC OptionException : public CVC4::Exception {
@@ -112,6 +112,9 @@ struct CVC4_PUBLIC Options {
   /** Parallel Only: Whether the winner is printed at the end or not. */
   bool printWinner;
 
+  /** The default expression depth to print on ostreams. */
+  int defaultExprDepth;
+
   /** Enumeration of simplification modes (when to simplify). */
   typedef enum {
     /** Simplify the assertions as they come in */
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 5eda230c3..58788c194 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -43,7 +43,8 @@ SMT2_TESTS = \
 	simple-lra.smt2 \
 	simple-rdl.smt2 \
 	simple-uf.smt2 \
-	simplification_bug4.smt2
+	simplification_bug4.smt2 \
+	parallel-let.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
@@ -115,7 +116,10 @@ BUG_TESTS = \
 	buggy-ite.smt2 \
 	bug303.smt2 \
 	bug310.cvc \
-	bug339.smt2
+	bug322.cvc \
+	bug322b.cvc \
+	bug339.smt2 \
+	bug365.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug322.cvc b/test/regress/regress0/bug322.cvc
new file mode 100644
index 000000000..c68fde795
--- /dev/null
+++ b/test/regress/regress0/bug322.cvc
@@ -0,0 +1,23 @@
+% EXPECT: sat
+% EXIT: 10
+% Preamble  --------------
+DATATYPE UNIT = Unit END;
+DATATYPE BOOL = Truth | Falsity END;
+
+% Decls     --------------
+node$type: TYPE;
+value$type: TYPE;
+Nodes$elem$type: TYPE = node$type;
+Nodes$t$type: TYPE;
+node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL;
+failure_pattern$type: TYPE = node_pair_set$type;
+is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, 
+                                                               deliver: failure_pattern$type): 
+                                                      (IF (EXISTS (q: node$type): 
+                                                          (NOT ((((deliver)[
+                                                                 (p)])[
+                                                                (q)]) = 
+                                                               (Truth)))) THEN 
+                                                      (Truth) ELSE (Falsity) ENDIF));
+
+CHECKSAT;
diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc
new file mode 100644
index 000000000..d10292dd5
--- /dev/null
+++ b/test/regress/regress0/bug322b.cvc
@@ -0,0 +1,12 @@
+% COMMAND-LINE: --incremental
+% EXPECT: valid
+% EXPECT: valid
+% EXPECT: valid
+% EXIT: 20
+x : INT;
+y : INT = x + 1;
+z : INT = -10;
+identity : INT -> INT = LAMBDA(x:INT) : x;
+QUERY identity(x) = x;
+QUERY identity(y) > x;
+QUERY identity(z) = -10;
diff --git a/test/regress/regress0/bug365.smt2 b/test/regress/regress0/bug365.smt2
new file mode 100644
index 000000000..6dd48a849
--- /dev/null
+++ b/test/regress/regress0/bug365.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_LIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(assert (let
+	   ((a 2))
+	   (= a (let ((a 7)) a))))
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc
index 80aecfe25..49684241c 100644
--- a/test/regress/regress0/datatypes/rec2.cvc
+++ b/test/regress/regress0/datatypes/rec2.cvc
@@ -1,7 +1,7 @@
 % EXPECT: valid
 % EXIT: 20
 c : BOOLEAN;
-a16 : [# _a : REAL, _b : REAL #] = (
+a16 : [# _a : INT, _b : INT #] = (
         IF c THEN (# _a := 3, _b := 2 #)
         ELSE (# _a := 1, _b := 5 #)
         ENDIF WITH ._a := 2);
diff --git a/test/regress/regress0/parallel-let.smt2 b/test/regress/regress0/parallel-let.smt2
new file mode 100644
index 000000000..1f12522ee
--- /dev/null
+++ b/test/regress/regress0/parallel-let.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(assert (distinct x y))
+(assert (let ((x y) (y x)) (= x y)))
+(check-sat)
+(exit)