This commit is a merge from the "betterstats" branch, which:

* Makes Options an "omnipresent thread-local global" (like the notion
  of the "current NodeManager" was already).  Options::current() accesses
  this structure.
* Removes Options from constructors and data structures everywhere
  (this cleans up a lot of things).
* No longer uses StatisticsRegistry statically.  An instance of the
  registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
  the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
  compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
  registry; this is needed by main() to reach in and get the registry,
  for flushing statistics at the end.

32 files changed, 359 insertions, 292 deletions

diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index f36c8a6e3..09aa3ed9f 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -21,6 +21,7 @@
 #include "expr/declaration_scope.h"
 #include "expr/expr.h"
 #include "expr/type.h"
+#include "expr/expr_manager_scope.h"
 #include "context/cdmap.h"
 #include "context/cdset.h"
 #include "context/context.h"
@@ -48,11 +49,15 @@ DeclarationScope::~DeclarationScope() {
   delete d_context;
 }
 
-void DeclarationScope::bind(const std::string& name, Expr obj) throw() {
+void DeclarationScope::bind(const std::string& name, Expr obj) throw(AssertionException) {
+  CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+  ExprManagerScope ems(obj);
   d_exprMap->insert(name, obj);
 }
 
-void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw() {
+void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw(AssertionException) {
+  CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+  ExprManagerScope ems(obj);
   d_exprMap->insert(name, obj);
   d_functions->insert(obj);
 }
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 9acc46b5f..17140c850 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -77,7 +77,7 @@ public:
    * @param name an identifier
    * @param obj the expression to bind to <code>name</code>
    */
-  void bind(const std::string& name, Expr obj) throw();
+  void bind(const std::string& name, Expr obj) throw(AssertionException);
 
   /**
    * Bind a function body to a name in the current scope.  If
@@ -90,7 +90,7 @@ public:
    * @param name an identifier
    * @param obj the expression to bind to <code>name</code>
    */
-  void bindDefinedFunction(const std::string& name, Expr obj) throw();
+  void bindDefinedFunction(const std::string& name, Expr obj) throw(AssertionException);
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index 4fc3f02d4..c1da288a4 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__EXPR_MANAGER_SCOPE_H
 #define __CVC4__EXPR_MANAGER_SCOPE_H
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 9b8511de9..5d34fb53c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -95,9 +95,8 @@ ExprManager::ExprManager(const Options& options) :
 }
 
 ExprManager::~ExprManager() {
-  delete d_nodeManager;
-  delete d_ctxt;
 #ifdef CVC4_STATISTICS_ON   
+  NodeManagerScope nms(d_nodeManager);
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
     if (d_exprStatistics[i] != NULL) {
       StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
@@ -111,6 +110,8 @@ ExprManager::~ExprManager() {
     }
   }
 #endif
+  delete d_nodeManager;
+  delete d_ctxt;
 }
 
 BooleanType ExprManager::booleanType() const {
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 3b9c41973..68655aed9 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -658,17 +658,12 @@ private:
   expr::NodeValue* constructNV();
   expr::NodeValue* constructNV() const;
 
-  inline void maybeCheckType(const TNode n) const {
-    /* force an immediate type check, if early type checking is
-       enabled and the current node isn't a variable or constant */
-    if( d_nm->d_earlyTypeChecking ) {
-      kind::MetaKind mk = n.getMetaKind();
-      if( mk != kind::metakind::VARIABLE 
-          && mk != kind::metakind::CONSTANT ) {
-        d_nm->getType(n, true);
-      }
-    }
-  }
+#ifdef CVC4_DEBUG
+  void maybeCheckType(const TNode n) const
+    throw(TypeCheckingExceptionPrivate, AssertionException);
+#else /* CVC4_DEBUG */
+  inline void maybeCheckType(const TNode n) const throw() { }
+#endif /* CVC4_DEBUG */
 
 public:
 
@@ -716,6 +711,7 @@ public:
 
 #include "expr/node.h"
 #include "expr/node_manager.h"
+#include "util/options.h"
 
 namespace CVC4 {
 
@@ -1240,6 +1236,22 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
   }
 }
 
+#ifdef CVC4_DEBUG
+template <unsigned nchild_thresh>
+inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
+    throw(TypeCheckingExceptionPrivate, AssertionException) {
+  /* force an immediate type check, if early type checking is
+     enabled and the current node isn't a variable or constant */
+  if( d_nm->getOptions()->earlyTypeChecking ) {
+    kind::MetaKind mk = n.getMetaKind();
+    if( mk != kind::metakind::VARIABLE 
+        && mk != kind::metakind::CONSTANT ) {
+      d_nm->getType(n, true);
+    }
+  }
+}
+#endif /* CVC4_DEBUG */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 9006bf4d9..207f1f492 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -29,6 +29,7 @@
 
 #include "util/Assert.h"
 #include "util/options.h"
+#include "util/stats.h"
 #include "util/tls.h"
 
 #include <algorithm>
@@ -84,22 +85,28 @@ struct NVReclaim {
 };
 
 NodeManager::NodeManager(context::Context* ctxt) :
-  d_attrManager(ctxt) {
-  Options options;
-  init(options);
+  d_optionsAllocated(new Options()),
+  d_options(d_optionsAllocated),
+  d_statisticsRegistry(new StatisticsRegistry()),
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_inReclaimZombies(false) {
+  init();
 }
 
 
 NodeManager::NodeManager(context::Context* ctxt, 
                          const Options& options) :
-  d_attrManager(ctxt) {
-  init(options);
+  d_optionsAllocated(NULL),
+  d_options(&options),
+  d_statisticsRegistry(new StatisticsRegistry()),
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_inReclaimZombies(false) {
+  init();
 }
 
-inline void NodeManager::init(const Options& options) {
-  d_nodeUnderDeletion = NULL;
-  d_inReclaimZombies = false;
-  d_earlyTypeChecking = options.earlyTypeChecking;
+inline void NodeManager::init() {
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -145,6 +152,9 @@ NodeManager::~NodeManager() {
     }
     Debug("gc:leaks") << ":end:" << std::endl;
   }
+
+  delete d_statisticsRegistry;
+  delete d_optionsAllocated;
 }
 
 void NodeManager::reclaimZombies() {
@@ -440,7 +450,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
   Debug("getType") << "getting type for " << n << std::endl;
 
-  if(needsCheck && !d_earlyTypeChecking) {
+  if(needsCheck && !d_options->earlyTypeChecking) {
     /* Iterate and compute the children bottom up. This avoids stack
        overflows in computeType() when the Node graph is really deep,
        which should only affect us when we're type checking lazily. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d8a690da5..36720bbb3 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -39,10 +39,11 @@
 #include "context/context.h"
 #include "util/configuration_private.h"
 #include "util/tls.h"
+#include "util/options.h"
 
 namespace CVC4 {
 
-struct Options;
+class StatisticsRegistry;
 
 namespace expr {
 
@@ -77,6 +78,10 @@ class NodeManager {
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
+  const Options* d_optionsAllocated;
+  const Options* d_options;
+  StatisticsRegistry* d_statisticsRegistry;
+
   NodeValuePool d_nodeValuePool;
 
   expr::attr::AttributeManager d_attrManager;
@@ -120,12 +125,6 @@ class NodeManager {
   Node d_operators[kind::LAST_KIND];
 
   /**
-   * Whether to do early type checking (only effective in debug
-   * builds; other builds never do early type checking).
-   */
-  bool d_earlyTypeChecking;
-
-  /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
    * NodeValue.  In particular, "non-inlined" constants are permitted
@@ -247,7 +246,7 @@ class NodeManager {
   TypeNode computeType(TNode n, bool check = false)
     throw (TypeCheckingExceptionPrivate, AssertionException);
 
-  void init(const Options& options);
+  void init();
 
 public:
 
@@ -255,9 +254,19 @@ public:
   explicit NodeManager(context::Context* ctxt, const Options& options);
   ~NodeManager();
 
-  /** The node manager in the current context. */
+  /** The node manager in the current public-facing CVC4 library context */
   static NodeManager* currentNM() { return s_current; }
 
+  /** Get this node manager's options */
+  const Options* getOptions() const {
+    return d_options;
+  }
+
+  /** Get this node manager's statistics registry */
+  StatisticsRegistry* getStatisticsRegistry() const {
+    return d_statisticsRegistry;
+  }
+
   // general expression-builders
 
   /** Create a node with one child. */
@@ -600,13 +609,19 @@ public:
 
   NodeManagerScope(NodeManager* nm) :
     d_oldNodeManager(NodeManager::s_current) {
+    // There are corner cases where nm can be NULL and it's ok.
+    // For example, if you write { Expr e; }, then when the null
+    // Expr is destructed, there's no active node manager.
+    //Assert(nm != NULL);
     NodeManager::s_current = nm;
+    Options::s_current = nm ? nm->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << NodeManager::s_current << "\n";
   }
 
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
+    Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << "returning to " << NodeManager::s_current << "\n";
   }
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 0d12e7011..46a456d50 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -69,7 +69,7 @@ bool Type::isNull() const {
 }
 
 Type& Type::operator=(const Type& t) {
-  NodeManagerScope nms(d_nodeManager);
+  NodeManagerScope nms(t.d_nodeManager);
   if(this != &t) {
     *d_typeNode = *t.d_typeNode;
     d_nodeManager = t.d_nodeManager;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 563fa472e..655562512 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -51,7 +51,8 @@ void doCommand(SmtEngine&, Command*);
 void printUsage();
 
 namespace CVC4 {
-  namespace main {/* Global options variable */
+  namespace main {
+    /** Global options variable */
     Options options;
 
     /** Full argv[0] */
@@ -59,6 +60,9 @@ namespace CVC4 {
 
     /** Just the basename component of argv[0] */
     const char *progName;
+
+    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
+    CVC4::StatisticsRegistry* pStatistics;
   }
 }
 
@@ -104,8 +108,8 @@ int main(int argc, char* argv[]) {
     *options.out << "unknown" << endl;
 #endif
     *options.err << "CVC4 Error:" << endl << e << endl;
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(*options.err);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(*options.err);
     }
     exit(1);
   } catch(bad_alloc) {
@@ -113,8 +117,8 @@ int main(int argc, char* argv[]) {
     *options.out << "unknown" << endl;
 #endif
     *options.err << "CVC4 ran out of memory." << endl;
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(*options.err);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(*options.err);
     }
     exit(1);
   } catch(...) {
@@ -171,17 +175,41 @@ int runCvc4(int argc, char* argv[]) {
     options.interactive = inputFromStdin && isatty(fileno(stdin));
   }
 
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+  }
+
   // Create the expression manager
   ExprManager exprMgr(options);
 
   // Create the SmtEngine
-  SmtEngine smt(&exprMgr, options);
+  SmtEngine smt(&exprMgr);
+
+  // signal handlers need access
+  pStatistics = smt.getStatisticsRegistry();
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
   ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(&s_statFilename);
+  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
 
   if(options.inputLanguage == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
@@ -200,26 +228,7 @@ int runCvc4(int argc, char* argv[]) {
     }
   }
 
-  // Determine which messages to show based on smtcomp_mode and verbosity
-  if(Configuration::isMuzzledBuild()) {
-    Debug.setStream(CVC4::null_os);
-    Trace.setStream(CVC4::null_os);
-    Notice.setStream(CVC4::null_os);
-    Chat.setStream(CVC4::null_os);
-    Message.setStream(CVC4::null_os);
-    Warning.setStream(CVC4::null_os);
-  } else {
-    if(options.verbosity < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-
+  if(!Configuration::isMuzzledBuild()) {
     OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
     Debug.getStream() << Expr::setlanguage(language);
     Trace.getStream() << Expr::setlanguage(language);
@@ -229,7 +238,6 @@ int runCvc4(int argc, char* argv[]) {
     Warning.getStream() << Expr::setlanguage(language);
   }
 
-
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
@@ -273,10 +281,10 @@ int runCvc4(int argc, char* argv[]) {
 #endif
 
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  RegisterStatistic statSatResultReg(&s_statSatResult);
+  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
 
   if(options.statistics) {
-    StatisticsRegistry::flushStatistics(*options.err);
+    smt.getStatisticsRegistry()->flushStatistics(*options.err);
   }
 
   return returnValue;
diff --git a/src/main/main.h b/src/main/main.h
index 2c2773a92..7e0bf6b65 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -21,6 +21,7 @@
 
 #include "util/options.h"
 #include "util/exception.h"
+#include "util/stats.h"
 #include "cvc4autoconfig.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
@@ -31,10 +32,13 @@ namespace CVC4 {
 namespace main {
 
 /** Full argv[0] */
-extern const char *progPath;
+extern const char* progPath;
 
 /** Just the basename component of argv[0] */
-extern const char *progName;
+extern const char* progName;
+
+/** A reference to the StatisticsRegistry for use by the signal handlers */
+extern CVC4::StatisticsRegistry* pStatistics;
 
 /**
  * If true, will not spin on segfault even when CVC4_DEBUG is on.
diff --git a/src/main/util.cpp b/src/main/util.cpp
index eb360818b..bf42025a0 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -51,8 +51,8 @@ bool segvNoSpin = false;
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   abort();
 }
@@ -60,8 +60,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   abort();
 }
@@ -85,8 +85,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(cerr);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(cerr);
     }
     abort();
   } else {
@@ -105,8 +105,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   } else if(addr < 10*1024) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -118,8 +118,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(cerr);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(cerr);
     }
     abort();
   } else {
@@ -131,8 +131,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -155,8 +155,8 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(cerr);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(cerr);
     }
     set_terminate(default_terminator);
   } else {
@@ -168,8 +168,8 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
@@ -181,16 +181,16 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   default_terminator();
 #else /* CVC4_DEBUG */
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+  if(options.statistics && pStatistics != NULL) {
+    pStatistics->flushStatistics(cerr);
   }
   default_terminator();
 #endif /* CVC4_DEBUG */
diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README
index af71779d5..cd3b638d6 100644
--- a/src/prop/minisat/CVC4-README
+++ b/src/prop/minisat/CVC4-README
@@ -13,7 +13,7 @@ the trunk.
 The PropEngine then uses the following
 
 // Create the sat solver (this is the proxy, which will create minisat)
-d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
+d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
 // Add some clauses
 d_cnfStream->convertAndAssert(node);
 // Check for satisfiabilty 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 44709630d..4da3aa842 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -56,13 +56,12 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te,
-                       Context* context, const Options& opts) :
+PropEngine::PropEngine(TheoryEngine* te, Context* context) :
   d_inCheckSat(false),
   d_theoryEngine(te),
   d_context(context) {
   Debug("prop") << "Constructing the PropEngine" << endl;
-  d_satSolver = new SatSolver(this, d_theoryEngine, d_context, opts);
+  d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
   d_satSolver->setCnfStream(d_cnfStream);
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b43c2d859..e1a1c08d7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -48,9 +48,6 @@ class PropEngine {
    */
   bool d_inCheckSat;
 
-  /** The global options */
-  //const Options d_options;
-
   /** The theory engine we will be using */
   TheoryEngine *d_theoryEngine;
 
@@ -72,7 +69,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*, context::Context*, const Options&);
+  PropEngine(TheoryEngine*, context::Context*);
 
   /**
    * Destructor.
diff --git a/src/prop/sat.h b/src/prop/sat.h
index f9e135c0d..e583f4da0 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -131,9 +131,6 @@ class SatSolver : public SatInputInterface {
   /** Context we will be using to synchronzie the sat solver */
   context::Context* d_context;
 
-  /** Remember the options */
-  // Options* d_options;
-
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
      sub-class for each solver. */
@@ -208,9 +205,8 @@ public:
   };
 
   SatSolver(PropEngine* propEngine,
-                   TheoryEngine* theoryEngine,
-                   context::Context* context,
-                   const Options& options);
+            TheoryEngine* theoryEngine,
+            context::Context* context);
 
   ~SatSolver();
 
@@ -261,7 +257,7 @@ public:
 #ifdef __CVC4_USE_MINISAT
 
 inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
-                     context::Context* context, const Options& options) :
+                     context::Context* context) :
   d_propEngine(propEngine),
   d_cnfStream(NULL),
   d_theoryEngine(theoryEngine),
@@ -269,12 +265,13 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_statistics()
 {
   // Create the solver
-  d_minisat = new Minisat::SimpSolver(this, d_context, options.incrementalSolving);
+  d_minisat = new Minisat::SimpSolver(this, d_context,
+                                      Options::current()->incrementalSolving);
   // Setup the verbosity
-  d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1;
+  d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
 
   // No random choices
-  if(Debug.isOn("no_rnd_decisions")){
+  if(Debug.isOn("no_rnd_decisions")) {
     d_minisat->random_var_freq = 0;
   }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fe5e55ae6..cb6dd3460 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -120,28 +120,17 @@ public:
 
 using namespace CVC4::smt;
 
-SmtEngine::SmtEngine(ExprManager* em) throw() :
-  d_exprManager(em) {
-  Options opts;
-  init(opts);
-}
-
-SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() :
-  d_exprManager(em){
-  init(opts);
-}
-
-void SmtEngine::init(const Options& opts) throw() {
-  d_context = d_exprManager->getContext();
-  d_userContext = new Context();
-
-  d_nodeManager = d_exprManager->getNodeManager();
+SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
+  d_context(em->getContext()),
+  d_userContext(new Context()),
+  d_exprManager(em),
+  d_nodeManager(d_exprManager->getNodeManager()) {
 
   NodeManagerScope nms(d_nodeManager);
 
   // We have mutual dependancy here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context, opts);
+  d_theoryEngine = new TheoryEngine(d_context);
 
   // Add the theories
   d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>();
@@ -149,7 +138,7 @@ void SmtEngine::init(const Options& opts) throw() {
   d_theoryEngine->addTheory<theory::arith::TheoryArith>();
   d_theoryEngine->addTheory<theory::arrays::TheoryArrays>();
   d_theoryEngine->addTheory<theory::bv::TheoryBV>();
-  switch(opts.uf_implementation) {
+  switch(Options::current()->uf_implementation) {
   case Options::TIM:
     d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>();
     break;
@@ -157,30 +146,22 @@ void SmtEngine::init(const Options& opts) throw() {
     d_theoryEngine->addTheory<theory::uf::morgan::TheoryUFMorgan>();
     break;
   default:
-    Unhandled(opts.uf_implementation);
+    Unhandled(Options::current()->uf_implementation);
   }
 
-  d_propEngine = new PropEngine(d_theoryEngine, d_context, opts);
+  d_propEngine = new PropEngine(d_theoryEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
   d_assertionList = NULL;
-  d_interactive = opts.interactive;
-  if(d_interactive) {
+  if(Options::current()->interactive) {
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
   d_assignments = NULL;
   d_haveAdditions = false;
   d_queryMade = false;
-
-  d_typeChecking = opts.typeChecking;
-  d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion;
-  d_produceModels = opts.produceModels;
-  d_produceAssignments = opts.produceAssignments;
-
-  d_incrementalSolving = opts.incrementalSolving;
 }
 
 void SmtEngine::shutdown() {
@@ -354,7 +335,7 @@ void SmtEngine::defineFunction(Expr func,
                                Expr formula) {
   Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
   NodeManagerScope nms(d_nodeManager);
-  Type formulaType = formula.getType(d_typeChecking);// type check body
+  Type formulaType = formula.getType(Options::current()->typeChecking);// type check body
   Type funcType = func.getType();
   Type rangeType = funcType.isFunction() ?
     FunctionType(funcType).getRangeType() : funcType;
@@ -445,7 +426,7 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
   throw(NoSuchFunctionException, AssertionException) {
 
   Node n;
-  if(!smt.d_lazyDefinitionExpansion) {
+  if(!Options::current()->lazyDefinitionExpansion) {
     Debug("expand") << "have: " << n << endl;
     n = expandDefinitions(smt, in);
     Debug("expand") << "made: " << n << endl;
@@ -486,7 +467,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
 }
 
 void SmtEngine::ensureBoolean(const BoolExpr& e) {
-  Type type = e.getType(d_typeChecking);
+  Type type = e.getType(Options::current()->typeChecking);
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
     stringstream ss;
@@ -501,7 +482,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << endl;
-  if(d_queryMade && !d_incrementalSolving) {
+  if(d_queryMade && !Options::current()->incrementalSolving) {
     throw ModalException("Cannot make multiple queries unless "
                          "incremental solving is enabled "
                          "(try --incremental)");
@@ -522,7 +503,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << endl;
-  if(d_queryMade && !d_incrementalSolving) {
+  if(d_queryMade && !Options::current()->incrementalSolving) {
     throw ModalException("Cannot make multiple queries unless "
                          "incremental solving is enabled "
                          "(try --incremental)");
@@ -554,7 +535,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
 Expr SmtEngine::simplify(const Expr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
-  if( d_typeChecking ) {
+  if( Options::current()->typeChecking ) {
     e.getType(true);// ensure expr is type-checked at this point
   }
   Debug("smt") << "SMT simplify(" << e << ")" << endl;
@@ -566,9 +547,9 @@ Expr SmtEngine::simplify(const Expr& e) {
 Expr SmtEngine::getValue(const Expr& e)
   throw(ModalException, AssertionException) {
   Assert(e.getExprManager() == d_exprManager);
-  Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point
+  Type type = e.getType(Options::current()->typeChecking);// ensure expr is type-checked at this point
   Debug("smt") << "SMT getValue(" << e << ")" << endl;
-  if(!d_produceModels) {
+  if(!Options::current()->produceModels) {
     const char* msg =
       "Cannot get value when produce-models options is off.";
     throw ModalException(msg);
@@ -601,7 +582,7 @@ Expr SmtEngine::getValue(const Expr& e)
 
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Type type = e.getType(d_typeChecking);
+  Type type = e.getType(Options::current()->typeChecking);
   // must be Boolean
   CheckArgument( type.isBoolean(), e,
                  "expected Boolean-typed variable or function application "
@@ -615,7 +596,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
                    n.getMetaKind() == kind::metakind::VARIABLE ), e,
                  "expected variable or defined-function application "
                  "in addToAssignment(),\ngot %s", e.toString().c_str() );
-  if(!d_produceAssignments) {
+  if(!Options::current()->produceAssignments) {
     return false;
   }
   if(d_assignments == NULL) {
@@ -628,7 +609,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
 
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Debug("smt") << "SMT getAssignment()" << endl;
-  if(!d_produceAssignments) {
+  if(!Options::current()->produceAssignments) {
     const char* msg =
       "Cannot get the current assignment when "
       "produce-assignments option is off.";
@@ -680,7 +661,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
   Debug("smt") << "SMT getAssertions()" << endl;
-  if(!d_interactive) {
+  if(!Options::current()->interactive) {
     const char* msg =
       "Cannot query the current assertion list when not in interactive mode.";
     throw ModalException(msg);
@@ -692,7 +673,7 @@ vector<Expr> SmtEngine::getAssertions()
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT push()" << endl;
-  if(!d_incrementalSolving) {
+  if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
   }
   d_userLevels.push_back(d_userContext->getLevel());
@@ -704,7 +685,7 @@ void SmtEngine::push() {
 void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT pop()" << endl;
-  if(!d_incrementalSolving) {
+  if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
   }
   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
@@ -731,4 +712,8 @@ void SmtEngine::internalPush() {
   d_propEngine->push();
 }
 
+StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
+  return d_exprManager->d_nodeManager->getStatisticsRegistry();
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c884b2c5f..b872985fb 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -49,6 +49,8 @@ class NodeHashFunction;
 
 class TheoryEngine;
 
+class StatisticsRegistry;
+
 namespace context {
   class Context;
 }/* CVC4::context namespace */
@@ -139,44 +141,11 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_queryMade;
 
-  /** 
-   * Whether or not to type check input expressions.
-   */
-  bool d_typeChecking;
-
-  /**
-   * Whether we're being used in an interactive setting.
-   */
-  bool d_interactive;
-
-  /**
-   * Whether we expand function definitions lazily.
-   */
-  bool d_lazyDefinitionExpansion;
-
-  /**
-   * Whether getValue() is enabled.
-   */
-  bool d_produceModels;
-
-  /**
-   * Whether getAssignment() is enabled.
-   */
-  bool d_produceAssignments;
-
-  /**
-   * Whether multiple queries can be made, and also push/pop is enabled.
-   */
-  bool d_incrementalSolving;
-
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
   Result d_status;
 
-  /** Called by the constructors to setup fields. */
-  void init(const Options& opts) throw();
-
   /**
    * This is called by the destructor, just before destroying the
    * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
@@ -215,12 +184,7 @@ public:
   /**
    * Construct an SmtEngine with the given expression manager.
    */
-  SmtEngine(ExprManager* em) throw();
-
-  /**
-   * Construct an SmtEngine with the given expression manager and user options.
-   */
-  SmtEngine(ExprManager* em, const Options& opts) throw();
+  SmtEngine(ExprManager* em) throw(AssertionException);
 
   /**
    * Destruct the SMT engine.
@@ -336,12 +300,10 @@ public:
    */
   void pop();
 
-  /** Enable type checking. Forces a type check on any Expr parameter
-      to an SmtEngine method. */
-  void enableTypeChecking() { d_typeChecking = true; }
-
-  /** Disable type checking. */
-  void disableTypeChecking() { d_typeChecking = false; }
+  /**
+   * Permit access to the underlying StatisticsRegistry.
+   */
+  StatisticsRegistry* getStatisticsRegistry() const;
 
 };/* class SmtEngine */
 
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 3bd5dc91d..4905f4dc5 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -255,3 +255,21 @@ void ArithPriorityQueue::clear(){
   Assert(d_varOrderQueue.empty());
   Assert(d_diffQueue.empty());
 }
+
+std::ostream& CVC4::theory::arith::operator<<(std::ostream& out, ArithPriorityQueue::PivotRule rule) {
+  switch(rule) {
+  case ArithPriorityQueue::MINIMUM:
+    out << "MINIMUM";
+    break;
+  case ArithPriorityQueue::BREAK_TIES:
+    out << "BREAK_TIES";
+    break;
+  case ArithPriorityQueue::MAXIMUM:
+    out << "MAXIMUM";
+    break;
+  default:
+    out << "PivotRule!UNKNOWN";
+  }
+
+  return out;
+}
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 4c83d648f..f912d7753 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -294,6 +294,7 @@ private:
   Statistics d_statistics;
 };
 
+std::ostream& operator<<(std::ostream& out, ArithPriorityQueue::PivotRule rule);
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index cecbefdee..09cfabdc8 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -261,7 +261,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
   }else if(reduction.getKind() == kind::LT){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::NOT, geq);
-  }else if( Options::rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
+  }else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::AND, geq, leq);
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 91f0bccfc..b1ebe2972 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -48,7 +48,21 @@ public:
     d_numVariables(0),
     d_delayedLemmas(),
     d_ZERO(0)
-  {}
+  {
+    switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
+    case Options::MINIMUM:
+      d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
+      break;
+    case Options::BREAK_TIES:
+      d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
+      break;
+    case Options::MAXIMUM:
+      d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
+      break;
+    default:
+      Unhandled(rule);
+    }
+  }
 
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
@@ -179,24 +193,6 @@ private:
   Node generateConflictBelow(ArithVar conflictVar);
 
 public:
-  void notifyOptions(const Options& opt){
-    switch(opt.pivotRule){
-    case Options::MINIMUM:
-      d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
-      break;
-    case Options::BREAK_TIES:
-      d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
-      break;
-    case Options::MAXIMUM:
-      d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
-      break;
-    default:
-      Unhandled(opt.pivotRule);
-    }
-  }
-
-
-public:
   /**
    * Checks to make sure the assignment is consistent with the tableau.
    * This code is for debugging.
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index a90e37bdc..85f554849 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -171,9 +171,6 @@ public:
 
   std::string identify() const { return std::string("TheoryArith"); }
 
-  void notifyOptions(const Options& opt) {
-    d_simplex.notifyOptions(opt);
-  }
 private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 72341869d..b5122d3c5 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -405,11 +405,6 @@ public:
    */
   virtual std::string identify() const = 0;
 
-  /**
-   * Notify the theory of the current set of options.
-   */
-  virtual void notifyOptions(const Options& opt) { }
-
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2411956f5..d1040e6fc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -68,7 +68,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
     d_engine->getSharedTermManager()->addEq(fact);
   }
 
-  if(d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
+  if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
     list<TNode> toReg;
     toReg.push_back(fact);
 
@@ -126,17 +126,15 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
         d_engine->theoryOf(n)->registerTerm(n);
       }
     }
-  }/* d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
+  }/* Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
 }
 
-TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
+TheoryEngine::TheoryEngine(context::Context* ctxt) :
   d_propEngine(NULL),
   d_context(ctxt),
   d_theoryOut(this, ctxt),
-  d_theoryRegistration(opts.theoryRegistration),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
-  d_opts(opts),
   d_statistics() {
 
   Rewriter::init();
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b773a84ee..be2e6e271 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -155,14 +155,12 @@ class TheoryEngine {
    */
   Node removeITEs(TNode t);
 
-  const Options& d_opts;
-
 public:
 
   /**
    * Construct a theory engine.
    */
-  TheoryEngine(context::Context* ctxt, const Options& opts);
+  TheoryEngine(context::Context* ctxt);
 
   /**
    * Destroy a theory engine.
@@ -177,8 +175,6 @@ public:
     TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
     d_theoryTable[theory->getId()] = theory;
     d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
-
-    theory->notifyOptions(d_opts);
   }
 
   SharedTermManager* getSharedTermManager() {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 1b73361c3..4bcc9a37d 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -40,6 +40,8 @@ using namespace CVC4;
 
 namespace CVC4 {
 
+CVC4_THREADLOCAL(const Options*) Options::s_current = NULL;
+
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
 #else /* CVC4_DEBUG */
@@ -75,6 +77,7 @@ Options::Options() :
   typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
   earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
   incrementalSolving(false),
+  rewriteArithEqualities(false),
   pivotRule(MINIMUM)
 {
 }
@@ -88,9 +91,9 @@ static const string optionsDescription = "\
    --show-config          show CVC4 static configuration\n\
    --segv-nospin          don't spin on segfault waiting for gdb\n\
    --lazy-type-checking   type check expressions only when necessary (default)\n\
-   --eager-type-checking  type check expressions immediately on creation\n\
+   --eager-type-checking  type check expressions immediately on creation (debug builds only)\n\
    --no-type-checking     never type check expressions\n\
-   --no-checking          disable ALL semantic checks, including type checks \n\
+   --no-checking          disable ALL semantic checks, including type checks\n\
    --no-theory-registration disable theory reg (not safe for some theories)\n\
    --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
    --verbose | -v         increase verbosity (repeatable)\n\
@@ -106,7 +109,8 @@ static const string optionsDescription = "\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
-   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic \n\
+   --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
+   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\
    --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
@@ -213,14 +217,14 @@ static struct option cmdlineOptions[] = {
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
-  { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
-  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
-  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
-  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
-  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
-  { "incremental", no_argument, NULL, INCREMENTAL},
+  { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
+  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING },
+  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
+  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
+  { "incremental", no_argument, NULL, INCREMENTAL },
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
-  { "rewrite-arithmetic-equalities" , no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES},
+  { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -484,8 +488,23 @@ throw(OptionException) {
   return optind;
 }
 
-bool Options::rewriteArithEqualities = false;
+std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) {
+  switch(rule) {
+  case Options::MINIMUM:
+    out << "MINIMUM";
+    break;
+  case Options::BREAK_TIES:
+    out << "BREAK_TIES";
+    break;
+  case Options::MAXIMUM:
+    out << "MAXIMUM";
+    break;
+  default:
+    out << "ArithPivotRule!UNKNOWN";
+  }
 
+  return out;
+}
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
diff --git a/src/util/options.h b/src/util/options.h
index 32ce77a64..efbd48900 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -26,6 +26,7 @@
 
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/tls.h"
 
 namespace CVC4 {
 
@@ -39,13 +40,23 @@ public:
 
 struct CVC4_PUBLIC Options {
 
+  /** The current Options in effect */
+  static CVC4_THREADLOCAL(const Options*) s_current;
+
+  /** Get the current Options in effect */
+  static inline const Options* current() {
+    return s_current;
+  }
+
+  /** The name of the binary (e.g. "cvc4") */
   std::string binary_name;
 
+  /** Whether to collect statistics during this run */
   bool statistics;
 
-  std::istream* in;
-  std::ostream* out;
-  std::ostream* err;
+  std::istream* in; /*< The input stream to use */
+  std::ostream* out; /*< The output stream to use */
+  std::ostream* err; /*< The error stream to use */
 
   /* -1 means no output */
   /* 0 is normal (and default) -- warnings only */
@@ -117,8 +128,10 @@ struct CVC4_PUBLIC Options {
   /** Whether incemental solving (push/pop) */
   bool incrementalSolving;
 
-  static bool rewriteArithEqualities;
+  /** Whether to rewrite equalities in arithmetic theory */
+  bool rewriteArithEqualities;
 
+  /** The pivot rule for arithmetic */
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
   ArithPivotRule pivotRule;
 
@@ -130,7 +143,14 @@ struct CVC4_PUBLIC Options {
    * suitable as an argument to printf. */
   std::string getDescription() const;
 
+  /**
+   * Print overall command-line option usage message, prefixed by
+   * "msg"---which could be an error message causing the usage
+   * output in the first place, e.g. "no such option --foo"
+   */
   static void printUsage(const std::string msg, std::ostream& out);
+
+  /** Print help for the --lang command line option */
   static void printLanguageHelp(std::ostream& out);
 
   /**
@@ -156,6 +176,8 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule);
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__OPTIONS_H */
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 5be9525a9..428f051e0 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -18,13 +18,33 @@
  **/
 
 #include "util/stats.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager_scope.h"
 
 using namespace CVC4;
 
-StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats;
-
 std::string Stat::s_delim(",");
 
+StatisticsRegistry* StatisticsRegistry::current() {
+  return NodeManager::currentNM()->getStatisticsRegistry();
+}
+
+void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  AlwaysAssert(registeredStats.find(s) == registeredStats.end());
+  registeredStats.insert(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::registerStat() */
+
+void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  AlwaysAssert(registeredStats.find(s) != registeredStats.end());
+  registeredStats.erase(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::unregisterStat() */
+
 void StatisticsRegistry::flushStatistics(std::ostream& out) {
 #ifdef CVC4_STATISTICS_ON
   for(StatSet::iterator i = d_registeredStats.begin();
@@ -34,5 +54,28 @@ void StatisticsRegistry::flushStatistics(std::ostream& out) {
     s->flushStat(out);
     out << std::endl;
   }
-#endif
+#endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::flushStatistics() */
+
+StatisticsRegistry::const_iterator StatisticsRegistry::begin() {
+  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin();
+}/* StatisticsRegistry::begin() */
+
+StatisticsRegistry::const_iterator StatisticsRegistry::end() {
+  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
+}/* StatisticsRegistry::end() */
+
+RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
+    d_em(&em), d_stat(stat) {
+  ExprManagerScope ems(*d_em);
+  StatisticsRegistry::registerStat(d_stat);
+}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */
+
+RegisterStatistic::~RegisterStatistic() {
+  if(d_em != NULL) {
+    ExprManagerScope ems(*d_em);
+    StatisticsRegistry::unregisterStat(d_stat);
+  } else {
+    StatisticsRegistry::unregisterStat(d_stat);
+  }
+}/* RegisterStatistic::~RegisterStatistic() */
diff --git a/src/util/stats.h b/src/util/stats.h
index bf962d02b..53acc9b1b 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -42,6 +42,8 @@ namespace CVC4 {
 #  define __CVC4_USE_STATISTICS false
 #endif
 
+class ExprManager;
+
 class CVC4_PUBLIC Stat;
 
 inline std::ostream& operator<<(std::ostream& os, const ::timespec& t);
@@ -49,9 +51,6 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t);
 /**
  * The main statistics registry.  This registry maintains the list of
  * currently active statistics and is able to "flush" them all.
- *
- * The statistics registry is only used statically; one does not
- * construct a statistics registry.
  */
 class CVC4_PUBLIC StatisticsRegistry {
 private:
@@ -64,42 +63,42 @@ private:
   typedef std::set< Stat*, StatCmp > StatSet;
 
   /** The set of currently active statistics */
-  static StatSet d_registeredStats;
+  StatSet d_registeredStats;
 
-  /** Private default constructor undefined (no construction permitted). */
-  StatisticsRegistry() CVC4_UNDEFINED;
   /** Private copy constructor undefined (no copy permitted). */
   StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
 
 public:
 
+  /** Construct a statistics registry */
+  StatisticsRegistry() { }
+
   /** An iterator type over a set of statistics */
   typedef StatSet::const_iterator const_iterator;
 
+  /** Get a pointer to the current statistics registry */
+  static StatisticsRegistry* current();
+
   /** Flush all statistics to the given output stream. */
-  static void flushStatistics(std::ostream& out);
+  void flushStatistics(std::ostream& out);
 
   /** Register a new statistic, making it active. */
-  static inline void registerStat(Stat* s) throw(AssertionException);
+  static void registerStat(Stat* s) throw(AssertionException);
 
   /** Unregister an active statistic, making it inactive. */
-  static inline void unregisterStat(Stat* s) throw(AssertionException);
+  static void unregisterStat(Stat* s) throw(AssertionException);
 
   /**
    * Get an iterator to the beginning of the range of the set of active
    * (registered) statistics.
    */
-  static inline const_iterator begin() {
-    return d_registeredStats.begin();
-  }
+  static const_iterator begin();
 
   /**
    * Get an iterator to the end of the range of the set of active
    * (registered) statistics.
    */
-  static inline const_iterator end() {
-    return d_registeredStats.end();
-  }
+  static const_iterator end();
 
 };/* class StatisticsRegistry */
 
@@ -175,24 +174,6 @@ inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1,
   return s1->getName() < s2->getName();
 }
 
-inline void StatisticsRegistry::registerStat(Stat* s)
-  throw(AssertionException) {
-  if(__CVC4_USE_STATISTICS) {
-    AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
-    d_registeredStats.insert(s);
-  }
-}/* StatisticsRegistry::registerStat() */
-
-
-inline void StatisticsRegistry::unregisterStat(Stat* s)
-  throw(AssertionException) {
-  if(__CVC4_USE_STATISTICS) {
-    AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
-    d_registeredStats.erase(s);
-  }
-}/* StatisticsRegistry::unregisterStat() */
-
-
 /**
  * A class to represent a "read-only" data statistic of type T.  Adds to
  * the Stat base class the pure virtual function getData(), which returns
@@ -766,14 +747,20 @@ public:
  * registration and unregistration.
  */
 class RegisterStatistic {
+  ExprManager* d_em;
   Stat* d_stat;
 public:
   RegisterStatistic(Stat* stat) : d_stat(stat) {
+    Assert(StatisticsRegistry::current() != NULL,
+           "You need to specify an expression manager "
+           "on which to set the statistic");
     StatisticsRegistry::registerStat(d_stat);
   }
-  ~RegisterStatistic() {
-    StatisticsRegistry::unregisterStat(d_stat);
-  }
+
+  RegisterStatistic(ExprManager& em, Stat* stat);
+
+  ~RegisterStatistic();
+
 };/* class RegisterStatistic */
 
 #undef __CVC4_USE_STATISTICS
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index 89d5174e3..c64c1463e 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -30,7 +30,7 @@ using namespace std;
 int main() {
   ExprManager em;
   Options opts;
-  SmtEngine smt(&em, opts);
+  SmtEngine smt(&em);
   Result r = smt.query(em.mkConst(true));
 
   return r == Result::VALID ? 0 : 1;
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index 76f3712f0..e88f11673 100644
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -59,8 +59,7 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    Options options;
-    d_theoryEngine = new TheoryEngine(d_ctxt, options);
+    d_theoryEngine = new TheoryEngine(d_ctxt);
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index f99698204..26908ec6e 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -242,8 +242,7 @@ public:
     d_nullChannel = new FakeOutputChannel;
 
     // create the TheoryEngine
-    Options options;
-    d_theoryEngine = new TheoryEngine(d_ctxt, options);
+    d_theoryEngine = new TheoryEngine(d_ctxt);
 
     d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >();
     d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >();