Add SmtGlobals Class

- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.

36 files changed, 394 insertions, 314 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index f39006788..1cd617b64 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -53,7 +53,6 @@
 
 #pragma once
 
-#include "expr/result.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/error_set.h"
@@ -61,6 +60,7 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
 #include "util/dense_map.h"
+#include "util/result.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1e3b21b17..3c5c1c414 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -28,9 +28,11 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-  , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
+                         OutputChannel& out, Valuation valuation,
+                         const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+    , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
 {}
 
 TheoryArith::~TheoryArith(){
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index a0a8e2c89..d26a120ae 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -46,7 +46,9 @@ private:
   KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer");
 
 public:
-  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
+              Valuation valuation, const LogicInfo& logicInfo,
+              SmtGlobals* globals);
   virtual ~TheoryArith();
 
   /**
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ab800f10d..bf1810331 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -33,7 +33,6 @@
 #include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/result.h"
 #include "expr/statistics_registry.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"  // for incrementalSolving()
@@ -70,6 +69,7 @@
 #include "util/dense_map.h"
 #include "util/integer.h"
 #include "util/rational.h"
+#include "util/result.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 0c2a704e8..32c12eba7 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -31,7 +31,6 @@
 #include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/result.h"
 #include "expr/statistics_registry.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
@@ -67,6 +66,7 @@
 #include "util/dense_map.h"
 #include "util/integer.h"
 #include "util/rational.h"
+#include "util/result.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 2863fad8a..ab57eb260 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -51,50 +51,52 @@ const bool d_solveWrite2 = false;
   //bool d_lazyRIntro1 = true;
   //bool d_eagerIndexSplitting = false;
 
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
-  d_numRow("theory::arrays::number of Row lemmas", 0),
-  d_numExt("theory::arrays::number of Ext lemmas", 0),
-  d_numProp("theory::arrays::number of propagations", 0),
-  d_numExplain("theory::arrays::number of explanations", 0),
-  d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
-  d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
-  d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
-  d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
-  d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
-  d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
-  d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
-  d_ppFacts(u),
-  //  d_ppCache(u),
-  d_literalsToPropagate(c),
-  d_literalsToPropagateIndex(c, 0),
-  d_isPreRegistered(c),
-  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
-  d_conflict(c, false),
-  d_backtracker(c),
-  d_infoMap(c, &d_backtracker),
-  d_mergeQueue(c),
-  d_mergeInProgress(false),
-  d_RowQueue(c),
-  d_RowAlreadyAdded(u),
-  d_sharedArrays(c),
-  d_sharedOther(c),
-  d_sharedTerms(c, false),
-  d_reads(c),
-  d_constReadsList(c),
-  d_constReadsContext(new context::Context()),
-  d_contextPopper(c, d_constReadsContext),
-  d_skolemIndex(c, 0),
-  d_decisionRequests(c),
-  d_permRef(c),
-  d_modelConstraints(c),
-  d_lemmasSaved(c),
-  d_defValues(c),
-  d_readTableContext(new context::Context()),
-  d_arrayMerges(c),
-  d_inCheckModel(false)
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
+                           OutputChannel& out, Valuation valuation,
+                           const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals),
+      d_numRow("theory::arrays::number of Row lemmas", 0),
+      d_numExt("theory::arrays::number of Ext lemmas", 0),
+      d_numProp("theory::arrays::number of propagations", 0),
+      d_numExplain("theory::arrays::number of explanations", 0),
+      d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
+      d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
+      d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
+      d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
+      d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
+      d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
+      d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
+      d_ppFacts(u),
+      //      d_ppCache(u),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_isPreRegistered(c),
+      d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
+      d_conflict(c, false),
+      d_backtracker(c),
+      d_infoMap(c, &d_backtracker),
+      d_mergeQueue(c),
+      d_mergeInProgress(false),
+      d_RowQueue(c),
+      d_RowAlreadyAdded(u),
+      d_sharedArrays(c),
+      d_sharedOther(c),
+      d_sharedTerms(c, false),
+      d_reads(c),
+      d_constReadsList(c),
+      d_constReadsContext(new context::Context()),
+      d_contextPopper(c, d_constReadsContext),
+      d_skolemIndex(c, 0),
+      d_decisionRequests(c),
+      d_permRef(c),
+      d_modelConstraints(c),
+      d_lemmasSaved(c),
+      d_defValues(c),
+      d_readTableContext(new context::Context()),
+      d_arrayMerges(c),
+      d_inCheckModel(false)
 {
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 28d994835..98cba0420 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -126,7 +126,9 @@ class TheoryArrays : public Theory {
 
   public:
 
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
+               Valuation valuation, const LogicInfo& logicInfo,
+               SmtGlobals* globals);
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index a4a3757cd..246f1e7e8 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -28,9 +28,11 @@ namespace booleans {
 
 class TheoryBool : public Theory {
 public:
-  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {
-  }
+  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out,
+             Valuation valuation, const LogicInfo& logicInfo,
+             SmtGlobals* globals)
+      : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, globals)
+  {}
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index fa6e8ab5c..2fbc0e402 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -27,8 +27,10 @@ namespace builtin {
 
 class TheoryBuiltin : public Theory {
 public:
-  TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
+  TheoryBuiltin(context::Context* c, context::UserContext* u,
+                OutputChannel& out, Valuation valuation,
+                const LogicInfo& logicInfo, SmtGlobals* globals)
+      : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, globals) {}
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
 
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index b93d0561e..7b071b9e9 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -19,17 +19,17 @@
 #ifndef __CVC4__BITBLASTER_TEMPLATE_H
 #define __CVC4__BITBLASTER_TEMPLATE_H
 
-
-#include "expr/node.h"
-#include <vector>
 #include <ext/hash_map>
+#include <vector>
 
-#include "context/cdhashmap.h"
 #include "bitblast_strategies_template.h"
+#include "context/cdhashmap.h"
+#include "expr/node.h"
 #include "expr/resource_manager.h"
 #include "prop/sat_solver.h"
-#include "theory/valuation.h"
+#include "smt/smt_globals.h"
 #include "theory/theory_registrar.h"
+#include "theory/valuation.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -84,25 +84,25 @@ protected:
   // caches and mappings
   TermDefMap d_termCache;
   ModelCache d_modelCache;
-  
+
   void initAtomBBStrategies();
   void initTermBBStrategies();
 protected:
   /// function tables for the various bitblasting strategies indexed by node kind
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
-  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; 
-  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; 
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
 public:
-  TBitblaster(); 
+  TBitblaster();
   virtual ~TBitblaster() {}
-  virtual void bbAtom(TNode node) = 0; 
+  virtual void bbAtom(TNode node) = 0;
   virtual void bbTerm(TNode node, Bits&  bits) = 0;
   virtual void makeVariable(TNode node, Bits& bits) = 0;
   virtual T getBBAtom(TNode atom) const = 0;
   virtual bool hasBBAtom(TNode atom) const = 0;
   virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
-  
-  
+
+
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
   void storeBBTerm(TNode term, const Bits& bits);
@@ -114,10 +114,10 @@ public:
    */
   Node getTermModel(TNode node, bool fullModel);
   void invalidateModelCache();
-}; 
+};
 
 
-class TheoryBV; 
+class TheoryBV;
 
 class TLazyBitblaster :  public TBitblaster<Node> {
   typedef std::vector<Node> Bits;
@@ -127,19 +127,20 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   class MinisatNotify : public prop::BVSatSolverInterface::Notify {
     prop::CnfStream* d_cnf;
     TheoryBV *d_bv;
-    TLazyBitblaster* d_lazyBB; 
+    TLazyBitblaster* d_lazyBB;
   public:
     MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv)
     : d_cnf(cnf)
     , d_bv(bv)
     , d_lazyBB(lbv)
     {}
+
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
     void spendResource(unsigned ammount);
     void safePoint(unsigned ammount);
   };
-  
+
   TheoryBV *d_bv;
   context::Context* d_ctx;
 
@@ -155,24 +156,25 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
                                     Only used when bvEagerPropagate option enabled. */
   TNodeSet d_variables;
-  TNodeSet d_bbAtoms; 
+  TNodeSet d_bbAtoms;
   AbstractionModule* d_abstraction;
   bool d_emptyNotify;
 
   context::CDO<bool> d_satSolverFullModel;
-  
+
   void addAtom(TNode atom);
   bool hasValue(TNode a);
-  Node getModelFromSatSolver(TNode a, bool fullModel);  
+  Node getModelFromSatSolver(TNode a, bool fullModel);
+
 public:
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
   Node getBBAtom(TNode atom) const;
   void storeBBAtom(TNode atom, Node atom_bb);
-  bool hasBBAtom(TNode atom) const; 
+  bool hasBBAtom(TNode atom) const;
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
   ~TLazyBitblaster() throw();
-  /** 
+  /**
    * Pushes the assumption literal associated with node to the SAT
    * solver assumption queue. 
    * 
@@ -261,26 +263,27 @@ class EagerBitblaster : public TBitblaster<Node> {
   TNodeSet d_variables;
 
   Node getModelFromSatSolver(TNode a, bool fullModel);
-  bool isSharedTerm(TNode node); 
+  bool isSharedTerm(TNode node);
 
 public:
+  EagerBitblaster(theory::bv::TheoryBV* theory_bv);
+  ~EagerBitblaster();
+
   void addAtom(TNode atom);
   void makeVariable(TNode node, Bits& bits);
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
   Node getBBAtom(TNode node) const;
-  bool hasBBAtom(TNode atom) const; 
+  bool hasBBAtom(TNode atom) const;
   void bbFormula(TNode formula);
   void storeBBAtom(TNode atom, Node atom_bb);
-  EagerBitblaster(theory::bv::TheoryBV* theory_bv); 
-  ~EagerBitblaster();
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
   void collectModelInfo(TheoryModel* m, bool fullModel);
 };
 
 class BitblastingRegistrar: public prop::Registrar {
-  EagerBitblaster* d_bitblaster; 
+  EagerBitblaster* d_bitblaster;
 public:
   BitblastingRegistrar(EagerBitblaster* bb)
     : d_bitblaster(bb)
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 37e1bd9ba..ff13867cc 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -33,15 +33,16 @@ class AigBitblaster;
  * BitblastSolver
  */
 class EagerBitblastSolver {
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
   AssertionSet d_assertionSet;
   /** Bitblasters */
   EagerBitblaster* d_bitblaster;
   AigBitblaster* d_aigBitblaster;
   bool d_useAig;
-  TheoryBV* d_bv; 
+  TheoryBV* d_bv;
+
 public:
-  EagerBitblastSolver(theory::bv::TheoryBV* bv); 
+  EagerBitblastSolver(theory::bv::TheoryBV* bv);
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 261a0b1c4..8ef49f786 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -35,7 +35,7 @@ class TheoryModel;
 
 namespace bv {
 
-class TLazyBitblaster; 
+class TLazyBitblaster;
 class TheoryBV;
 
 class BVQuickCheck {
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 77461163c..0e066eefb 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -18,8 +18,8 @@
 
 #pragma once
 
-#include "theory/bv/bv_subtheory.h"
 #include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -58,7 +58,7 @@ class BitblastSolver : public SubtheorySolver {
   BVQuickCheck* d_quickCheck;
   QuickXPlain* d_quickXplain;
   //  Node getModelValueRec(TNode node);
-  void setConflict(TNode conflict); 
+  void setConflict(TNode conflict);
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index ec2bfd9c0..39606ca7c 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -46,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_nullContext = new context::Context();
 
   d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
+                                           d_nullContext, d_bv->globals());
 
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 3c2b4ed78..b8173cb8b 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -26,12 +26,13 @@
 #include "theory/theory_model.h"
 #include "theory_bv_utils.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv; 
+namespace CVC4 {
+namespace theory {
+namespace bv {
 
 
-TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
+TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
+                                 const std::string name, bool emptyNotify)
   : TBitblaster<Node>()
   , d_bv(bv)
   , d_ctx(c)
@@ -44,13 +45,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st
   , d_satSolverFullModel(c, false)
   , d_name(name)
   , d_statistics(name) {
+
   d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
   d_nullRegistrar = new prop::NullRegistrar();
   d_nullContext = new context::Context();
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_nullRegistrar,
-                                           d_nullContext);
-  
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
+                                           d_nullContext, d_bv->globals());
+
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
@@ -59,7 +60,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st
 }
 
 void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
-  d_abstraction = abs; 
+  d_abstraction = abs;
 }
 
 TLazyBitblaster::~TLazyBitblaster() throw() {
@@ -103,8 +104,8 @@ void TLazyBitblaster::bbAtom(TNode node) {
     if (expansion.getKind() == kind::CONST_BOOLEAN) {
       atom_bb = expansion;
     } else {
-      Assert (expansion.getKind() == kind::AND); 
-      std::vector<Node> atoms; 
+      Assert (expansion.getKind() == kind::AND);
+      std::vector<Node> atoms;
       for (unsigned i = 0; i < expansion.getNumChildren(); ++i) {
         Node normalized_i = Rewriter::rewrite(expansion[i]);
         Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ?
@@ -481,7 +482,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 }
 
 void TLazyBitblaster::clearSolver() {
-  Assert (d_ctx->getLevel() == 0); 
+  Assert (d_ctx->getLevel() == 0);
   delete d_satSolver;
   delete d_satSolverNotify;
   delete d_cnfStream;
@@ -492,16 +493,19 @@ void TLazyBitblaster::clearSolver() {
   d_bbAtoms.clear();
   d_variables.clear();
   d_termCache.clear();
-  
-  invalidateModelCache();  
+
+  invalidateModelCache();
   // recreate sat solver
   d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_nullRegistrar,
-                                           d_nullContext);
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
+                                           d_nullContext, d_bv->globals());
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
   d_satSolver->setNotify(d_satSolverNotify);
 }
+
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4039fceec..0505035c7 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -31,38 +31,40 @@
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
 using namespace CVC4::context;
-
-using namespace std;
 using namespace CVC4::theory::bv::utils;
+using namespace std;
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
-    d_context(c),
-    d_alreadyPropagatedSet(c),
-    d_sharedTermsSet(c),
-    d_subtheories(),
-    d_subtheoryMap(),
-    d_statistics(),
-    d_staticLearnCache(),
-    d_lemmasAdded(c, false),
-    d_conflict(c, false),
-    d_invalidateModelCache(c, true),
-    d_literalsToPropagate(c),
-    d_literalsToPropagateIndex(c, 0),
-    d_propagatedBy(c),
-    d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule()),
-    d_isCoreTheory(false),
-    d_calledPreregister(false)
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
+                   OutputChannel& out, Valuation valuation,
+                   const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals),
+      d_context(c),
+      d_alreadyPropagatedSet(c),
+      d_sharedTermsSet(c),
+      d_subtheories(),
+      d_subtheoryMap(),
+      d_statistics(),
+      d_staticLearnCache(),
+      d_lemmasAdded(c, false),
+      d_conflict(c, false),
+      d_invalidateModelCache(c, true),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_propagatedBy(c),
+      d_eagerSolver(NULL),
+      d_abstractionModule(new AbstractionModule()),
+      d_isCoreTheory(false),
+      d_calledPreregister(false)
 {
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     d_eagerSolver = new EagerBitblastSolver(this);
-    return; 
+    return;
   }
 
   if (options::bitvectorEqualitySolver()) {
@@ -70,7 +72,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_subtheories.push_back(core_solver);
     d_subtheoryMap[SUB_CORE] = core_solver;
   }
-  
+
   if (options::bitvectorInequalitySolver()) {
     SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
     d_subtheories.push_back(ineq_solver);
@@ -101,7 +103,7 @@ TheoryBV::~TheoryBV() {
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    return; 
+    return;
   }
   if (options::bitvectorEqualitySolver()) {
     dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
@@ -179,31 +181,31 @@ void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) {
       d_BVDivByZeroAckerman[size] = TNodeSet();
     }
     d_BVDivByZeroAckerman[size].insert(term[0]);
-    seen.insert(term); 
+    seen.insert(term);
   } else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) {
     unsigned size = utils::getSize(term[0]);
     if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) {
       d_BVRemByZeroAckerman[size] = TNodeSet();
     }
     d_BVRemByZeroAckerman[size].insert(term[0]);
-    seen.insert(term); 
+    seen.insert(term);
   }
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
-    collectNumerators(term[i], seen); 
+    collectNumerators(term[i], seen);
   }
-  seen.insert(term); 
+  seen.insert(term);
 }
 
 void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
   Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
-  
+
   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   AlwaysAssert(!options::incrementalSolving());
-  TNodeSet seen; 
+  TNodeSet seen;
   for (unsigned i = 0; i < assertions.size(); ++i) {
-    collectNumerators(assertions[i], seen); 
+    collectNumerators(assertions[i], seen);
   }
-  
+
   // process division UF
   Debug("bv-ackermanize") << "Process division UF...\n";
   for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) {
@@ -215,13 +217,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
         TNode arg1 = *i;
         TNode arg2 = *j;
         TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1);
-        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); 
+        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2);
 
         Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
         Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
         Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
         Debug("bv-ackermanize") << "  " << lemma << "\n";
-        assertions.push_back(lemma); 
+        assertions.push_back(lemma);
       }
     }
   }
@@ -236,13 +238,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
         TNode arg1 = *i;
         TNode arg2 = *j;
         TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1);
-        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); 
+        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2);
 
         Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
         Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
         Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
         Debug("bv-ackermanize") << "  " << lemma << "\n";
-        assertions.push_back(lemma); 
+        assertions.push_back(lemma);
       }
     }
   }
@@ -265,7 +267,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 
     if (options::bitvectorDivByZeroConst()) {
       Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
-      return nm->mkNode(kind, node[0], node[1]); 
+      return nm->mkNode(kind, node[0], node[1]);
     }
 
     TNode num = node[0], den = node[1];
@@ -275,9 +277,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
       // Ackermanize UF if using eager bit-blasting
-      Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); 
+      Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
       node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
-      return node; 
+      return node;
     } else {
       Node divByZero = getBVDivByZero(node.getKind(), width);
       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
@@ -300,7 +302,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
- 
+
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     // the aig bit-blaster option is set heuristically
     // if bv abstraction is not used
@@ -309,13 +311,13 @@ void TheoryBV::preRegisterTerm(TNode node) {
     }
 
     if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) {
-      Node formula = node[0]; 
+      Node formula = node[0];
       d_eagerSolver->assertFormula(formula);
     }
     // nothing to do for the other terms
-    return; 
+    return;
   }
-  
+
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     d_subtheories[i]->preRegister(node);
   }
@@ -370,7 +372,7 @@ void TheoryBV::check(Effort e)
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
   // we may be getting new assertions so the model cache may not be sound
-  d_invalidateModelCache.set(true); 
+  d_invalidateModelCache.set(true);
   // if we are using the eager solver
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     // this can only happen on an empty benchmark
@@ -380,28 +382,28 @@ void TheoryBV::check(Effort e)
     if (!Theory::fullEffort(e))
       return;
 
-    std::vector<TNode> assertions; 
+    std::vector<TNode> assertions;
     while (!done()) {
       TNode fact = get().assertion;
       Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
-      assertions.push_back(fact); 
+      assertions.push_back(fact);
     }
-    Assert (d_eagerSolver->hasAssertions(assertions)); 
-    
+    Assert (d_eagerSolver->hasAssertions(assertions));
+
     bool ok = d_eagerSolver->checkSat();
     if (!ok) {
       if (assertions.size() == 1) {
         d_out->conflict(assertions[0]);
-        return; 
+        return;
       }
       Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions);
       d_out->conflict(conflict);
-      return; 
+      return;
     }
     return;
   }
-  
-  
+
+
   if (Theory::fullEffort(e)) {
     ++(d_statistics.d_numCallsToCheckFullEffort);
   } else {
@@ -446,7 +448,7 @@ void TheoryBV::check(Effort e)
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver->collectModelInfo(m, fullModel); 
+    d_eagerSolver->collectModelInfo(m, fullModel);
   }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
@@ -469,7 +471,7 @@ Node TheoryBV::getModelValue(TNode var) {
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    return; 
+    return;
   }
 
   if (inConflict()) {
@@ -508,29 +510,29 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      Node node = Rewriter::rewrite(in); 
+      Node node = Rewriter::rewrite(in);
       if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) ||
           (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) {
         Node extract = node[0].isConst() ? node[1] : node[0];
         if (extract[0].getKind() == kind::VARIABLE) {
           Node c = node[0].isConst() ? node[0] : node[1];
-        
+
           unsigned high = utils::getExtractHigh(extract);
           unsigned low = utils::getExtractLow(extract);
           unsigned var_bitwidth = utils::getSize(extract[0]);
           std::vector<Node> children;
-        
+
           if (low == 0) {
             Assert (high != var_bitwidth - 1);
             unsigned skolem_size = var_bitwidth - high - 1;
             Node skolem = utils::mkVar(skolem_size);
-            children.push_back(skolem); 
+            children.push_back(skolem);
             children.push_back(c);
           } else if (high == var_bitwidth - 1) {
             unsigned skolem_size = low;
             Node skolem = utils::mkVar(skolem_size);
             children.push_back(c);
-            children.push_back(skolem); 
+            children.push_back(skolem);
           } else {
             unsigned skolem1_size = low;
             unsigned skolem2_size = var_bitwidth - high - 1;
@@ -541,7 +543,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
             children.push_back(skolem1);
           }
           Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children);
-          Assert (utils::getSize(concat) == utils::getSize(extract[0])); 
+          Assert (utils::getSize(concat) == utils::getSize(extract[0]));
           outSubstitutions.addSubstitution(extract[0], concat);
           return PP_ASSERT_STATUS_SOLVED;
         }
@@ -552,7 +554,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   case kind::BITVECTOR_SLT:
   case kind::BITVECTOR_ULE:
   case kind::BITVECTOR_SLE:
-    
+
   default:
     // TODO other predicates
     break;
@@ -562,7 +564,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 Node TheoryBV::ppRewrite(TNode t)
 {
-  Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; 
+  Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
   Node res = t;
   if (RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
@@ -591,8 +593,8 @@ Node TheoryBV::ppRewrite(TNode t)
     } else {
       res = t;
     }
-  } 
-  
+  }
+
 
   // if(t.getKind() == kind::EQUAL &&
   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
@@ -618,18 +620,18 @@ Node TheoryBV::ppRewrite(TNode t)
   //         return new_eq;
   //       }
   //     }
-      
+
   //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
   //       ++(d_statistics.d_numMultSlice);
   //       return new_eq;
   //     }
   //   }
   // }
-  
+
   if (options::bvAbstraction() && t.getType().isBoolean()) {
-    d_abstractionModule->addInputAtom(res); 
+    d_abstractionModule->addInputAtom(res);
   }
-  Debug("bv-pp-rewrite") << "to   " << res << "\n"; 
+  Debug("bv-pp-rewrite") << "to   " << res << "\n";
   return res;
 }
 
@@ -637,13 +639,13 @@ void TheoryBV::presolve() {
   Debug("bitvector") << "TheoryBV::presolve" << endl;
 }
 
-static int prop_count = 0; 
+static int prop_count = 0;
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
   Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
-  prop_count++; 
-  
+  prop_count++;
+
   // If already in conflict, no more propagation
   if (d_conflict) {
     Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
@@ -720,7 +722,7 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); 
+  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
@@ -736,7 +738,7 @@ void TheoryBV::enableCoreTheorySlicer() {
   d_isCoreTheory = true;
   if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
     CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    core->enableSlicer(); 
+    core->enableSlicer();
   }
 }
 
@@ -746,7 +748,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
     return;
   }
   d_staticLearnCache.insert(in);
-    
+
   if (in.getKind() == kind::EQUAL) {
     if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
        (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
@@ -754,7 +756,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
 
       if(p.getNumChildren() == 2
-         && p[0].getKind()  == kind::BITVECTOR_SHL 
+         && p[0].getKind()  == kind::BITVECTOR_SHL
          && p[1].getKind()  == kind::BITVECTOR_SHL ){
         unsigned size = utils::getSize(s);
         Node one = utils::mkConst(size, 1u);
@@ -796,14 +798,18 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
 void TheoryBV::setConflict(Node conflict) {
   if (options::bvAbstraction()) {
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
-      
+
     std::vector<Node> lemmas;
-    lemmas.push_back(new_conflict); 
+    lemmas.push_back(new_conflict);
     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
     for (unsigned i = 0; i < lemmas.size(); ++i) {
-      lemma(utils::mkNode(kind::NOT, lemmas[i])); 
+      lemma(utils::mkNode(kind::NOT, lemmas[i]));
     }
   }
   d_conflict = true;
   d_conflictNode = conflict;
 }
+
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4b3649a86..8ded63c28 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/statistics_registry.h"
+#include "smt/smt_globals.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
@@ -35,10 +36,10 @@ namespace bv {
 class CoreSolver;
 class InequalitySolver;
 class AlgebraicSolver;
-class BitblastSolver; 
+class BitblastSolver;
 
 class EagerBitblastSolver;
-  
+
 class AbstractionModule;
 
 class TheoryBV : public Theory {
@@ -49,14 +50,14 @@ class TheoryBV : public Theory {
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-  
-  std::vector<SubtheorySolver*> d_subtheories;
-  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
 
+  std::vector<SubtheorySolver*> d_subtheories;
+  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+
   ~TheoryBV();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
@@ -80,13 +81,14 @@ public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
   void enableCoreTheorySlicer();
-  
+
   Node ppRewrite(TNode t);
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
-  
+
   void presolve();
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
 private:
 
   class Statistics {
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 3d70e9a9a..9ba20fcc9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -31,32 +31,34 @@
 #include "theory/type_enumerator.h"
 #include "theory/valuation.h"
 
-
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;
-
-
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
-  //d_cycle_check(c),
-  d_hasSeenCycle(c, false),
-  d_infer(c),
-  d_infer_exp(c),
-  d_notify( *this ),
-  d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
-  d_labels( c ),
-  d_selector_apps( c ),
-  //d_consEqc( c ),
-  d_conflict( c, false ),
-  d_collectTermsCache( c ),
-  d_consTerms( c ),
-  d_selTerms( c ),
-  d_singleton_eq( u ){
 
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
+                                 Valuation valuation,
+                                 const LogicInfo& logicInfo,
+                                 SmtGlobals* globals)
+    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, globals),
+      //d_cycle_check(c),
+      d_hasSeenCycle(c, false),
+      d_infer(c),
+      d_infer_exp(c),
+      d_notify( *this ),
+      d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
+      d_labels( c ),
+      d_selector_apps( c ),
+      //d_consEqc( c ),
+      d_conflict( c, false ),
+      d_collectTermsCache( c ),
+      d_consTerms( c ),
+      d_selTerms( c ),
+      d_singleton_eq( u )
+{
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
@@ -2044,3 +2046,7 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
   }
   return false;
 }
+
+} /* namepsace CVC4::theory::datatypes */
+} /* namepsace CVC4::theory */
+} /* namepsace CVC4 */
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index bbbf799bd..fc6e435cc 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -180,31 +180,40 @@ private:
   /** sygus utilities */
   SygusSplit * d_sygus_split;
   SygusSymBreak * d_sygus_sym_break;
+
 private:
   /** singleton lemmas (for degenerate co-datatype case) */
   std::map< TypeNode, Node > d_singleton_lemma[2];
+
   /** Cache for singleton equalities processed */
   BoolMap d_singleton_eq;
-private:
+
   /** assert fact */
   void assertFact( Node fact, Node exp );
+
   /** flush pending facts */
   void flushPendingFacts();
+
   /** do pending merged */
   void doPendingMerges();
+
   /** get or make eqc info */
   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
+
   /** has eqc info */
   bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); }
+
   /** get eqc constructor */
   TNode getEqcConstructor( TNode r );
+
 protected:
   /** compute care graph */
   void computeCareGraph();
+
 public:
   TheoryDatatypes(context::Context* c, context::UserContext* u,
                   OutputChannel& out, Valuation valuation,
-                  const LogicInfo& logicInfo);
+                  const LogicInfo& logicInfo, SmtGlobals* globals);
   ~TheoryDatatypes();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 6400fec38..9a8d77844 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -51,13 +51,11 @@ namespace removeToFPGeneric {
 
 
 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context* c,
-                           context::UserContext* u,
-                           OutputChannel& out,
-                           Valuation valuation,
-                           const LogicInfo& logicInfo) :
-  Theory(THEORY_FP, c, u, out, valuation, logicInfo) {
-}/* TheoryFp::TheoryFp() */
+TheoryFp::TheoryFp(context::Context* c, context::UserContext* u,
+                   OutputChannel& out, Valuation valuation,
+                   const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_FP, c, u, out, valuation, logicInfo, globals)
+{}/* TheoryFp::TheoryFp() */
 
 
 Node TheoryFp::expandDefinition(LogicRequest &, Node node) {
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 6fb41685f..fe3c377af 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -14,10 +14,11 @@ public:
 
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
   TheoryFp(context::Context* c,
-               context::UserContext* u,
-               OutputChannel& out,
-               Valuation valuation,
-               const LogicInfo& logicInfo);
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
+           SmtGlobals* globals);
 
   Node expandDefinition(LogicRequest &, Node node);
 
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 427ac577c..8cba51c8f 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -26,15 +26,16 @@
 
 using namespace std;
 
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-                     Valuation valuation, const LogicInfo& logicInfo)
-: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-, d_model(c)
-, d_assertionsDB(c)
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
+                     OutputChannel& out, Valuation valuation,
+                     const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+    , d_model(c)
+    , d_assertionsDB(c)
 {}
 
 Node TheoryIdl::ppRewrite(TNode atom) {
@@ -148,3 +149,7 @@ bool TheoryIdl::processAssertion(const IDLAssertion& assertion) {
   // Everything fine, no conflict
   return true;
 }
+
+} /* namepsace CVC4::theory::idl */
+} /* namepsace CVC4::theory */
+} /* namepsace CVC4 */
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 7c879e722..aa7267eb7 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -45,7 +45,8 @@ public:
 
   /** Theory constructor. */
   TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-            Valuation valuation, const LogicInfo& logicInfo);
+            Valuation valuation, const LogicInfo& logicInfo,
+            SmtGlobals* globals);
 
   /** Pre-processing of input atoms */
   Node ppRewrite(TNode atom);
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 60d0e1d48..2113ea66e 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -86,8 +86,9 @@ public:
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
-  virtual void safePoint(uint64_t ammount) throw(Interrupted, UnsafeInterruptException, AssertionException) {
-  }
+  virtual void safePoint(uint64_t amount)
+      throw(Interrupted, UnsafeInterruptException, AssertionException)
+  {}
 
   /**
    * Indicate a theory conflict has arisen.
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e9ff60137..b808f4cd5 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,8 +34,8 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
+    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 98f486145..f24c10fc0 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -46,10 +46,14 @@ private:
   int d_baseDecLevel;
 
   eq::EqualityEngine* d_masterEqualityEngine;
+
 private:
-  void computeCareGraph();  
+  void computeCareGraph();
+
 public:
-  TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryQuantifiers(context::Context* c, context::UserContext* u,
+                    OutputChannel& out, Valuation valuation,
+                    const LogicInfo& logicInfo, SmtGlobals* globals);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index db93c597c..82ebb5bf8 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -25,10 +25,11 @@ TheorySets::TheorySets(context::Context* c,
                        context::UserContext* u,
                        OutputChannel& out,
                        Valuation valuation,
-                       const LogicInfo& logicInfo) :
-  Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
-  d_internal(new TheorySetsPrivate(*this, c, u)) {
-}
+                       const LogicInfo& logicInfo,
+                       SmtGlobals* globals)
+    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, globals),
+      d_internal(new TheorySetsPrivate(*this, c, u))
+{}
 
 TheorySets::~TheorySets() {
   delete d_internal;
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 6136fc8f8..7ff8abec6 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -40,11 +40,9 @@ public:
    * Constructs a new instance of TheorySets w.r.t. the provided
    * contexts.
    */
-  TheorySets(context::Context* c,
-               context::UserContext* u,
-               OutputChannel& out,
-               Valuation valuation,
-               const LogicInfo& logicInfo);
+  TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out,
+             Valuation valuation, const LogicInfo& logicInfo,
+             SmtGlobals* globals);
 
   ~TheorySets();
 
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f200397bc..0c3171065 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -19,12 +19,12 @@
 #include <boost/foreach.hpp>
 
 #include "expr/emptyset.h"
-#include "expr/result.h"
 #include "options/sets_options.h"
 #include "theory/sets/expr_patterns.h" // ONLY included here
 #include "theory/sets/scrutinize.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/theory_model.h"
+#include "util/result.h"
 
 using namespace std;
 using namespace CVC4::expr::pattern;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index dfd3c4803..b68687d54 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -55,42 +55,44 @@ Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, No
 }
 
 
-TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-  RMAXINT(LONG_MAX),
-  d_notify( *this ),
-  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
-  d_conflict(c, false),
-  d_infer(c),
-  d_infer_exp(c),
-  d_nf_pairs(c),
-  d_loop_antec(u),
-  d_length_intro_vars(u),
-  d_pregistered_terms_cache(u),
-  d_registered_terms_cache(u),
-  d_preproc(u),
-  d_preproc_cache(u),
-  d_extf_infer_cache(c),
-  d_congruent(c),
-  d_proxy_var(u),
-  d_proxy_var_to_length(u),
-  d_neg_ctn_eqlen(c),
-  d_neg_ctn_ulen(c),
-  d_neg_ctn_cached(u),
-  d_ext_func_terms(c),
-  d_regexp_memberships(c),
-  d_regexp_ucached(u),
-  d_regexp_ccached(c),
-  d_pos_memberships(c),
-  d_neg_memberships(c),
-  d_inter_cache(c),
-  d_inter_index(c),
-  d_processed_memberships(c),
-  d_regexp_ant(c),
-  d_input_vars(u),
-  d_input_var_lsum(u),
-  d_cardinality_lits(u),
-  d_curr_cardinality(c, 0)
+TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
+                             OutputChannel& out, Valuation valuation,
+                             const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, globals),
+      RMAXINT(LONG_MAX),
+      d_notify( *this ),
+      d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
+      d_conflict(c, false),
+      d_infer(c),
+      d_infer_exp(c),
+      d_nf_pairs(c),
+      d_loop_antec(u),
+      d_length_intro_vars(u),
+      d_pregistered_terms_cache(u),
+      d_registered_terms_cache(u),
+      d_preproc(u),
+      d_preproc_cache(u),
+      d_extf_infer_cache(c),
+      d_congruent(c),
+      d_proxy_var(u),
+      d_proxy_var_to_length(u),
+      d_neg_ctn_eqlen(c),
+      d_neg_ctn_ulen(c),
+      d_neg_ctn_cached(u),
+      d_ext_func_terms(c),
+      d_regexp_memberships(c),
+      d_regexp_ucached(u),
+      d_regexp_ccached(c),
+      d_pos_memberships(c),
+      d_neg_memberships(c),
+      d_inter_cache(c),
+      d_inter_index(c),
+      d_processed_memberships(c),
+      d_regexp_ant(c),
+      d_input_vars(u),
+      d_input_var_lsum(u),
+      d_cardinality_lits(u),
+      d_curr_cardinality(c, 0)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 40358649b..ddb800ee1 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -52,7 +52,9 @@ class TheoryStrings : public Theory {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
 public:
-  TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryStrings(context::Context* c, context::UserContext* u,
+                OutputChannel& out, Valuation valuation,
+                const LogicInfo& logicInfo, SmtGlobals* globals);
   ~TheoryStrings();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5f4c80cf2..d17d97f97 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -34,6 +34,7 @@
 #include "options/theory_options.h"
 #include "options/theoryof_mode.h"
 #include "smt/logic_request.h"
+#include "smt/smt_globals.h"
 #include "smt_util/command.h"
 #include "smt_util/dump.h"
 #include "theory/logic_info.h"
@@ -245,7 +246,8 @@ protected:
    * Construct a Theory.
    */
   Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
-         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw()
+         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
+         SmtGlobals* globals) throw()
   : d_id(id)
   , d_satContext(satContext)
   , d_userContext(userContext)
@@ -261,6 +263,7 @@ protected:
   , d_out(&out)
   , d_valuation(valuation)
   , d_proofEnabled(false)
+  , d_globals(globals)
   {
     StatisticsRegistry::registerStat(&d_checkTime);
     StatisticsRegistry::registerStat(&d_computeCareGraphTime);
@@ -313,6 +316,8 @@ protected:
    */
   bool d_proofEnabled;
 
+  SmtGlobals* d_globals;
+
 public:
 
   /**
@@ -870,6 +875,10 @@ public:
    */
   virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
 
+
+  /** Returns a pointer to the globals copy the theory is using. */
+  SmtGlobals* globals() { return d_globals; }
+
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 52922e2ca..a55b3a1c9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -104,7 +104,8 @@ void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveITE& iteRemover,
-                           const LogicInfo& logicInfo)
+                           const LogicInfo& logicInfo,
+                           SmtGlobals* globals)
 : d_propEngine(NULL),
   d_decisionEngine(NULL),
   d_context(context),
@@ -133,6 +134,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_false(),
   d_interrupted(false),
   d_resourceManager(NodeManager::currentResourceManager()),
+  d_globals(globals),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
@@ -1390,8 +1392,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
   }
 
   // Share with other portfolio threads
-  if(options::lemmaOutputChannel() != NULL) {
-    options::lemmaOutputChannel()->notifyNewLemma(node.toExpr());
+  if(d_globals->getLemmaOutputChannel() != NULL) {
+    d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
   // Run theory preprocessing, maybe
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2185f22ff..adc4daeee 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -30,6 +30,7 @@
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
+#include "smt/smt_globals.h"
 #include "smt_util/command.h"
 #include "theory/atom_requests.h"
 #include "theory/bv/bv_to_bool.h"
@@ -206,6 +207,7 @@ class TheoryEngine {
    */
   context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 
+
   /**
    * Statistics for a particular theory.
    */
@@ -476,10 +478,14 @@ class TheoryEngine {
   bool d_interrupted;
   ResourceManager* d_resourceManager;
 
+  /** Container for misc. globals. */
+  SmtGlobals* d_globals;
+
 public:
 
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic);
+  TheoryEngine(context::Context* context, context::UserContext* userContext,
+               RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -498,7 +504,9 @@ public:
   inline void addTheory(theory::TheoryId theoryId) {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
-    d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo);
+    d_theoryTable[theoryId] =
+        new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId],
+                        theory::Valuation(this), d_logicInfo, d_globals);
   }
 
   inline void setPropEngine(prop::PropEngine* propEngine) {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 31bee316a..e21b7ef7d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -30,18 +30,20 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_UF, c, u, out, valuation, logicInfo),
-  d_notify(*this),
-  /* The strong theory solver can be notified by EqualityEngine::init(),
-   * so make sure it's initialized first. */
-  d_thss(NULL),
-  d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
-  d_conflict(c, false),
-  d_literalsToPropagate(c),
-  d_literalsToPropagateIndex(c, 0),
-  d_functionsTerms(c),
-  d_symb(u)
+TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
+                   OutputChannel& out, Valuation valuation,
+                   const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals),
+      d_notify(*this),
+      /* The strong theory solver can be notified by EqualityEngine::init(),
+       * so make sure it's initialized first. */
+      d_thss(NULL),
+      d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
+      d_conflict(c, false),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_functionsTerms(c),
+      d_symb(u)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 82597e286..aff78f53d 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -161,7 +161,9 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
+           Valuation valuation, const LogicInfo& logicInfo,
+           SmtGlobals* globals);
 
   ~TheoryUF();