Bug-related:

* ITE removal fixed to be context-dependent (on UserContext).
  Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
  (partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
  was labeled sat); re-enable it for "make regress"

Also:

* --check-model doesn't fail if quantified assertions don't simplify away.

* fix some examples, and the Java system test, for the disappearance of the
  BoolExpr class

* add copy constructor to array type enumerator (the type enumerator
  framework requires copy ctors, and the automatically-generated copy ctor
  was copying pointers that were then deleted, leaving dangling pointers in
  the copy and causing segfaults)

* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
  you to dump before/after a particular preprocessing pass.  E.g.,
  --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
  "--dump=assertions" by itself is after all preprocessing, just before CNF
  conversion.
* minor fixes to dumping output
* include Model in language bindings

Minor refactoring/misc:

* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
  (e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
  options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications

34 files changed, 320 insertions, 193 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index 7d42f9484..2eedbf64c 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -151,6 +151,7 @@ using namespace CVC4;
 %include "util/array.i"
 %include "util/array_store_all.i"
 %include "util/hash.i"
+%include "util/util_model.i"
 
 %include "expr/type.i"
 %include "util/ascription_type.i"
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 220629cfd..9df4dba85 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -890,7 +890,7 @@ void GetModelCommand::printResult(std::ostream& out) const throw() {
   if(! ok()) {
     this->Command::printResult(out);
   } else {
-    d_smtEngine->printModel( out, d_result );
+    out << *d_result;
   }
 }
 
diff --git a/src/options/base_options b/src/options/base_options
index 91b6354d1..9f0ccc9a5 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -108,10 +108,10 @@ common-option statistics statistics --stats bool
 undocumented-alias --statistics = --stats
 undocumented-alias --no-statistics = --no-stats
 
-common-option parseOnly parse-only --parse-only bool :read-write
+option parseOnly parse-only --parse-only bool :read-write
  exit after parsing input
 
-common-option preprocessOnly preprocess-only --preprocess-only bool
+option preprocessOnly preprocess-only --preprocess-only bool
  exit after preprocessing input
 
 option segvNoSpin --segv-nospin bool
diff --git a/src/options/mkoptions b/src/options/mkoptions
index ffaff9927..48050ef7e 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -21,23 +21,24 @@ function usage {
 }
 
 progress_char=/
+if [ -t 1 ]; then r="\r"; else r=""; fi
 function progress {
   file="$(expr "$1" : '.*\(.................................................................\)')"
   if [ -z "$file" ]; then file="$1"; else file="[...]$file"; fi
-  printf "\r%c %-70s (%3d%%)" "$progress_char" "$file" "$(($2*100/$3))"
+  [ -t 1 ] && printf "$r%c %-70s (%3d%%)" "$progress_char" "$file" "$(($2*100/$3))"
   progress_char="`echo "$progress_char" | tr -- '-\\\\|/' '\\\\|/-'`"
 }
 
 function NOTE {
-  printf "\r%-80s\n" "$kf:$lineno: note: $@"
+  printf "$r%-80s\n" "$kf:$lineno: note: $@"
 }
 
 function WARN {
-  printf "\r%-80s\n" "$kf:$lineno: warning: $@"
+  printf "$r%-80s\n" "$kf:$lineno: warning: $@"
 }
 
 function ERR {
-  printf "\r%-80s\n" "$kf:$lineno: error: $@"
+  printf "$r%-80s\n" "$kf:$lineno: error: $@"
   exit 1
 }
 
@@ -1322,7 +1323,7 @@ EOF
     rm -f "$output.tmp"
   else
     mv -f "$output.tmp" "$output"
-    printf "\rregenerated %-68s\n" "$output"
+    printf "${r}regenerated %-68s\n" "$output"
   fi
 }
 
@@ -1505,7 +1506,7 @@ if diff -q "$output" "$output.tmp" &>/dev/null; then
   regenerated=false
 else
   mv -f "$output.tmp" "$output"
-  printf "\rregenerated %-68s\n" "$output"
+  printf "${r}regenerated %-68s\n" "$output"
   regenerated=true
 fi
 rm -f "$output.tmp"
@@ -1513,5 +1514,5 @@ rm -f "$output.tmp"
 done
 
 if ! $regenerated; then
-  printf "\r%-80s\r" ""
+  [ -t 1 ] && printf "$r%-80s$r" ""
 fi
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 7b58ba4f9..3198c8b64 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -156,7 +156,7 @@ Parser::mkBoundVar(const std::string& name, const Type& type) {
 
 Expr
 Parser::mkFunction(const std::string& name, const Type& type,
-                            bool levelZero) {
+                   bool levelZero) {
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
   defineFunction(name, expr, levelZero);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 37b926c34..1bfba3eb4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -634,7 +634,7 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   | str[s]
     { sexpr = SExpr(s); }
   | symbol[s,CHECK_NONE,SYM_SORT]
-    { sexpr = SExpr(s); }
+    { sexpr = SExpr(SExpr::Keyword(s)); }
   | builtinOp[k]
     { std::stringstream ss;
       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 34bf0bb6d..ddac7db46 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -187,10 +187,15 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* AstPrinter::toStream(CommandStatus*) */
 
-void AstPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
+void AstPrinter::toStream(std::ostream& out, Model& m) const throw() {
   out << "Model()";
 }
 
+void AstPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+  // shouldn't be called; only the non-Command* version above should be
+  Unreachable();
+}
+
 static void toStream(std::ostream& out, const EmptyCommand* c)  throw() {
   out << "EmptyCommand(" << c->getName() << ")";
 }
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index d5701c088..ea7cd2d16 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -31,12 +31,12 @@ namespace ast {
 
 class AstPrinter : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  //for models
-  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
+  void toStream(std::ostream& out, Model& m) const throw();
 };/* class AstPrinter */
 
 }/* CVC4::printer::ast namespace */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 5d2ffb9db..7937e82f3 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -741,25 +741,25 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
-void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
-  theory::TheoryModel* tm = (theory::TheoryModel*)m;
+void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+  theory::TheoryModel& tm = (theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( tn.isSort() ){
       //print the cardinality
-      if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
-        out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl;
+      if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+        out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
       }
     }
     out << c << std::endl;
     if( tn.isSort() ){
       //print the representatives
-      if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
-        for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){
-          if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){
-            out << tm->d_rep_set.d_type_reps[tn][i] << " : " << tn << ";" << std::endl;
+      if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+        for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+          if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+            out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
           }else{
-            out << "% rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl;
+            out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
           }
         }
       }
@@ -778,7 +778,7 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const t
     }else{
       out << tn;
     }
-    out << " = " << tm->getValue( n ) << ";" << std::endl;
+    out << " = " << tm.getValue( n ) << ";" << std::endl;
 
 /*
     //for table format (work in progress)
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 72564f24d..a8daebf23 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -34,12 +34,11 @@ namespace cvc {
 
 class CvcPrinter : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
+  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  //for models
-  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
 };/* class CvcPrinter */
 
 }/* CVC4::printer::cvc namespace */
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f20ab2901..8b4eab24f 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -127,9 +127,9 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
   }
 }/* Printer::toStream(SExpr) */
 
-void Printer::toStream(std::ostream& out, Model* m) const throw() {
-  for(size_t i = 0; i < m->getNumCommands(); ++i) {
-    toStream(out, m, m->getCommand(i));
+void Printer::toStream(std::ostream& out, Model& m) const throw() {
+  for(size_t i = 0; i < m.getNumCommands(); ++i) {
+    toStream(out, m, m.getCommand(i));
   }
 }/* Printer::toStream(Model) */
 
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 48b76d15a..bc99f5130 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -44,6 +44,9 @@ protected:
   // derived classes can construct, but no one else.
   Printer() throw() {}
 
+  /** write model response to command */
+  virtual void toStream(std::ostream& out, Model& m, const Command* c) const throw() = 0;
+
 public:
   /** Get the Printer for a given OutputLanguage */
   static Printer* getPrinter(OutputLanguage lang) throw() {
@@ -78,12 +81,8 @@ public:
   virtual void toStream(std::ostream& out, const Result& r) const throw();
 
   /** Write a Model out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, Model* m ) const throw();
+  virtual void toStream(std::ostream& out, Model& m) const throw();
 
-  //for models
-
-  /** write model response to command */
-  virtual void toStream(std::ostream& out, Model* m, const Command* c) const throw() = 0;
 };/* class Printer */
 
 }/* CVC4 namespace */
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index 553692dc5..6424e377e 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -51,8 +51,13 @@ void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw()
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 }/* Smt1Printer::toStream() */
 
-void Smt1Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c);
+void Smt1Printer::toStream(std::ostream& out, Model& m) const throw() {
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m);
+}
+
+void Smt1Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+  // shouldn't be called; only the non-Command* version above should be
+  Unreachable();
 }
 
 }/* CVC4::printer::smt1 namespace */
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
index d1b36208c..39f69e8ff 100644
--- a/src/printer/smt1/smt1_printer.h
+++ b/src/printer/smt1/smt1_printer.h
@@ -30,13 +30,13 @@ namespace printer {
 namespace smt1 {
 
 class Smt1Printer : public CVC4::Printer {
+  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
-  //for models
-  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
+  void toStream(std::ostream& out, Model& m) const throw();
 };/* class Smt1Printer */
 
 }/* CVC4::printer::smt1 namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 31754cb3a..466af8676 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -532,32 +532,32 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 }/* Smt2Printer::toStream(CommandStatus*) */
 
 
-void Smt2Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
-  theory::TheoryModel* tm = (theory::TheoryModel*)m;
+void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+  theory::TheoryModel& tm = (theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( tn.isSort() ){
       //print the cardinality
-      if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
-        out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl;
+      if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+        out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
       }
     }
     out << c << std::endl;
     if( tn.isSort() ){
       //print the representatives
-      if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
-        for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){
-          if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){
-            out << "(declare-fun " << tm->d_rep_set.d_type_reps[tn][i] << " () " << tn << ")" << std::endl;
+      if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+        for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+          if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+            out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl;
           }else{
-            out << "; rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl;
+            out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
           }
         }
       }
     }
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
     Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
-    Node val = tm->getValue( n );
+    Node val = tm.getValue( n );
     if(val.getKind() == kind::LAMBDA) {
       out << "(define-fun " << n << " " << val[0]
           << " " << n.getType().getRangeType()
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index ce48f36f3..5b3b30367 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -31,12 +31,11 @@ namespace smt2 {
 
 class Smt2Printer : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  //for models
-  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
   void toStream(std::ostream& out, const Result& r) const throw();
 };/* class Smt2Printer */
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 7fc7a1d9c..e36589ba8 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1410,7 +1410,7 @@ void Solver::push()
   trail_user_lim.push(trail.size());
   assert(trail_user_lim.size() == assertionLevel);
 
-  context->push();
+  context->push(); // SAT context for CVC4
 
   Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
 }
@@ -1476,7 +1476,7 @@ void Solver::pop()
 
   Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
 
-  context->pop();
+  context->pop(); // SAT context for CVC4
 
   // Notify the cnf
   proxy->removeClausesAboveLevel(assertionLevel);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 12e85de13..cac030e87 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -110,9 +110,7 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
-  if(!d_inCheckSat && Dump.isOn("learned")) {
-    Dump("learned") << AssertCommand(node.toExpr());
-  } else if(Dump.isOn("lemmas")) {
+  if(Dump.isOn("lemmas")) {
     Dump("lemmas") << AssertCommand(node.toExpr());
   }
 
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 7d5dd56c9..2af826d24 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -75,23 +75,20 @@ benchmark\n\
 declarations\n\
 + Dump user declarations.  Implied by all following modes.\n\
 \n\
-assertions\n\
-+ Output the assertions after non-clausal simplification and static\n\
-  learning phases, but before presolve-time T-lemmas arrive.  If\n\
-  non-clausal simplification and static learning are off\n\
-  (--simplification=none --no-static-learning), the output\n\
-  will closely resemble the input (with term-level ITEs removed).\n\
-\n\
 skolems\n\
 + Dump internally-created skolem variable declarations.  These can\n\
   arise from preprocessing simplifications, existential elimination,\n\
   and a number of other things.  Implied by all following modes.\n\
 \n\
-learned\n\
-+ Output the assertions after non-clausal simplification, static\n\
-  learning, and presolve-time T-lemmas.  This should include all eager\n\
-  T-lemmas (in the form provided by the theory, which my or may not be\n\
-  clausal).  Also includes level-0 BCP done by Minisat.\n\
+assertions\n\
++ Output the assertions after preprocessing and before clausification.\n\
+  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
+  where PASS is one of the preprocessing passes: skolem-quant simplify\n\
+  static-learning ite-removal repeat-simplify theory-preprocessing.\n\
+  PASS can also be the special value \"everything\", in which case the\n\
+  assertions are printed before any preprocessing (with\n\
+  \"assertions:pre-everything\") or after all preprocessing completes\n\
+  (with \"assertions:post-everything\").\n\
 \n\
 clauses\n\
 + Do all the preprocessing outlined above, and dump the CNF-converted\n\
@@ -127,7 +124,7 @@ theory::fullcheck [non-stateful]\n\
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
 Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
-one from the assertions category (either assertions, learned, or clauses), and\n\
+one from the assertions category (either assertions or clauses), and\n\
 perhaps one or more stateful or non-stateful modes for checking correctness\n\
 and completeness of decision procedure implementations.  Stateful modes dump\n\
 the contextual assertions made by the core solver (all decisions and\n\
@@ -177,8 +174,30 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
     if(!strcmp(optargPtr, "benchmark")) {
     } else if(!strcmp(optargPtr, "declarations")) {
     } else if(!strcmp(optargPtr, "assertions")) {
+      Dump.on("assertions:post-everything");
+    } else if(!strncmp(optargPtr, "assertions:", 11)) {
+      const char* p = optargPtr + 11;
+      if(!strncmp(p, "pre-", 4)) {
+        p += 4;
+      } else if(!strncmp(p, "post-", 5)) {
+        p += 5;
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      if(!strcmp(p, "everything")) {
+      } else if(!strcmp(p, "skolem-quant")) {
+      } else if(!strcmp(p, "simplify")) {
+      } else if(!strcmp(p, "static-learning")) {
+      } else if(!strcmp(p, "ite-removal")) {
+      } else if(!strcmp(p, "repeat-simplify")) {
+      } else if(!strcmp(p, "theory-preprocessing")) {
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      Dump.on("assertions");
     } else if(!strcmp(optargPtr, "skolems")) {
-    } else if(!strcmp(optargPtr, "learned")) {
     } else if(!strcmp(optargPtr, "clauses")) {
     } else if(!strcmp(optargPtr, "t-conflicts") ||
               !strcmp(optargPtr, "t-lemmas") ||
@@ -225,7 +244,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
     Dump.on("benchmark");
     if(strcmp(optargPtr, "benchmark")) {
       Dump.on("declarations");
-      if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) {
+      if(strcmp(optargPtr, "declarations")) {
         Dump.on("skolems");
       }
     }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2d83b7960..0a5270d83 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): cconway, kshitij
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -199,10 +199,17 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** Assertions to push to sat */
   vector<Node> d_assertionsToCheck;
 
-  /** Map from skolem variables to index in d_assertionsToCheck containing
-   * corresponding introduced Boolean ite */
+  /**
+   * Map from skolem variables to index in d_assertionsToCheck containing
+   * corresponding introduced Boolean ite
+   */
   IteSkolemMap d_iteSkolemMap;
 
+public:
+  /** Instance of the ITE remover */
+  RemoveITE d_iteRemover;
+
+private:
   /** The top level substitutions */
   SubstitutionMap d_topLevelSubstitutions;
 
@@ -261,17 +268,17 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   bool simplifyAssertions() throw(TypeCheckingException);
 
-  /**
-   * contains quantifiers
-   */
-  bool containsQuantifiers( Node n );
-
 public:
 
   SmtEnginePrivate(SmtEngine& smt) :
     d_smt(smt),
+    d_assertionsToPreprocess(),
     d_nonClausalLearnedLiterals(),
+    d_realAssertionsEnd(0),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
+    d_assertionsToCheck(),
+    d_iteSkolemMap(),
+    d_iteRemover(smt.d_userContext),
     d_topLevelSubstitutions(smt.d_userContext),
     d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) {
     d_smt.d_nodeManager->subscribeEvents(this);
@@ -339,6 +346,8 @@ public:
     d_assertionsToPreprocess.clear();
     d_nonClausalLearnedLiterals.clear();
     d_assertionsToCheck.clear();
+    d_realAssertionsEnd = 0;
+    d_iteSkolemMap.clear();
   }
 
   /**
@@ -404,7 +413,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic));
+  d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
 
   // Add the theories
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -593,9 +602,9 @@ void SmtEngine::setLogicInternal() throw() {
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
-      Theory::setTheoryOfMode(theory::THEORY_OF_TERM_BASED);
+      Theory::setTheoryOfMode(THEORY_OF_TERM_BASED);
     } else {
-      Theory::setTheoryOfMode(theory::THEORY_OF_TYPE_BASED);
+      Theory::setTheoryOfMode(THEORY_OF_TYPE_BASED);
     }
   } else {
     Theory::setTheoryOfMode(options::theoryOfMode());
@@ -791,6 +800,8 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
         d_logic = value.getValue();
         setLogicInternal();
         return;
+      } else {
+        throw UnrecognizedOptionException();
       }
     }
   }
@@ -800,10 +811,18 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
      key == "source" ||
      key == "category" ||
      key == "difficulty" ||
-     key == "smt-lib-version" ||
      key == "notes") {
     // ignore these
     return;
+  } else if(key == "smt-lib-version") {
+    if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
+        (value.isRational() && value.getRationalValue() == Rational(2)) ||
+        (value.getValue() == "2") ) {
+      // supported SMT-LIB version
+      return;
+    }
+    Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
+    throw UnrecognizedOptionException();
   } else if(key == "status") {
     string s;
     if(value.isAtom()) {
@@ -1013,6 +1032,20 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   }
 }
 
+// check if the given node contains a universal quantifier
+static bool containsQuantifiers(Node n) {
+  if(n.getKind() == kind::FORALL) {
+    return true;
+  } else {
+    for(unsigned i = 0; i < n.getNumChildren(); ++i) {
+      if(containsQuantifiers(n[i])) {
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
 Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
   Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl;
   if( n.getKind()==kind::NOT ){
@@ -1117,7 +1150,7 @@ void SmtEnginePrivate::removeITEs() {
   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 
   // Remove all of the ITE occurrences and normalize
-  RemoveITE::run(d_assertionsToCheck, d_iteSkolemMap);
+  d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap);
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
     d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]);
   }
@@ -1144,6 +1177,18 @@ void SmtEnginePrivate::staticLearning() {
   }
 }
 
+// do dumping (before/after any preprocessing pass)
+static void dumpAssertions(const char* key,
+                           const std::vector<Node>& assertionList) {
+  if( Dump.isOn("assertions") &&
+      Dump.isOn(std::string("assertions:") + key) ) {
+    // Push the simplified assertions to the dump output stream
+    for(unsigned i = 0; i < assertionList.size(); ++ i) {
+      TNode n = assertionList[i];
+      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+    }
+  }
+}
 
 // returns false if it learns a conflict
 bool SmtEnginePrivate::nonClausalSimplify() {
@@ -1335,7 +1380,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 
   NodeBuilder<> learnedBuilder(kind::AND);
   Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
-  learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd-1];
+  learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
 
   if( options::incrementalSolving() ||
       options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
@@ -1398,7 +1443,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
 
   if(learnedBuilder.getNumChildren() > 1) {
-    d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(learnedBuilder));
+    d_assertionsToCheck[d_realAssertionsEnd - 1] =
+      Rewriter::rewrite(Node(learnedBuilder));
   }
 
   d_propagator.finish();
@@ -1544,8 +1590,11 @@ bool SmtEnginePrivate::simplifyAssertions()
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << " doing repeated simplification" << std::endl;
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
+      Assert(d_assertionsToCheck.empty());
       bool noConflict = nonClausalSimplify();
-      if(!noConflict) return false;
+      if(!noConflict) {
+        return false;
+      }
     }
 
     Trace("smt") << "POST repeatSimp" << std::endl;
@@ -1566,20 +1615,6 @@ bool SmtEnginePrivate::simplifyAssertions()
   return true;
 }
 
-
-bool SmtEnginePrivate::containsQuantifiers( Node n ){
-  if( n.getKind()==kind::FORALL ){
-    return true;
-  }else{
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( containsQuantifiers( n[i] ) ){
-        return true;
-      }
-    }
-    return false;
-  }
-}
-
 Result SmtEngine::check() {
   Assert(d_fullyInited);
   Assert(d_pendingPops == 0);
@@ -1636,14 +1671,21 @@ void SmtEnginePrivate::processAssertions() {
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
 
+  // Dump the assertions
+  dumpAssertions("pre-everything", d_assertionsToPreprocess);
+
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  // any assertions added beyond realAssertionsEnd must NOT affect the equisatisfiability
+  Assert(d_assertionsToCheck.size() == 0);
+
+  // any assertions added beyond realAssertionsEnd must NOT affect the
+  // equisatisfiability
   d_realAssertionsEnd = d_assertionsToPreprocess.size();
-  if (d_realAssertionsEnd == 0) {
+  if(d_realAssertionsEnd == 0) {
+    // nothing to do
     return;
   }
 
@@ -1682,6 +1724,7 @@ void SmtEnginePrivate::processAssertions() {
     Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << endl;
   }
 
+  dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
   if( options::preSkolemQuant() ){
     //apply pre-skolemization to existential quantifiers
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
@@ -1694,10 +1737,14 @@ void SmtEnginePrivate::processAssertions() {
       }
     }
   }
+  dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
 
+  dumpAssertions("pre-simplify", d_assertionsToPreprocess);
   Chat() << "simplifying assertions..." << endl;
   bool noConflict = simplifyAssertions();
+  dumpAssertions("post-simplify", d_assertionsToPreprocess);
 
+  dumpAssertions("pre-static-learning", d_assertionsToCheck);
   if(options::doStaticLearning()) {
     // Perform static learning
     Chat() << "doing static learning..." << endl;
@@ -1705,7 +1752,9 @@ void SmtEnginePrivate::processAssertions() {
                       << "performing static learning" << endl;
     staticLearning();
   }
+  dumpAssertions("post-static-learning", d_assertionsToCheck);
 
+  dumpAssertions("pre-ite-removal", d_assertionsToCheck);
   {
     Chat() << "removing term ITEs..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
@@ -1714,7 +1763,9 @@ void SmtEnginePrivate::processAssertions() {
     removeITEs();
     d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size();
   }
+  dumpAssertions("post-ite-removal", d_assertionsToCheck);
 
+  dumpAssertions("pre-repeat-simplify", d_assertionsToCheck);
   if(options::repeatSimp()) {
     d_assertionsToCheck.swap(d_assertionsToPreprocess);
     Chat() << "simplifying assertions..." << endl;
@@ -1725,7 +1776,7 @@ void SmtEnginePrivate::processAssertions() {
       IteSkolemMap::iterator it = d_iteSkolemMap.begin();
       IteSkolemMap::iterator iend = d_iteSkolemMap.end();
       NodeBuilder<> builder(kind::AND);
-      builder << d_assertionsToCheck[d_realAssertionsEnd-1];
+      builder << d_assertionsToCheck[d_realAssertionsEnd - 1];
       for (; it != iend; ++it) {
         if (d_topLevelSubstitutions.hasSubstitution((*it).first)) {
           builder << d_assertionsToCheck[(*it).second];
@@ -1733,7 +1784,8 @@ void SmtEnginePrivate::processAssertions() {
         }
       }
       if(builder.getNumChildren() > 1) {
-        d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(builder));
+        d_assertionsToCheck[d_realAssertionsEnd - 1] =
+          Rewriter::rewrite(Node(builder));
       }
       // For some reason this is needed for some benchmarks, such as
       // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
@@ -1742,6 +1794,7 @@ void SmtEnginePrivate::processAssertions() {
       //      Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
     }
   }
+  dumpAssertions("post-repeat-simplify", d_assertionsToCheck);
 
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
@@ -1756,6 +1809,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
+  dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck);
   {
     Chat() << "theory preprocessing..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
@@ -1765,14 +1819,7 @@ void SmtEnginePrivate::processAssertions() {
       d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
     }
   }
-
-  if(Dump.isOn("assertions")) {
-    // Push the simplified assertions to the dump output stream
-    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-      Dump("assertions")
-        << AssertCommand(d_assertionsToCheck[i].toExpr());
-    }
-  }
+  dumpAssertions("post-theory-preprocessing", d_assertionsToCheck);
 
   // Push the formula to decision engine
   if(noConflict) {
@@ -1785,6 +1832,8 @@ void SmtEnginePrivate::processAssertions() {
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
+  dumpAssertions("post-everything", d_assertionsToCheck);
+
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
@@ -1824,7 +1873,7 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
   }
 }
 
-Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) {
+Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException, ModalException) {
 
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
@@ -1891,7 +1940,7 @@ Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) {
   return r;
 }/* SmtEngine::checkSat() */
 
-Result SmtEngine::query(const Expr& e) throw(TypeCheckingException) {
+Result SmtEngine::query(const Expr& e) throw(TypeCheckingException, ModalException) {
 
   Assert(!e.isNull());
   Assert(e.getExprManager() == d_exprManager);
@@ -2003,8 +2052,7 @@ Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) {
   return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
 }
 
-Expr SmtEngine::getValue(const Expr& e)
-  throw(ModalException) {
+Expr SmtEngine::getValue(const Expr& e) throw(ModalException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
@@ -2028,13 +2076,15 @@ Expr SmtEngine::getValue(const Expr& e)
     throw ModalException(msg);
   }
 
-  // do not need to apply preprocessing substitutions (should be recorded in model already)
+  // do not need to apply preprocessing substitutions (should be recorded
+  // in model already)
 
-  // Normalize for the theories
-  Node n = Rewriter::rewrite( e.getNode() );
+  // Expand, then normalize
+  Node n = expandDefinitions(e).getNode();
+  n = Rewriter::rewrite(n);
 
   Trace("smt") << "--- getting value of " << n << endl;
-  theory::TheoryModel* m = d_theoryEngine->getModel();
+  TheoryModel* m = d_theoryEngine->getModel();
   Node resultNode;
   if( m ){
     resultNode = m->getValue( n );
@@ -2112,7 +2162,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
     Node n = Rewriter::rewrite(*i);
 
     Trace("smt") << "--- getting value of " << n << endl;
-    theory::TheoryModel* m = d_theoryEngine->getModel();
+    TheoryModel* m = d_theoryEngine->getModel();
     Node resultNode;
     if( m ){
       resultNode = m->getValue( n );
@@ -2192,15 +2242,19 @@ void SmtEngine::checkModel(bool hardFailure) {
   // and if Notice() is on, the user gave --verbose (or equivalent).
 
   Notice() << "SmtEngine::checkModel(): generating model" << endl;
-  theory::TheoryModel* m = d_theoryEngine->getModel();
+  TheoryModel* m = d_theoryEngine->getModel();
   if(Notice.isOn()) {
-    printModel(Notice.getStream(), m);
+    // This operator<< routine is non-const (i.e., takes a non-const Model&).
+    // This confuses the Notice() output routines, so extract the ostream
+    // from it and output it "manually."  Should be fixed by making Model
+    // accessors const.
+    Notice.getStream() << *m;
   }
 
   // We have a "fake context" for the substitution map (we don't need it
   // to be context-dependent)
   context::Context fakeContext;
-  theory::SubstitutionMap substitutions(&fakeContext);
+  SubstitutionMap substitutions(&fakeContext);
 
   for(size_t k = 0; k < m->getNumCommands(); ++k) {
     const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
@@ -2239,7 +2293,7 @@ void SmtEngine::checkModel(bool hardFailure) {
         // now check if n contains func by doing a substitution
         // [func->func2] and checking equality of the Nodes.
         // (this just a way to check if func is in n.)
-        theory::SubstitutionMap subs(&fakeContext);
+        SubstitutionMap subs(&fakeContext);
         Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY);
         subs.addSubstitution(func, func2);
         if(subs.apply(n) != n) {
@@ -2281,9 +2335,22 @@ void SmtEngine::checkModel(bool hardFailure) {
     n = Node::fromExpr(simplify(n.toExpr()));
     Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
 
+    TheoryId thy = Theory::theoryOf(n);
+    if(thy == THEORY_QUANTIFIERS || thy == THEORY_REWRITERULES) {
+      // Note this "skip" is done here, rather than above.  This is
+      // because (1) the quantifier could in principle simplify to false,
+      // which should be reported, and (2) checking for the quantifier
+      // above, before simplification, doesn't catch buried quantifiers
+      // anyway (those not at the top-level).
+      Notice() << "SmtEngine::checkModel(): -- skipping quantified assertion"
+               << endl;
+      continue;
+    }
+
     // The result should be == true.
     if(n != NodeManager::currentNM()->mkConst(true)) {
-      Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl;
+      Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
+               << endl;
       stringstream ss;
       ss << "SmtEngine::checkModel(): "
          << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
@@ -2328,8 +2395,7 @@ Proof* SmtEngine::getProof() throw(ModalException) {
 #endif /* CVC4_PROOF */
 }
 
-vector<Expr> SmtEngine::getAssertions()
-  throw(ModalException) {
+vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
@@ -2346,7 +2412,7 @@ vector<Expr> SmtEngine::getAssertions()
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
 }
 
-void SmtEngine::push() {
+void SmtEngine::push() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -2371,7 +2437,7 @@ void SmtEngine::push() {
                        << d_userContext->getLevel() << endl;
 }
 
-void SmtEngine::pop() {
+void SmtEngine::pop() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   Trace("smt") << "SMT pop()" << endl;
@@ -2415,7 +2481,7 @@ void SmtEngine::internalPush() {
   if(options::incrementalSolving()) {
     d_private->processAssertions();
     d_userContext->push();
-    d_context->push();
+    // the d_context push is done inside of the SAT solver
     d_propEngine->push();
   }
 }
@@ -2435,7 +2501,7 @@ void SmtEngine::doPendingPops() {
   Assert(d_pendingPops == 0 || options::incrementalSolving());
   while(d_pendingPops > 0) {
     d_propEngine->pop();
-    d_context->pop();
+    // the d_context pop is done inside of the SAT solver
     d_userContext->pop();
     --d_pendingPops;
   }
@@ -2503,15 +2569,9 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() {
   return d_statisticsRegistry->getStatistic(name);
 }
 
-void SmtEngine::printModel( std::ostream& out, Model* m ){
-  SmtScope smts(this);
-  Expr::dag::Scope scope(out, false);
-  Printer::getPrinter(options::outputLanguage())->toStream( out, m );
-}
-
-void SmtEngine::setUserAttribute( std::string& attr, Expr expr ){
+void SmtEngine::setUserAttribute(std::string& attr, Expr expr) {
   SmtScope smts(this);
-  d_theoryEngine->setUserAttribute( attr, expr.getNode() );
+  d_theoryEngine->setUserAttribute(attr, expr.getNode());
 }
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index df2e47b5b..3ede00510 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -290,8 +290,8 @@ class CVC4_PUBLIC SmtEngine {
   smt::SmtEngineStatistics* d_stats;
 
   /**
-   * Add to Model command.  This is used for recording a command that should be reported
-   * during a get-model call.
+   * Add to Model command.  This is used for recording a command
+   * that should be reported during a get-model call.
    */
   void addToModelCommand(Command* c);
 
@@ -369,13 +369,13 @@ public:
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const Expr& e) throw(TypeCheckingException);
+  Result query(const Expr& e) throw(TypeCheckingException, ModalException);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException);
+  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException);
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -442,12 +442,12 @@ public:
   /**
    * Push a user-level context.
    */
-  void push();
+  void push() throw(ModalException);
 
   /**
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
-  void pop();
+  void pop() throw(ModalException);
 
   /**
    * Interrupt a running query.  This can be called from another thread
@@ -572,14 +572,10 @@ public:
   }
 
   /**
-   * print model function (need this?)
+   * Set user attribute.
+   * This function is called when an attribute is set by a user.
+   * In SMT-LIBv2 this is done via the syntax (! expr :attr)
    */
-  void printModel( std::ostream& out, Model* m );
-
-  /** Set user attribute
-    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
-    *  via the syntax (! expr :attr)
-    */
   void setUserAttribute( std::string& attr, Expr expr );
 
 };/* class SmtEngine */
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index c6b73b9f6..161c90f5c 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -46,13 +46,37 @@ public:
     d_index(type.getArrayIndexType()),
     d_constituentType(type.getArrayConstituentType()),
     d_nm(NodeManager::currentNM()),
-    d_finished(false)
+    d_indexVec(),
+    d_constituentVec(),
+    d_finished(false),
+    d_arrayConst()
   {
     d_indexVec.push_back(*d_index);
     d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
     d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
   }
 
+  // An array enumerator could be large, and generally you don't want to
+  // go around copying these things; but a copy ctor is presently required
+  // by the TypeEnumerator framework.
+  ArrayEnumerator(const ArrayEnumerator& ae) throw() :
+    TypeEnumeratorBase<ArrayEnumerator>(ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
+    d_index(ae.d_index),
+    d_constituentType(ae.d_constituentType),
+    d_nm(ae.d_nm),
+    d_indexVec(ae.d_indexVec),
+    d_constituentVec(),// copied below
+    d_finished(ae.d_finished),
+    d_arrayConst(ae.d_arrayConst)
+  {
+    for(std::vector<TypeEnumerator*>::const_iterator i =
+          ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
+        i != i_end;
+        ++i) {
+      d_constituentVec.push_back(new TypeEnumerator(**i));
+    }
+  }
+
   ~ArrayEnumerator() {
     while (!d_constituentVec.empty()) {
       delete d_constituentVec.back();
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index d4b71c9e2..a4cbd720b 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -77,11 +77,6 @@ Cardinality TheoryModel::getCardinality( Type t ){
   }
 }
 
-void TheoryModel::toStream( std::ostream& out )
-{
-  out << this;
-}
-
 Node TheoryModel::getModelValue( TNode n )
 {
   if( n.isConst() ) {
@@ -550,6 +545,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     }
   } while (changed);
 
+#ifdef CVC4_ASSERTIONS
   if (fullModel) {
     // Assert that all representatives have been converted to constants
     for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
@@ -557,6 +553,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       Assert(repSet.empty());
     }
   }
+#endif /* CVC4_ASSERTIONS */
 
   Trace("model-builder") << "Copy representatives to model..." << std::endl;
   tm->d_reps.clear();
diff --git a/src/theory/model.h b/src/theory/model.h
index 0a846a3c6..a10d0a9ac 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -116,8 +116,6 @@ public:
   Expr getValue( Expr expr );
   /** get cardinality for sort */
   Cardinality getCardinality( Type t );
-  /** to stream function */
-  void toStream( std::ostream& out );
 public:
   /** print representative debug function */
   void printRepresentativeDebug( const char* c, Node r );
@@ -139,6 +137,7 @@ public:
   typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
   typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
   typedef TypeSetMap::iterator iterator;
+  typedef TypeSetMap::const_iterator const_iterator;
 private:
   TypeSetMap d_typeSet;
   TypeToTypeEnumMap d_teMap;
@@ -173,9 +172,9 @@ private:
     s->insert(n);
   }
 
-  std::set<Node>* getSet(TypeNode t)
+  std::set<Node>* getSet(TypeNode t) const
   {
-    iterator it = d_typeSet.find(t);
+    const_iterator it = d_typeSet.find(t);
     if (it == d_typeSet.end()) {
       return NULL;
     }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 33dcdd533..44eb00730 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -106,10 +106,6 @@ Node FirstOrderModel::getInterpretedValue( TNode n ){
   return TheoryModel::getInterpretedValue( n );
 }
 
-void FirstOrderModel::toStream(std::ostream& out){
-
-}
-
 
 //for evaluation of quantifier bodies
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 64e5fc904..52688a816 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -85,8 +85,6 @@ public:
 public:
   // initialize the model
   void initialize( bool considerAxioms = true );
-  /** to stream function */
-  void toStream( std::ostream& out );
 //the following functions are for evaluating quantifier bodies
 public:
   /** reset evaluation */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index de32409c5..4de6dc231 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -50,6 +50,7 @@ using namespace CVC4::theory;
 
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
+                           RemoveITE& iteRemover,
                            const LogicInfo& logicInfo)
 : d_propEngine(NULL),
   d_decisionEngine(NULL),
@@ -70,7 +71,10 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_propagationMapTimestamp(context, 0),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
+  d_iteRemover(iteRemover),
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+  d_true(),
+  d_false(),
   d_interrupted(false),
   d_inPreregister(false),
   d_factsAsserted(context, false),
@@ -1175,7 +1179,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
   std::vector<Node> additionalLemmas;
   IteSkolemMap iteSkolemMap;
   additionalLemmas.push_back(node);
-  RemoveITE::run(additionalLemmas, iteSkolemMap);
+  d_iteRemover.run(additionalLemmas, iteSkolemMap);
   additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
 
   // assert to prop engine
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8f534a62c..633d52a32 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -387,6 +387,8 @@ class TheoryEngine {
    */
   theory::LemmaStatus lemma(TNode node, bool negated, bool removable);
 
+  RemoveITE& d_iteRemover;
+
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -399,7 +401,7 @@ class TheoryEngine {
 public:
 
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* context, context::UserContext* userContext, const LogicInfo& logic);
+  TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index a4462d824..d69f0edf0 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -137,7 +137,8 @@ EXTRA_DIST = \
 	array_store_all.i \
 	ascription_type.i \
 	rational.i \
-	hash.i
+	hash.i \
+	util_model.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index e8a539615..b6e17ba29 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -27,9 +27,6 @@ using namespace std;
 
 namespace CVC4 {
 
-struct IteRewriteAttrTag {};
-typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
-
 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
@@ -43,9 +40,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
   // The result may be cached already
-  Node cachedRewrite;
   NodeManager *nodeManager = NodeManager::currentNM();
-  if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) {
+  ITECache::iterator i = d_iteCache.find(node);
+  if(i != d_iteCache.end()) {
+    Node cachedRewrite = (*i).second;
     Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
     return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
   }
@@ -64,7 +62,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 
       // Attach the skolem
-      nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
+      d_iteCache[node] = skolem;
 
       // Remove ITEs from the new assertion, rewrite it and push it to the output
       newAssertion = run(newAssertion, output, iteSkolemMap);
@@ -94,15 +92,15 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
 
     // If changes, we rewrite
     if(somethingChanged) {
-      cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
-      nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
+      Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
+      d_iteCache[node] = cachedRewrite;
       return cachedRewrite;
     } else {
-      nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+      d_iteCache[node] = Node::null();
       return node;
     }
   } else {
-    nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+    d_iteCache[node] = Node::null();
     return node;
   }
 }
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 7327d4a64..452b2d8a9 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -23,15 +23,23 @@
 #include <vector>
 #include "expr/node.h"
 #include "util/dump.h"
+#include "context/context.h"
+#include "context/cdhashmap.h"
 
 namespace CVC4 {
 
 typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveITE {
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache;
+  ITECache d_iteCache;
 
 public:
 
+  RemoveITE(context::UserContext* u) :
+    d_iteCache(u) {
+  }
+
   /**
    * Removes the ITE nodes by introducing skolem variables. All
    * additional assertions are pushed into assertions. iteSkolemMap
@@ -39,7 +47,7 @@ public:
    * assertions containing the new Boolean ite created in conjunction
    * with that skolem variable.
    */
-  static void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
+  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
 
   /**
    * Removes the ITE from the node by introducing skolem
@@ -48,8 +56,8 @@ public:
    * variables to the index in assertions containing the new Boolean
    * ite created in conjunction with that skolem variable.
    */
-  static Node run(TNode node, std::vector<Node>& additionalAssertions,
-                  IteSkolemMap& iteSkolemMap);
+  Node run(TNode node, std::vector<Node>& additionalAssertions,
+           IteSkolemMap& iteSkolemMap);
 
 };/* class RemoveTTE */
 
diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index 6dfe2c566..a5768c723 100644
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -18,6 +18,7 @@
 #include "expr/command.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/command_list.h"
+#include "printer/printer.h"
 
 #include <vector>
 
@@ -25,6 +26,13 @@ using namespace std;
 
 namespace CVC4 {
 
+std::ostream& operator<<(std::ostream& out, Model& m) {
+  smt::SmtScope smts(&m.d_smt);
+  Expr::dag::Scope scope(out, false);
+  Printer::getPrinter(options::outputLanguage())->toStream(out, m);
+  return out;
+}
+
 Model::Model() :
   d_smt(*smt::currentSmtEngine()) {
 }
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 97010dd45..07f964d46 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -29,14 +29,21 @@ namespace CVC4 {
 
 class CVC4_PUBLIC Command;
 class CVC4_PUBLIC SmtEngine;
+class CVC4_PUBLIC Model;
+
+std::ostream& operator<<(std::ostream&, Model&) CVC4_PUBLIC;
 
 class CVC4_PUBLIC Model {
-private:
+  friend std::ostream& operator<<(std::ostream&, Model&);
+
+protected:
   /** The SmtEngine we're associated to */
   const SmtEngine& d_smt;
-public:
-  /** construct the base class */
+
+  /** construct the base class; users cannot do this, only CVC4 internals */
   Model();
+
+public:
   /** virtual destructor */
   virtual ~Model() { }
   /** get number of commands to report */
@@ -48,8 +55,6 @@ public:
   virtual Expr getValue(Expr expr) = 0;
   /** get cardinality for sort */
   virtual Cardinality getCardinality(Type t) = 0;
-  /** write the model to a stream */
-  virtual void toStream(std::ostream& out) = 0;
 };/* class Model */
 
 class ModelBuilder
diff --git a/src/util/util_model.i b/src/util/util_model.i
new file mode 100644
index 000000000..0d1b3bc81
--- /dev/null
+++ b/src/util/util_model.i
@@ -0,0 +1,5 @@
+%{
+#include "util/util_model.h"
+%}
+
+%include "util/util_model.h"