Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

47 files changed, 559 insertions, 198 deletions

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index ea0b26248..54d95ced0 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): acsys
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/Assert.h b/src/util/Assert.h
index e38a3f9cf..3334de4a0 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -235,9 +235,7 @@ public:
 
 #ifdef CVC4_DEBUG
 
-#ifdef CVC4_DEBUG
 extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException;
-#endif /* CVC4_DEBUG */
 
 /**
  * Special assertion failure handling in debug mode; in non-debug
@@ -259,9 +257,9 @@ void debugAssertionFailed(const AssertionException& thisException,
     do {                                                                \
       if(EXPECT_FALSE( ! (cond) )) {                                    \
         /* save the last assertion failure */                           \
-        const char* lastException = s_debugLastException;               \
-        CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
-        CVC4::debugAssertionFailed(exception, lastException);                 \
+        const char* lastException = ::CVC4::s_debugLastException;       \
+        ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+        ::CVC4::debugAssertionFailed(exception, lastException);         \
       }                                                                 \
     } while(0)
 
@@ -271,27 +269,27 @@ void debugAssertionFailed(const AssertionException& thisException,
 #  define AlwaysAssert(cond, msg...)                                    \
      do {                                                               \
        if(EXPECT_FALSE( ! (cond) )) {                                   \
-         throw CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+         throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
        }                                                                \
      } while(0)
 #endif /* CVC4_DEBUG */
 
 #define Unreachable(msg...) \
-  throw CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unhandled(msg...) \
-  throw CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unimplemented(msg...) \
-  throw CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define InternalError(msg...) \
-  throw CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
-  throw CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw ::CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
   AlwaysAssertArgument(cond, arg, ## msg)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
   do { \
     if(EXPECT_FALSE( ! (cond) )) { \
-      throw CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
     } \
   } while(0)
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 61ff27c08..f371a4d72 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -8,7 +8,7 @@ noinst_LTLIBRARIES = libutil.la libutilcudd.la
 # libutilcudd.la is a separate library so that we can pass separate
 # compiler flags
 libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@
-libutilcudd_la_LIBADD = @CUDD_LDFLAGS@
+libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ @CUDD_LIBS@
 
 # Do not list built sources (like integer.h, rational.h, and tls.h) here!
 # Rather, list them under BUILT_SOURCES, and their .in versions under
diff --git a/src/util/array.h b/src/util/array.h
index c00cfdaa3..22605922b 100644
--- a/src/util/array.h
+++ b/src/util/array.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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h
index 418172235..c5c6b1399 100644
--- a/src/util/backtrackable.h
+++ b/src/util/backtrackable.h
@@ -2,10 +2,10 @@
 /*! \file backtrackable.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index ade08164b..f05ebaf17 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -2,7 +2,7 @@
 /*! \file bitvector.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
  ** 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)
diff --git a/src/util/bool.h b/src/util/bool.h
index d2a29c8d5..15d46b5d1 100644
--- a/src/util/bool.h
+++ b/src/util/bool.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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp
index 92534bfd4..862f1e5fc 100644
--- a/src/util/boolean_simplification.cpp
+++ b/src/util/boolean_simplification.cpp
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file boolean_simplification.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index c2da8af5b..b3dffa475 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -2,7 +2,7 @@
 /*! \file boolean_simplification.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** 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)
@@ -198,6 +198,16 @@ public:
   }
 
   /**
+   * Negates an Expr, doing all the double-negation elimination that's
+   * possible.
+   *
+   * @param e the Expr to negate (cannot be the null Expr)
+   */
+  static Expr negate(Expr e) throw(AssertionException) {
+    return negate(Node::fromExpr(e)).toExpr();
+  }
+
+  /**
    * Simplify an OR, AND, or IMPLIES.  This function is the identity
    * for all other kinds.
    */
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index e7f86c80e..6985ae38e 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -22,6 +22,11 @@
 #ifndef __CVC4__CARDINALITY_H
 #define __CVC4__CARDINALITY_H
 
+#if SWIG
+%include "util/integer.h"
+%include "util/Assert.h"
+#endif /* SWIG */
+
 #include <iostream>
 #include <utility>
 
@@ -140,6 +145,11 @@ public:
     return d_card > 0;
   }
 
+  /** Returns true iff this cardinality is infinite. */
+  bool isInfinite() const throw() {
+    return d_card < 0;
+  }
+
   /**
    * Returns true iff this cardinality is finite or countably
    * infinite.
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index aa3e6bf6b..c13b63e3f 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -49,6 +49,10 @@ bool Configuration::isTracingBuild() {
   return IS_TRACING_BUILD;
 }
 
+bool Configuration::isDumpingBuild() {
+  return IS_DUMPING_BUILD;
+}
+
 bool Configuration::isMuzzledBuild() {
   return IS_MUZZLED_BUILD;
 }
@@ -89,7 +93,11 @@ unsigned Configuration::getVersionRelease() {
   return CVC4_RELEASE;
 }
 
-string Configuration::about() {
+std::string Configuration::getVersionExtra() {
+  return CVC4_EXTRAVERSION;
+}
+
+std::string Configuration::about() {
   return CVC4_ABOUT_STRING;
 }
 
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 31a2ca3d4..cb207298c 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -53,6 +53,8 @@ public:
 
   static bool isTracingBuild();
 
+  static bool isDumpingBuild();
+
   static bool isMuzzledBuild();
 
   static bool isAssertionBuild();
@@ -73,6 +75,8 @@ public:
 
   static unsigned getVersionRelease();
 
+  static std::string getVersionExtra();
+
   static std::string about();
 
   static bool isBuiltWithGmp();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 0421273ca..13347d970 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -49,6 +49,12 @@ namespace CVC4 {
 #  define IS_TRACING_BUILD false
 #endif /* CVC4_TRACING */
 
+#ifdef CVC4_DUMPING
+#  define IS_DUMPING_BUILD true
+#else /* CVC4_DUMPING */
+#  define IS_DUMPING_BUILD false
+#endif /* CVC4_DUMPING */
+
 #ifdef CVC4_MUZZLE
 #  define IS_MUZZLED_BUILD true
 #else /* CVC4_MUZZLE */
diff --git a/src/util/congruence_closure.cpp b/src/util/congruence_closure.cpp
index 9ce902b2a..14315ac5a 100644
--- a/src/util/congruence_closure.cpp
+++ b/src/util/congruence_closure.cpp
@@ -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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index 83f6d15c0..4e690ec16 100644
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -34,7 +34,7 @@
 #include "context/cdset.h"
 #include "context/cdlist_context_memory.h"
 #include "util/exception.h"
-#include "theory/uf/morgan/stacking_map.h"
+#include "context/stacking_map.h"
 #include "util/stats.h"
 
 namespace CVC4 {
@@ -66,11 +66,11 @@ struct CongruenceOperator {
   typedef Tail_ Tail;
 };/* class CongruenceOperator<> */
 
-#define CONGRUENCE_OPERATORS_1(kind1) CongruenceOperator<kind1, EndOfCongruenceOpList>
-#define CONGRUENCE_OPERATORS_2(kind1, kind2) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_1(kind2)>
-#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_2(kind2, kind3)>
-#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_3(kind2, kind3, kind4)>
-#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) CongruenceOperator<kind1, CONGRUENCE_OPERATORS_4(kind2, kind3, kind4, kind5)>
+#define CONGRUENCE_OPERATORS_1(kind1) ::CVC4::CongruenceOperator<kind1, ::CVC4::EndOfCongruenceOpList>
+#define CONGRUENCE_OPERATORS_2(kind1, kind2) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_1(kind2)>
+#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_2(kind2, kind3)>
+#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_3(kind2, kind3, kind4)>
+#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_4(kind2, kind3, kind4, kind5)>
 
 /**
  * Returns true if the kind k is registered as a congruence operator
@@ -139,7 +139,7 @@ class CongruenceClosure {
   OutputChannel* d_out;
 
   // typedef all of these so that iterators are easy to define
-  typedef theory::uf::morgan::StackingMap<Node, NodeHashFunction> RepresentativeMap;
+  typedef context::StackingMap<Node, Node, NodeHashFunction> RepresentativeMap;
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
   typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
@@ -270,6 +270,7 @@ private:
       if(i == d_eqMap.end()) {
         ++d_newSkolemVars;
         Node v = NodeManager::currentNM()->mkSkolem(t.getType());
+        Debug("cc") << "CC made skolem " << v << std::endl;
         addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null());
         d_added.insert(v);
         d_eqMap[t] = v;
@@ -333,7 +334,7 @@ private:
    * Find the EC representative for a term t in the current context.
    */
   inline TNode find(TNode t) const throw(AssertionException) {
-    TNode rep1 = d_representative.find(t);
+    TNode rep1 = d_representative[t];
     return rep1.isNull() ? t : rep1;
   }
 
@@ -1088,7 +1089,6 @@ std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__UTIL__CONGRUENCE_CLOSURE_H */
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 926f31847..93651f1a9 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -2,7 +2,7 @@
 /*! \file datatype.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: ajreynol
  ** 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)
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 477b16f66..c64f420dd 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): ajreynol
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/debug.h b/src/util/debug.h
index 402c5bed4..ad2dbc2dd 100644
--- a/src/util/debug.h
+++ b/src/util/debug.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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index 7641472f8..46807b1f9 100644
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index 3eee8aeb6..1c2bd3ef7 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h
index c0a8cf260..2c8b842e4 100644
--- a/src/util/dynamic_array.h
+++ b/src/util/dynamic_array.h
@@ -2,10 +2,10 @@
 /*! \file dynamic_array.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -17,11 +17,10 @@
  ** \todo document this file
  **/
 
-
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTIL__DYNAMICARRAY_H
-#define __CVC4__UTIL__DYNAMICARRAY_H
+#ifndef __CVC4__UTIL__DYNAMIC_ARRAY_H
+#define __CVC4__UTIL__DYNAMIC_ARRAY_H
 
 #include "util/Assert.h"
 
@@ -29,14 +28,14 @@ namespace CVC4 {
 
 template <class T>
 class DynamicArray {
-private:
+protected:
   T* d_arr;
   unsigned d_size;
   unsigned d_allocated;
 
   bool d_callDestructor;
 
-  void grow(){
+  void grow() {
     bool empty = (d_arr == NULL);
     d_allocated = empty ? 15 : d_allocated * 2 + 1;
     unsigned allocSize = sizeof(T) * d_allocated;
@@ -48,14 +47,14 @@ private:
   }
 
 public:
-  DynamicArray(bool deallocate = false):
+  DynamicArray(bool callDestructor = false) :
     d_arr(NULL),
     d_size(0),
     d_allocated(0),
-    d_callDestructor(deallocate){
+    d_callDestructor(callDestructor) {
   }
 
-  ~DynamicArray(){
+  virtual ~DynamicArray() {
     if(d_callDestructor) {
       for(unsigned i = 0; i < d_size; ++i) {
         d_arr[i].~T();
@@ -83,12 +82,17 @@ public:
     ++d_size;
   }
 
+  const T& operator[](unsigned i) const {
+    Assert(i < d_size, "index out of bounds in DynamicArray::operator[]");
+    return d_arr[i];
+  }
+
   T& operator[](unsigned i) {
     Assert(i < d_size, "index out of bounds in DynamicArray::operator[]");
     return d_arr[i];
   }
 
-  const T& back() const{
+  const T& back() const {
     Assert(d_size > 0, "DynamicArray::back() called on empty list");
     return d_arr[d_size - 1];
   }
@@ -96,12 +100,53 @@ public:
   void pop_back() {
     Assert(d_size > 0, "DynamicArray::back() called on empty list");
     --d_size;
-    if(d_callDestructor){
-      d_arr[d_size].~T();;
+    if(d_callDestructor) {
+      d_arr[d_size].~T();
+    }
+  }
+
+  typedef T* iterator;
+  typedef const T* const_iterator;
+
+  iterator begin() { return d_arr; }
+  iterator end() { return d_arr + d_size; }
+  const_iterator begin() const { return d_arr; }
+  const_iterator end() const { return d_arr + d_size; }
+
+};/* class DynamicArray<T> */
+
+template <class T, class Ctor = T>
+class DynamicGrowingArray : public DynamicArray<T> {
+  Ctor d_ctor;
+
+public:
+  DynamicGrowingArray(bool callDestructor, const Ctor& c) :
+    DynamicArray<T>(callDestructor),
+    d_ctor(c) {
+  }
+
+  DynamicGrowingArray(bool callDestructor = false) :
+    DynamicArray<T>(callDestructor),
+    d_ctor() {
+  }
+
+  T& operator[](unsigned i) {
+    while(this->d_allocated <= i) {
+      this->grow();
+    }
+    while(this->d_size <= i) {
+      ::new((void*)(this->d_arr + this->d_size)) T(d_ctor);
+      ++this->d_size;
     }
+    return this->d_arr[i];
+  }
+
+  const T& operator[](unsigned i) const {
+    Assert(this->d_size > i);
+    return this->d_arr[i];
   }
-};/* CVC4::DynamicArray */
+};/* CVC4::DynamicGrowingArray */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UTIL__DYNAMICARRAY_H */
+#endif /* __CVC4__UTIL__DYNAMIC_ARRAY_H */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index 87102e644..7d2badbfe 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/hash.h b/src/util/hash.h
index cca60ce76..10211970f 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index 7e1b9a1aa..b2973081d 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant
  **
  ** A multiprecision integer constant.
  **/
@@ -26,8 +26,14 @@
 
 #ifdef CVC4_CLN_IMP
 #  include "util/integer_cln_imp.h"
+#  if SWIG
+     %include "util/integer_cln_imp.h"
+#  endif /* SWIG */
 #endif /* CVC4_CLN_IMP */
 
 #ifdef CVC4_GMP_IMP
 #  include "util/integer_gmp_imp.h"
+#  if SWIG
+     %include "util/integer_gmp_imp.h"
+#  endif /* SWIG */
 #endif /* CVC4_GMP_IMP */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 664027cdc..a7de8c75e 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -2,10 +2,10 @@
 /*! \file integer_cln_imp.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, dejan
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 60cee3937..237114d24 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -2,10 +2,10 @@
 /*! \file integer_gmp_imp.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index e9c5122b3..bd5048040 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -2,7 +2,7 @@
 /*! \file ite_removal.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** 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)
@@ -11,20 +11,22 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Representation of cardinality
+ ** \brief Removal of term ITEs
  **
- ** Simple class to represent a cardinality; used by the CVC4 type system
- ** give the cardinality of sorts.
+ ** Removal of term ITEs.
  **/
 
 #include <vector>
 
 #include "util/ite_removal.h"
 #include "theory/rewriter.h"
+#include "expr/command.h"
 
 using namespace CVC4;
 using namespace std;
 
+namespace CVC4 {
+
 struct IteRewriteAttrTag {};
 typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
 
@@ -34,8 +36,7 @@ void RemoveITE::run(std::vector<Node>& output) {
   }
 }
 
-Node RemoveITE::run(TNode node, std::vector<Node>& output)
-{
+Node RemoveITE::run(TNode node, std::vector<Node>& output) {
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
@@ -54,8 +55,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output)
       // Make the skolem to represent the ITE
       Node skolem = nodeManager->mkVar(nodeType);
 
+      if(Dump.isOn("declarations")) {
+        stringstream kss;
+        kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << skolem;
+        string ks = kss.str();
+        Dump("declarations") << CommentCommand(ks + " is a variable introduced due to term-level ITE removal") << endl
+                             << DeclareFunctionCommand(ks, nodeType.toType()) << endl;
+      }
+
       // The new assertion
-      Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
+      Node newAssertion =
+        nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
+                            skolem.eqNode(node[2]));
       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 
       // Attach the skolem
@@ -91,4 +102,6 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output)
     nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
     return node;
   }
-};
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index b286665cc..d68c6d933 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file ite_removal.h
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,10 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Representation of cardinality
+ ** \brief Removal of term ITEs
  **
- ** Simple class to represent a cardinality; used by the CVC4 type system
- ** give the cardinality of sorts.
+ ** Removal of term ITEs.
  **/
 
 #pragma once
@@ -38,7 +37,6 @@ public:
    */
   static Node run(TNode node, std::vector<Node>& additionalAssertions);
 
-};
+};/* class RemoveTTE */
 
-
-}
+}/* CVC4 namespace */
diff --git a/src/util/language.h b/src/util/language.h
index dbda6a315..d3405e35b 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -86,6 +86,9 @@ namespace output {
 enum CVC4_PUBLIC Language {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
+  /** Match the output language to the input language */
+  LANG_AUTO = -1,
+
   // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
   // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
   //
diff --git a/src/util/matcher.h b/src/util/matcher.h
index 5dc511bc2..6daceb8fd 100644
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file matcher.h
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
+ ** Original author: mdeters
+ ** Major contributors: ajreynol
  ** 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)
diff --git a/src/util/ntuple.h b/src/util/ntuple.h
index 4c9a033a1..4f8b73945 100644
--- a/src/util/ntuple.h
+++ b/src/util/ntuple.h
@@ -30,6 +30,11 @@ public:
   T1 first;
   T2 second;
   T3 third;
+  triple(const T1& t1, const T2& t2, const T3& t3) :
+    first(t1),
+    second(t2),
+    third(t3) {
+  }
 };/* class triple<> */
 
 template <class T1, class T2, class T3>
@@ -45,9 +50,12 @@ public:
   T2 second;
   T3 third;
   T4 fourth;
-  quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4)
-    : first(t1), second(t2), third(t3), fourth(t4)
-  { }
+  quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) :
+    first(t1),
+    second(t2),
+    third(t3),
+    fourth(t4) {
+  }
 };/* class quad<> */
 
 template <class T1, class T2, class T3, class T4>
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 9bceee931..7e6011352 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -2,7 +2,7 @@
 /*! \file options.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, cconway
+ ** Major contributors: cconway, taking
  ** Minor contributors (to current version): barrett, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -62,15 +62,16 @@ Options::Options() :
   err(&std::cerr),
   verbosity(0),
   inputLanguage(language::input::LANG_AUTO),
-  uf_implementation(MORGAN),
+  outputLanguage(language::output::LANG_AUTO),
   parseOnly(false),
+  preprocessOnly(false),
   semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
   theoryRegistration(true),
   memoryMap(false),
   strictParsing(false),
   lazyDefinitionExpansion(false),
   simplificationMode(SIMPLIFICATION_MODE_BATCH),
-  simplificationStyle(NO_SIMPLIFICATION_STYLE),
+  doStaticLearning(true),
   interactive(false),
   interactiveSetByUser(false),
   segvNoSpin(false),
@@ -95,10 +96,13 @@ Options::Options() :
 
 static const string optionsDescription = "\
    --lang | -L            force input language (default is `auto'; see --lang help)\n\
+   --output-lang          force output language (default is `auto'; see --lang help)\n\
    --version | -V         identify this CVC4 binary\n\
    --help | -h            this command line reference\n\
    --parse-only           exit after parsing input\n\
-   --preprocess-only      exit after parsing preprocessing input (and dump preprocessed assertions, unless -q)\n\
+   --preprocess-only      exit after preprocessing (useful with --stats or --dump)\n\
+   --dump=MODE            dump preprocessed assertions, T-propagations, etc., see --dump=help\n\
+   --dump-to=FILE         all dumping goes to FILE (instead of stdout)\n\
    --mmap                 memory map file input\n\
    --show-config          show CVC4 static configuration\n\
    --segv-nospin          don't spin on segfault waiting for gdb\n\
@@ -115,13 +119,13 @@ static const string optionsDescription = "\
    --stats                give statistics on exit\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
    --print-expr-types     print types with variables when printing exprs\n\
-   --uf=morgan|tim        select uninterpreted function theory implementation\n\
    --interactive          run interactively\n\
    --no-interactive       do not run interactively\n\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
    --simplification=MODE  choose simplification mode, see --simplification=help\n\
+   --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
    --replay=file          replay decisions from file\n\
    --replay-log=file      log decisions and propagations to file\n\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
@@ -140,6 +144,13 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   pl | cvc4      CVC4 presentation language\n\
   smt | smtlib   SMT-LIB format 1.2\n\
   smt2 | smtlib2 SMT-LIB format 2.0\n\
+\n\
+Languages currently supported as arguments to the --output-lang option:\n\
+  auto           match the output language to the input language\n\
+  pl | cvc4      CVC4 presentation language\n\
+  smt | smtlib   SMT-LIB format 1.2\n\
+  smt2 | smtlib2 SMT-LIB format 2.0\n\
+  ast            internal format (simple syntax-tree language)\n\
 ";
 
 static const string simplificationHelp = "\
@@ -154,18 +165,74 @@ incremental\n\
 + run nonclausal simplification and clausal propagation at each ASSERT\n\
   (and at CHECKSAT/QUERY/SUBTYPE)\n\
 \n\
-You can also specify the level of aggressiveness for the simplification\n\
-(by repeating the --simplification option):\n\
+none\n\
++ do not perform nonclausal simplification\n\
+";
+
+static const string dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
 \n\
-toplevel (default)\n\
-+ apply toplevel simplifications (things known true/false at outer level\n\
-  only)\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+  does not include any declarations or assertions.  Implied by all following\n\
+  modes.\n\
 \n\
-aggressive\n\
-+ do aggressive, local simplification across the entire formula\n\
+declarations\n\
++ Dump declarations.  Implied by all following modes.\n\
 \n\
-none\n\
-+ do not perform nonclausal simplification\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\
+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\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+  output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+  Implied by all \"stateful\" modes below and conflicts with all\n\
+  non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
+one from the assertions category (either asertions, learned, 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 propagations\n\
+as assertions; that affects the validity of the resulting correctness and\n\
+completeness queries, so of course stateful and non-stateful modes cannot\n\
+be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
+to a file.\n\
 ";
 
 string Options::getDescription() const {
@@ -192,8 +259,11 @@ enum OptionValue {
   SMTCOMP = 256, /* avoid clashing with char options */
   STATS,
   SEGV_NOSPIN,
+  OUTPUT_LANGUAGE,
   PARSE_ONLY,
   PREPROCESS_ONLY,
+  DUMP,
+  DUMP_TO,
   NO_CHECKING,
   NO_THEORY_REGISTRATION,
   USE_MMAP,
@@ -204,6 +274,7 @@ enum OptionValue {
   UF_THEORY,
   LAZY_DEFINITION_EXPANSION,
   SIMPLIFICATION_MODE,
+  NO_STATIC_LEARNING,
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_MODELS,
@@ -263,8 +334,11 @@ static struct option cmdlineOptions[] = {
   { "version"    , no_argument      , NULL, 'V'         },
   { "about"      , no_argument      , NULL, 'V'         },
   { "lang"       , required_argument, NULL, 'L'         },
+  { "output-lang", required_argument, NULL, OUTPUT_LANGUAGE },
   { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
-  { "preprocess-only", no_argument  , NULL, PREPROCESS_ONLY  },
+  { "preprocess-only", no_argument      , NULL, PREPROCESS_ONLY },
+  { "dump"       , required_argument, NULL, DUMP        },
+  { "dump-to"    , required_argument, NULL, DUMP_TO     },
   { "mmap"       , no_argument      , NULL, USE_MMAP    },
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
@@ -272,6 +346,7 @@ static struct option cmdlineOptions[] = {
   { "uf"         , required_argument, NULL, UF_THEORY   },
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
+  { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
@@ -371,6 +446,32 @@ throw(OptionException) {
       languageHelp = true;
       break;
 
+    case OUTPUT_LANGUAGE:
+      if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
+        outputLanguage = language::output::LANG_CVC4;
+        break;
+      } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
+        outputLanguage = language::output::LANG_SMTLIB;
+        break;
+      } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
+        outputLanguage = language::output::LANG_SMTLIB_V2;
+        break;
+      } else if(!strcmp(optarg, "ast")) {
+        outputLanguage = language::output::LANG_AST;
+        break;
+      } else if(!strcmp(optarg, "auto")) {
+        outputLanguage = language::output::LANG_AUTO;
+        break;
+      }
+
+      if(strcmp(optarg, "help")) {
+        throw OptionException(string("unknown language for --output-lang: `") +
+                              optarg + "'.  Try --output-lang help.");
+      }
+
+      languageHelp = true;
+      break;
+
     case 't':
       Trace.on(optarg);
       break;
@@ -396,6 +497,87 @@ throw(OptionException) {
       preprocessOnly = true;
       break;
 
+    case DUMP: {
+#ifdef CVC4_DUMPING
+      char* tokstr = optarg;
+      char* toksave;
+      while((optarg = strtok_r(tokstr, ",", &toksave)) != NULL) {
+        tokstr = NULL;
+        if(!strcmp(optarg, "benchmark")) {
+        } else if(!strcmp(optarg, "declarations")) {
+        } else if(!strcmp(optarg, "assertions")) {
+        } else if(!strcmp(optarg, "learned")) {
+        } else if(!strcmp(optarg, "clauses")) {
+        } else if(!strcmp(optarg, "t-conflicts") ||
+                  !strcmp(optarg, "t-lemmas") ||
+                  !strcmp(optarg, "t-explanations")) {
+          // These are "non-state-dumping" modes.  If state (SAT decisions,
+          // propagations, etc.) is dumped, it will interfere with the validity
+          // of these generated queries.
+          if(Dump.isOn("state")) {
+            throw OptionException(string("dump option `") + optarg +
+                                  "' conflicts with a previous, "
+                                  "state-dumping dump option.  You cannot "
+                                  "mix stateful and non-stateful dumping modes; "
+                                  "see --dump help.");
+          } else {
+            Dump.on("no-permit-state");
+          }
+        } else if(!strcmp(optarg, "state") ||
+                  !strcmp(optarg, "missed-t-conflicts") ||
+                  !strcmp(optarg, "t-propagations") ||
+                  !strcmp(optarg, "missed-t-propagations")) {
+          // These are "state-dumping" modes.  If state (SAT decisions,
+          // propagations, etc.) is not dumped, it will interfere with the
+          // validity of these generated queries.
+          if(Dump.isOn("no-permit-state")) {
+            throw OptionException(string("dump option `") + optarg +
+                                  "' conflicts with a previous, "
+                                  "non-state-dumping dump option.  You cannot "
+                                  "mix stateful and non-stateful dumping modes; "
+                                  "see --dump help.");
+          } else {
+            Dump.on("state");
+          }
+        } else if(!strcmp(optarg, "help")) {
+          puts(dumpHelp.c_str());
+          exit(1);
+        } else {
+          throw OptionException(string("unknown option for --dump: `") +
+                                optarg + "'.  Try --dump help.");
+        }
+
+        Dump.on(optarg);
+        Dump.on("benchmark");
+        if(strcmp(optarg, "benchmark")) {
+          Dump.on("declarations");
+        }
+      }
+#else /* CVC4_DUMPING */
+      throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+      break;
+    }
+
+    case DUMP_TO: {
+#ifdef CVC4_DUMPING
+      if(optarg == NULL || *optarg == '\0') {
+        throw OptionException(string("Bad file name for --dump-to"));
+      } else if(!strcmp(optarg, "-")) {
+        Dump.setStream(DumpC::dump_cout);
+      } else {
+        ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc);
+        if(!*dumpTo) {
+          throw OptionException(string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
+        }
+        Dump.setStream(*dumpTo);
+      }
+#else /* CVC4_DUMPING */
+      throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+    }
+      break;
+
     case NO_THEORY_REGISTRATION:
       theoryRegistration = false;
       break;
@@ -437,24 +619,6 @@ throw(OptionException) {
       }
       break;
 
-    case UF_THEORY:
-      {
-        if(!strcmp(optarg, "tim")) {
-          uf_implementation = Options::TIM;
-        } else if(!strcmp(optarg, "morgan")) {
-          uf_implementation = Options::MORGAN;
-        } else if(!strcmp(optarg, "help")) {
-          printf("UF implementations available:\n");
-          printf("  tim\n");
-          printf("  morgan\n");
-          exit(1);
-        } else {
-          throw OptionException(string("unknown option for --uf: `") +
-                                optarg + "'.  Try --uf help.");
-        }
-      }
-      break;
-
     case LAZY_DEFINITION_EXPANSION:
       lazyDefinitionExpansion = true;
       break;
@@ -464,12 +628,8 @@ throw(OptionException) {
         simplificationMode = SIMPLIFICATION_MODE_BATCH;
       } else if(!strcmp(optarg, "incremental")) {
         simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
-      } else if(!strcmp(optarg, "aggressive")) {
-        simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE;
-      } else if(!strcmp(optarg, "toplevel")) {
-        simplificationStyle = TOPLEVEL_SIMPLIFICATION_STYLE;
       } else if(!strcmp(optarg, "none")) {
-        simplificationStyle = NO_SIMPLIFICATION_STYLE;
+        simplificationMode = SIMPLIFICATION_MODE_NONE;
       } else if(!strcmp(optarg, "help")) {
         puts(simplificationHelp.c_str());
         exit(1);
@@ -479,6 +639,10 @@ throw(OptionException) {
       }
       break;
 
+    case NO_STATIC_LEARNING:
+      doStaticLearning = false;
+      break;
+
     case INTERACTIVE:
       interactive = true;
       interactiveSetByUser = true;
@@ -622,6 +786,7 @@ throw(OptionException) {
       printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
       printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
       printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
+      printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
       printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
       printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
       printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
diff --git a/src/util/options.h b/src/util/options.h
index ce2bc71e7..c4e115b08 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -2,8 +2,8 @@
 /*! \file options.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): dejan, taking
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -71,11 +71,8 @@ struct CVC4_PUBLIC Options {
   /** The input language */
   InputLanguage inputLanguage;
 
-  /** Enumeration of UF implementation choices */
-  typedef enum { TIM, MORGAN } UfImplementation;
-
-  /** Which implementation of uninterpreted function theory to use */
-  UfImplementation uf_implementation;
+  /** The output language */
+  OutputLanguage outputLanguage;
 
   /** Should we print the help message? */
   bool help;
@@ -112,21 +109,16 @@ struct CVC4_PUBLIC Options {
     /** Simplify the assertions as they come in */
     SIMPLIFICATION_MODE_INCREMENTAL,
     /** Simplify the assertions all together once a check is requested */
-    SIMPLIFICATION_MODE_BATCH
+    SIMPLIFICATION_MODE_BATCH,
+    /** Don't do simplification */
+    SIMPLIFICATION_MODE_NONE
   } SimplificationMode;
 
-  /** When to perform nonclausal simplifications. */
+  /** When/whether to perform nonclausal simplifications. */
   SimplificationMode simplificationMode;
 
-  /** Enumeration of simplification styles (how much to simplify). */
-  typedef enum {
-    AGGRESSIVE_SIMPLIFICATION_STYLE,
-    TOPLEVEL_SIMPLIFICATION_STYLE,
-    NO_SIMPLIFICATION_STYLE
-  } SimplificationStyle;
-
-  /** Style of nonclausal simplifications to perform. */
-  SimplificationStyle simplificationStyle;
+  /** Whether to perform the static learning pass. */
+  bool doStaticLearning;
 
   /** Whether we're in interactive mode or not */
   bool interactive;
@@ -229,34 +221,18 @@ struct CVC4_PUBLIC Options {
 };/* struct Options */
 
 inline std::ostream& operator<<(std::ostream& out,
-                                Options::UfImplementation uf) CVC4_PUBLIC;
-
-inline std::ostream& operator<<(std::ostream& out,
-                                Options::UfImplementation uf) {
-  switch(uf) {
-  case Options::TIM:
-    out << "TIM";
-    break;
-  case Options::MORGAN:
-    out << "MORGAN";
-    break;
-  default:
-    out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]";
-  }
-
-  return out;
-}
-
-inline std::ostream& operator<<(std::ostream& out,
                                 Options::SimplificationMode mode) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out,
                                 Options::SimplificationMode mode) {
   switch(mode) {
+  case Options::SIMPLIFICATION_MODE_INCREMENTAL:
+    out << "SIMPLIFICATION_MODE_INCREMENTAL";
+    break;
   case Options::SIMPLIFICATION_MODE_BATCH:
     out << "SIMPLIFICATION_MODE_BATCH";
     break;
-  case Options::SIMPLIFICATION_MODE_INCREMENTAL:
-    out << "SIMPLIFICATION_MODE_INCREMENTAL";
+  case Options::SIMPLIFICATION_MODE_NONE:
+    out << "SIMPLIFICATION_MODE_NONE";
     break;
   default:
     out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 29de4c360..3823f7be6 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -40,6 +40,8 @@ MessageC MessageChannel CVC4_PUBLIC (&cout);
 NoticeC NoticeChannel CVC4_PUBLIC (&cout);
 ChatC ChatChannel CVC4_PUBLIC (&cout);
 TraceC TraceChannel CVC4_PUBLIC (&cout);
+std::ostream DumpC::dump_cout(cout.rdbuf());// copy cout stream buffer
+DumpC DumpChannel CVC4_PUBLIC (&DumpC::dump_cout);
 
 #ifndef CVC4_MUZZLE
 
@@ -155,6 +157,40 @@ int TraceC::printf(std::string tag, const char* fmt, ...) {
 
 #  endif /* CVC4_TRACING */
 
+#  ifdef CVC4_DUMPING
+
+int DumpC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int DumpC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+#  endif /* CVC4_DUMPING */
+
 #endif /* ! CVC4_MUZZLE */
 
 }/* CVC4 namespace */
diff --git a/src/util/output.h b/src/util/output.h
index 6d0f27f2a..e096ff028 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): cconway, taking, dejan
+ ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -190,6 +190,7 @@ public:
   bool on (std::string tag) { d_tags.insert(tag); return true; }
   bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
   bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
 
   bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
@@ -297,6 +298,7 @@ public:
   bool on (std::string tag) { d_tags.insert(tag); return true; }
   bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
   bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
 
   bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
@@ -305,6 +307,51 @@ public:
   std::ostream& getStream() { return *d_os; }
 };/* class TraceC */
 
+/** The dump output class */
+class CVC4_PUBLIC DumpC {
+  std::set<std::string> d_tags;
+  std::ostream* d_os;
+
+public:
+  /**
+   * A copy of cout for use by the dumper.  This is important because
+   * it has different settings (e.g., the expr printing depth is always
+   * unlimited). */
+  static std::ostream dump_cout;
+
+  explicit DumpC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class DumpC */
+
 /** The debug output singleton */
 extern DebugC DebugChannel CVC4_PUBLIC;
 /** The warning output singleton */
@@ -317,6 +364,8 @@ extern NoticeC NoticeChannel CVC4_PUBLIC;
 extern ChatC ChatChannel CVC4_PUBLIC;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC4_PUBLIC;
+/** The dump output singleton */
+extern DumpC DumpChannel CVC4_PUBLIC;
 
 #ifdef CVC4_MUZZLE
 
@@ -326,6 +375,7 @@ extern TraceC TraceChannel CVC4_PUBLIC;
 #  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
 #  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+#  define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel
 
 inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
@@ -335,6 +385,8 @@ inline int NoticeC::printf(const char* fmt, ...) { return 0; }
 inline int ChatC::printf(const char* fmt, ...) { return 0; }
 inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; }
 
 #else /* CVC4_MUZZLE */
 
@@ -356,6 +408,13 @@ inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
 inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
 #  endif /* CVC4_TRACING */
+#  ifdef CVC4_DUMPING
+#    define Dump ::CVC4::DumpChannel
+#  else /* CVC4_DUMPING */
+#    define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel
+inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_DUMPING */
 
 #endif /* CVC4_MUZZLE */
 
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index 88c488290..17c1e31fc 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -11,9 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Multi-precision rational constants.
+ ** \brief A multi-precision rational constant
  **
- ** Multi-precision rational constants.
+ ** A multi-precision rational constant.
  **/
 
 // this is used to avoid a public header dependence on cvc4autoconfig.h
@@ -26,8 +26,14 @@
 
 #ifdef CVC4_CLN_IMP
 #  include "util/rational_cln_imp.h"
+#  if SWIG
+     %include "util/rational_cln_imp.h"
+#  endif /* SWIG */
 #endif /* CVC4_CLN_IMP */
 
 #ifdef CVC4_GMP_IMP
 #  include "util/rational_gmp_imp.h"
+#  if SWIG
+     %include "util/rational_gmp_imp.h"
+#  endif /* SWIG */
 #endif /* CVC4_GMP_IMP */
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 057100d10..22e3a7ad1 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index b97484ff1..a883500f9 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 5921b8fd3..b26172d66 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 167e0fc22..b97965169 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 8e1db27c4..8a2bcf3b2 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file result.h
+/*! \file result.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/result.h b/src/util/result.h
index 7da1dc0b7..c4733eab9 100644
--- a/src/util/result.h
+++ b/src/util/result.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  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 376a8a224..63ce23874 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -2,10 +2,10 @@
 /*! \file sexpr.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 70d486ff6..474d8fa7a 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -2,10 +2,10 @@
 /*! \file stats.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -20,6 +20,13 @@
 #include "util/stats.h"
 #include "expr/node_manager.h"
 #include "expr/expr_manager_scope.h"
+#include "lib/clock_gettime.h"
+
+#ifdef CVC4_STATISTICS_ON
+#  define __CVC4_USE_STATISTICS true
+#else
+#  define __CVC4_USE_STATISTICS false
+#endif
 
 using namespace CVC4;
 
@@ -67,6 +74,24 @@ StatisticsRegistry::const_iterator StatisticsRegistry::end() {
   return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
 }/* StatisticsRegistry::end() */
 
+void TimerStat::start() {
+  if(__CVC4_USE_STATISTICS) {
+    AlwaysAssert(!d_running);
+    clock_gettime(CLOCK_MONOTONIC, &d_start);
+    d_running = true;
+  }
+}/* TimerStat::start() */
+
+void TimerStat::stop() {
+  if(__CVC4_USE_STATISTICS) {
+    AlwaysAssert(d_running);
+    ::timespec end;
+    clock_gettime(CLOCK_MONOTONIC, &end);
+    d_data += end - d_start;
+    d_running = false;
+  }
+}/* TimerStat::stop() */
+
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
     d_em(&em), d_stat(stat) {
   ExprManagerScope ems(*d_em);
diff --git a/src/util/stats.h b/src/util/stats.h
index a94733595..7d3e33a6f 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -32,7 +32,6 @@
 #include <vector>
 
 #include "util/Assert.h"
-#include "lib/clock_gettime.h"
 
 namespace CVC4 {
 
@@ -702,27 +701,13 @@ public:
   }
 
   /** Start the timer. */
-  void start() {
-    if(__CVC4_USE_STATISTICS) {
-      AlwaysAssert(!d_running);
-      clock_gettime(CLOCK_MONOTONIC, &d_start);
-      d_running = true;
-    }
-  }
+  void start();
 
   /**
    * Stop the timer and update the statistic value with the
    * accumulated time.
    */
-  void stop() {
-    if(__CVC4_USE_STATISTICS) {
-      AlwaysAssert(d_running);
-      ::timespec end;
-      clock_gettime(CLOCK_MONOTONIC, &end);
-      d_data += end - d_start;
-      d_running = false;
-    }
-  }
+  void stop();
 
 };/* class TimerStat */
 
diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index 61c48fa8d..5d772b576 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -2,10 +2,10 @@
 /*! \file trans_closure.cpp
  ** \verbatim
  ** Original author: barrett
- ** Major contributors: none
+ ** Major contributors: ajreynol
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index 951a32a63..ef04d7af5 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -2,8 +2,8 @@
 /*! \file trans_closure.h
  ** \verbatim
  ** Original author: barrett
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: ajreynol
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences