Merge remote-tracking branch 'origin/master' into segfaultfix

49 files changed, 425 insertions, 357 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 3bff9fc95..c414ac749 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -1,19 +1,17 @@
 /*********************                                                        */
 /*! \file abstraction.cpp
-** \verbatim
-** Original author: Liana Hadarean
-** Major contributors: none.
-** Minor contributors (to current version): none.
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief [[ Add one-line brief description here ]]
-**
-** [[ Add lengthier description here ]]
-** \todo document this file
-**/
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "theory/bv/abstraction.h"
 #include "theory/bv/theory_bv_utils.h"
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index cd4c443a7..2e86c834d 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -1,11 +1,11 @@
- /*********************                                                        */
+/*********************                                                        */
 /*! \file abstraction.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: none.
- ** Minor contributors (to current version): none.
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/aig_bitblaster.h b/src/theory/bv/aig_bitblaster.cpp
index d1635f950..ce775874f 100644
--- a/src/theory/bv/aig_bitblaster.h
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file aig_bitblaster.h
+/*! \file aig_bitblaster.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): lianah
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -15,11 +15,6 @@
  **/
 
 #include "cvc4_private.h"
-
-#ifndef __CVC4__AIG__BITBLASTER_H
-#define __CVC4__AIG__BITBLASTER_H
-
-
 #include "bitblaster_template.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
@@ -112,6 +107,14 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); 
 }
 
+} /* CVC4::theory::bv */
+} /* CVC4::theory */
+} /* CVC4 */
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
 
 Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
 
@@ -467,13 +470,6 @@ AigBitblaster::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_solveTime); 
 }
 
-
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-
 #else // CVC4_USE_ABC
 
 namespace CVC4 {
@@ -547,6 +543,13 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return NULL;
 }
 
+} /* CVC4::theory::bv */
+} /* CVC4::theory */
+} /* CVC4 */
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
 
 Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
 
@@ -647,12 +650,4 @@ AigBitblaster::Statistics::~Statistics() {}
 AigBitblaster::AigBitblaster() {
   Unreachable();
 }
-
-} // namespace bv
-} // namespace theory
-} // namespace CVC4
-
-
 #endif // CVC4_USE_ABC
-
-#endif // __CVC4__AIG__BITBLASTER_H
diff --git a/src/theory/bv/bitblast_mode.cpp b/src/theory/bv/bitblast_mode.cpp
index 91a140539..51c0290af 100644
--- a/src/theory/bv/bitblast_mode.cpp
+++ b/src/theory/bv/bitblast_mode.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bitblast_mode.h b/src/theory/bv/bitblast_mode.h
index 318e17467..89ecdc381 100644
--- a/src/theory/bv/bitblast_mode.h
+++ b/src/theory/bv/bitblast_mode.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index fba744d69..62c92c0a8 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bitblast_strategies.h
+/*! \file bitblast_strategies_template.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h
index 91cc2d640..a236c69e8 100644
--- a/src/theory/bv/bitblast_utils.h
+++ b/src/theory/bv/bitblast_utils.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): none.
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 25de81f2c..ecd7013c7 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bitblaster.h
+/*! \file bitblaster_template.h
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): lianah, Morgan Deters, Dejan Jovanovic
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -27,6 +27,7 @@
 #include "bitblast_strategies_template.h"
 #include "prop/sat_solver.h"
 #include "theory/valuation.h"
+#include "theory/theory_registrar.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -57,6 +58,8 @@ namespace bv {
 class BitblastingRegistrar;
 
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
 class AbstractionModule;
 
 /**
@@ -70,7 +73,7 @@ class TBitblaster {
 protected:
   typedef std::vector<T> Bits;
   typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction>  TermDefMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       AtomSet;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       TNodeSet;
 
   typedef void  (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
   typedef T     (*AtomBBStrategy) (TNode, TBitblaster<T>*);
@@ -104,8 +107,6 @@ class TheoryBV;
 
 class TLazyBitblaster :  public TBitblaster<Node> {
   typedef std::vector<Node> Bits;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet;
   typedef context::CDList<prop::SatLiteral> AssertionList;
   typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap;
   
@@ -134,12 +135,12 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   prop::BVSatSolverInterface*        d_satSolver;
   prop::CnfStream*                   d_cnfStream;
 
-  AssertionList d_assertedAtoms; /**< context dependent list storing the atoms
+  AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms
                                      currently asserted by the DPLL SAT solver. */
-  ExplanationMap d_explanations; /**< context dependent list of explanations for the propagated literals.
+  ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
                                     Only used when bvEagerPropagate option enabled. */
-  VarSet d_variables;
-  AtomSet d_bbAtoms; 
+  TNodeSet d_variables;
+  TNodeSet d_bbAtoms; 
   AbstractionModule* d_abstraction;
   bool d_emptyNotify;
   
@@ -188,7 +189,7 @@ public:
    */
   void collectModelInfo(TheoryModel* m, bool fullModel);
 
-  typedef VarSet::const_iterator vars_iterator;
+  typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
   vars_iterator endVars() { return d_variables.end(); }
 
@@ -239,7 +240,14 @@ class EagerBitblaster : public TBitblaster<Node> {
   BitblastingRegistrar*              d_bitblastingRegistrar;
   context::Context*                  d_nullContext;
   prop::CnfStream*                   d_cnfStream;
-  TNodeSet d_bbAtoms; 
+
+  theory::bv::TheoryBV* d_bv;
+  TNodeSet d_bbAtoms;
+  TNodeSet d_variables;
+
+  Node getVarValue(TNode a, bool fullModel);
+  bool isSharedTerm(TNode node); 
+
 public:
   void addAtom(TNode atom);
   void makeVariable(TNode node, Bits& bits);
@@ -249,12 +257,22 @@ public:
   bool hasBBAtom(TNode atom) const; 
   void bbFormula(TNode formula);
   void storeBBAtom(TNode atom, Node atom_bb);
-  EagerBitblaster(); 
+  EagerBitblaster(theory::bv::TheoryBV* theory_bv); 
   ~EagerBitblaster();
   bool assertToSat(TNode node, bool propagate = true);
-  bool solve(); 
+  bool solve();
+  void collectModelInfo(TheoryModel* m, bool fullModel);
 };
 
+class BitblastingRegistrar: public prop::Registrar {
+  EagerBitblaster* d_bitblaster; 
+public:
+  BitblastingRegistrar(EagerBitblaster* bb)
+    : d_bitblaster(bb)
+  {}
+  void preRegister(Node n);
+}; /* class Registrar */
+
 class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
   typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
   typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index af35c0499..f9f8ff581 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bv_eager_solver.h
+/*! \file bv_eager_solver.cpp
  ** \verbatim
- ** Original author: Liana Hadarean 
+ ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -16,19 +16,19 @@
 
 #include "theory/bv/bv_eager_solver.h"
 #include "theory/bv/bitblaster_template.h"
-#include "theory/bv/eager_bitblaster.h"
-#include "theory/bv/aig_bitblaster.h"
+#include "theory/bv/options.h"
 
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
-EagerBitblastSolver::EagerBitblastSolver()
+EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv)
   : d_assertionSet()
   , d_bitblaster(NULL)
   , d_aigBitblaster(NULL)
   , d_useAig(options::bitvectorAig())
+  , d_bv(bv)
 {}
 
 EagerBitblastSolver::~EagerBitblastSolver() {
@@ -53,7 +53,7 @@ void EagerBitblastSolver::initialize() {
   if (d_useAig) {
     d_aigBitblaster = new AigBitblaster();
   } else {
-    d_bitblaster = new EagerBitblaster();
+    d_bitblaster = new EagerBitblaster(d_bv);
   }
 }
 
@@ -106,3 +106,8 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode> &formulas) {
   }
   return true; 
 }
+
+void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  AlwaysAssert(!d_useAig && d_bitblaster);
+  d_bitblaster->collectModelInfo(m, fullModel); 
+}
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 1fb65c9c8..37e1bd9ba 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file bv_eager_solver.h
  ** \verbatim
- ** Original author: Liana Hadarean 
+ ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -16,6 +16,8 @@
 
 #include "cvc4_private.h"
 #include "expr/node.h"
+#include "theory/theory_model.h"
+#include "theory/bv/theory_bv.h"
 #include <vector>
 #pragma once
 
@@ -37,8 +39,9 @@ class EagerBitblastSolver {
   EagerBitblaster* d_bitblaster;
   AigBitblaster* d_aigBitblaster;
   bool d_useAig;
+  TheoryBV* d_bv; 
 public:
-  EagerBitblastSolver(); 
+  EagerBitblastSolver(theory::bv::TheoryBV* bv); 
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
@@ -48,6 +51,7 @@ public:
   void turnOffAig();
   bool isInitialized();
   void initialize();
+  void collectModelInfo(theory::TheoryModel* m, bool fullModel);
 };
 
 }
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index ff344d307..aa605de04 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 9a898ebe6..3c67f506f 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -39,9 +39,6 @@ extern const ReasonId AxiomReasonId;
 
 class InequalityGraph : public context::ContextNotifyObj{
 
-
-  context::Context* d_context;
-
   struct InequalityEdge {
     TermId next;
     ReasonId reason;
@@ -126,7 +123,6 @@ class InequalityGraph : public context::ContextNotifyObj{
 
   context::CDO<bool> d_inConflict;
   std::vector<TNode> d_conflict;
-  bool d_signed; 
 
   ModelValues  d_modelValues;
   void initializeModelValue(TNode node); 
@@ -214,12 +210,10 @@ public:
   
   InequalityGraph(context::Context* c, bool s = false)
     : ContextNotifyObj(c), 
-      d_context(c),
       d_ineqNodes(),
       d_ineqEdges(),
       d_inConflict(c, false),
       d_conflict(),
-      d_signed(s),
       d_modelValues(c),
       d_disequalities(c),
       d_disequalitiesAlreadySplit(),
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 1adbb83d9..5f35f95e3 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file bv_quick_check.cpp
  ** \verbatim
- ** Original author: Liana Hadaren
+ ** Original author: Liana Hadarean
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index c09994c06..6c32fbb4d 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -26,6 +26,7 @@
 #include "context/cdo.h"
 #include "prop/sat_solver_types.h"
 #include "util/statistics_registry.h"
+#include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -34,11 +35,6 @@ class TheoryModel;
 
 namespace bv {
 
-
-
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-
 class TLazyBitblaster; 
 class TheoryBV;
 
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 8d21734db..9a314fd6a 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -5,7 +5,7 @@
  ** Major contributors: Andrew Reynolds, Dejan Jovanovic
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 9dd86b5ea..4c784ce6f 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -1,18 +1,19 @@
 /*********************                                                        */
-/*! \file bv_subtheory_bitblast.cpp
-** \verbatim
-** Original author: Liana Hadarean 
-** Major contributors: none
-** Minor contributors (to current version): none
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief Algebraic solver.
-**
-** Algebraic solver.
-**/
+/*! \file bv_subtheory_algebraic.cpp
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
 #include "util/boolean_simplification.h"
 #include "theory/theory_model.h"
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index fbc8c3ff0..03588a78f 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -1,18 +1,18 @@
 /*********************                                                        */
 /*! \file bv_subtheory_algebraic.h
-** \verbatim
-** Original author: Liana Hadarean 
-** Major contributors: none
-** Minor contributors (to current version): none
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief Algebraic solver.
-**
-** Algebraic solver.
-**/
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
 
 #pragma once
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ebe017ee1..a2a6e19ac 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -2,10 +2,10 @@
 /*! \file bv_subtheory_bitblast.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Clark Barrett
- ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Kshitij Bansal
+ ** Major contributors: Clark Barrett, Liana Hadarean
+ ** Minor contributors (to current version): Morgan Deters, Kshitij Bansal, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -17,9 +17,10 @@
 #include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/lazy_bitblaster.h"
+#include "theory/bv/bitblaster_template.h"
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/options.h"
+#include "theory/bv/abstraction.h"
 #include "theory/decision_attributes.h"
 #include "decision/options.h"
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 511318521..414abdcce 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -2,10 +2,10 @@
 /*! \file bv_subtheory_bitblast.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Liana Hadarean, Clark Barrett
+ ** Major contributors: Liana Hadarean
+ ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 179f3a44d..d2c79fec2 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 9ab6cfce4..5b9c54095 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -5,7 +5,7 @@
  ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 4b894fe2a..4f9eb0823 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index ef03166e6..b9195c7d1 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index aef1437a0..06a1d4a44 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 28501ba96..b266b591b 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
index d7f5d6fde..5df170e21 100644
--- a/src/theory/bv/bvintropow2.cpp
+++ b/src/theory/bv/bvintropow2.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file bvintropow2.cpp
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "theory/bv/bvintropow2.h"
 #include "theory/rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h
index 3844d03e1..774645560 100644
--- a/src/theory/bv/bvintropow2.h
+++ b/src/theory/bv/bvintropow2.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file bvintropow2.h
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 
 
 #include "cvc4_private.h"
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index 01aeeab91..5ffe7032a 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.cpp
index da73c7f09..e8fee00f5 100644
--- a/src/theory/bv/eager_bitblaster.h
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -1,51 +1,42 @@
 /*********************                                                        */
-/*! \file eager_bitblaster.h
+/*! \file eager_bitblaster.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): lianah
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
  ** \brief 
  **
- ** Bitblaster for the lazy bv solver. 
+ ** Bitblaster for the eager bv solver. 
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__EAGER__BITBLASTER_H
-#define __CVC4__EAGER__BITBLASTER_H
-
-
-#include "bitblaster_template.h"
-#include "theory/theory_registrar.h"
+#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/options.h"
+#include "theory/theory_model.h"
+#include "theory/bv/theory_bv.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
-#include "theory/bv/options.h"
 
-namespace CVC4 {
-namespace theory {
-namespace bv {
 
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv; 
 
-class BitblastingRegistrar: public prop::Registrar {
-  EagerBitblaster* d_bitblaster; 
-public:
-  BitblastingRegistrar(EagerBitblaster* bb)
-    : d_bitblaster(bb)
-  {}
-  void preRegister(Node n) {
-    d_bitblaster->bbAtom(n); 
-  };
+void BitblastingRegistrar::preRegister(Node n) {
+  d_bitblaster->bbAtom(n); 
+};
 
-};/* class Registrar */
-
-EagerBitblaster::EagerBitblaster()
+EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   : TBitblaster<Node>()
+  , d_bv(theory_bv)
   , d_bbAtoms()
+  , d_variables()
 {
   d_bitblastingRegistrar = new BitblastingRegistrar(this); 
   d_nullContext = new context::Context();
@@ -126,6 +117,7 @@ void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
   for (unsigned i = 0; i < utils::getSize(var); ++i) {
     bits.push_back(utils::mkBitOf(var, i)); 
   }
+  d_variables.insert(var); 
 }
 
 Node EagerBitblaster::getBBAtom(TNode node) const {
@@ -154,10 +146,63 @@ bool EagerBitblaster::solve() {
 }
 
 
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
+/**
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
+ *
+ * @return
+ */
+Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
+  if (!hasBBTerm(a)) {
+    Assert(isSharedTerm(a));
+    return Node();
+  }
+  Bits bits;
+  getBBTerm(a, bits);
+  Integer value(0);
+  for (int i = bits.size() -1; i >= 0; --i) {
+    prop::SatValue bit_value;
+    if (d_cnfStream->hasLiteral(bits[i])) {
+      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+      bit_value = d_satSolver->value(bit);
+      Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+    } else {
+      // the bit is unconstrainted so we can give it an arbitrary value
+      bit_value = prop::SAT_VALUE_FALSE;
+    }
+    Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+    value = value * 2 + bit_int;
+  }
+  return utils::mkConst(BitVector(bits.size(), value));
+}
 
 
+void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+  TNodeSet::const_iterator it = d_variables.begin();
+  for (; it!= d_variables.end(); ++it) {
+    TNode var = *it;
+    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
+      Node const_value = getVarValue(var, fullModel);
+      if(const_value == Node()) {
+        if( fullModel ){
+          // if the value is unassigned just set it to zero
+          const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
+        }
+      }
+      if(const_value != Node()) {
+        Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+                                 << var << " "
+                                 << const_value << "))\n";
+        m->assertEquality(var, const_value, true);
+      }
+    }
+  }
+}
 
-#endif
+bool EagerBitblaster::isSharedTerm(TNode node) {
+  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
+}
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 4b2bba741..b4ecc1d3d 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -25,7 +25,7 @@ constant CONST_BITVECTOR \
     ::CVC4::BitVector \
     ::CVC4::BitVectorHashFunction \
     "util/bitvector.h" \
-    "a fixed-width bit-vector constant"
+    "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class"
 
 enumerator BITVECTOR_TYPE \
     "::CVC4::theory::bv::BitVectorEnumerator" \
@@ -36,101 +36,101 @@ well-founded BITVECTOR_TYPE \
     "(*CVC4::theory::TypeEnumerator(%TYPE%))" \
     "theory/type_enumerator.h"
 
-operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
-operator BITVECTOR_AND 2: "bitwise and"
-operator BITVECTOR_OR 2: "bitwise or"
-operator BITVECTOR_XOR 2: "bitwise xor"
-operator BITVECTOR_NOT 1 "bitwise not"
-operator BITVECTOR_NAND 2 "bitwise nand"
-operator BITVECTOR_NOR 2 "bitwise nor"
-operator BITVECTOR_XNOR 2 "bitwise xnor"
-operator BITVECTOR_COMP 2 "equality comparison (returns one bit)"
-operator BITVECTOR_MULT 2: "bit-vector multiplication"
-operator BITVECTOR_PLUS 2: "bit-vector addition"
-operator BITVECTOR_SUB 2 "bit-vector subtraction"
-operator BITVECTOR_NEG 1 "bit-vector unary negation"
-operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"
-operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"
-operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division"
-operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)"
-operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)"
-# total division kinds 
-operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)"
-operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)"
-
-operator BITVECTOR_SHL 2 "bit-vector left shift"
-operator BITVECTOR_LSHR 2 "bit-vector logical shift right"
-operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right"
-operator BITVECTOR_ULT 2 "bit-vector unsigned less than"
-operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal"
-operator BITVECTOR_UGT 2 "bit-vector unsigned greater than"
-operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal"
-operator BITVECTOR_SLT 2 "bit-vector signed less than"
-operator BITVECTOR_SLE 2 "bit-vector signed less than or equal"
-operator BITVECTOR_SGT 2 "bit-vector signed greater than"
-operator BITVECTOR_SGE 2 "signed greater than or equal"
-
-operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting"
-operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvudiv"
-operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvurem"
+operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors"
+operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors"
+operator BITVECTOR_OR 2: "bitwise or of two or more bit-vectors"
+operator BITVECTOR_XOR 2: "bitwise xor of two or more bit-vectors"
+operator BITVECTOR_NOT 1 "bitwise not of a bit-vector"
+operator BITVECTOR_NAND 2 "bitwise nand of two bit-vectors"
+operator BITVECTOR_NOR 2 "bitwise nor of two bit-vectors"
+operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors"
+operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)"
+operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
+operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
+operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
+operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
+operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)"
+operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)"
+operator BITVECTOR_SDIV 2 "2's complement signed division"
+operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
+operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
+# total division kinds
+operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
+operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
+
+operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)"
+operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SLT 2 "bit-vector signed less than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
+
+operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
+operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
+operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
 
 constant BITVECTOR_BITOF_OP \
 	::CVC4::BitVectorBitOf \
 	::CVC4::BitVectorBitOfHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector boolean bit extract"
+	"operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class"
 
 constant BITVECTOR_EXTRACT_OP \
 	::CVC4::BitVectorExtract \
 	::CVC4::BitVectorExtractHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector extract"
+	"operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class"
 
 constant BITVECTOR_REPEAT_OP \
 	::CVC4::BitVectorRepeat \
 	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector repeat"
+	"operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class"
 
 constant BITVECTOR_ZERO_EXTEND_OP \
 	::CVC4::BitVectorZeroExtend \
 	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector zero-extend"
+	"operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class"
 
 constant BITVECTOR_SIGN_EXTEND_OP \
 	::CVC4::BitVectorSignExtend \
 	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector sign-extend"
+	"operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class"
 
 constant BITVECTOR_ROTATE_LEFT_OP \
 	::CVC4::BitVectorRotateLeft \
 	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate left"
+	"operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class"
 
 constant BITVECTOR_ROTATE_RIGHT_OP \
 	::CVC4::BitVectorRotateRight \
 	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate right"
+	"operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class"
 
-parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract"
-parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract"
-parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat"
-parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend"
-parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend"
-parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left"
-parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right"
+parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
+parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
+parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
+parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
+parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
+parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
+parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
 
 constant INT_TO_BITVECTOR_OP \
 	::CVC4::IntToBitVector \
 	"::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \
 	"util/bitvector.h" \
-	"operator for the integer conversion to bit-vector"
-parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector"
-operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer"
+	"operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class"
+parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
+operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector"
 
 typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
 
@@ -142,7 +142,7 @@ typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 
-typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule
+typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompTypeRule
 
 typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
@@ -178,7 +178,7 @@ typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanization
 typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
 typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
 typerule BITVECTOR_BITOF   ::CVC4::theory::bv::BitVectorBitOfTypeRule
-typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule
+typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
 typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.cpp
index 013e230f6..f721a22f0 100644
--- a/src/theory/bv/lazy_bitblaster.h
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -1,25 +1,20 @@
 /*********************                                                        */
-/*! \file lazy_bitblaster.h
-** \verbatim
-** Original author: Liana Hadarean
-** Major contributors: none
-** Minor contributors (to current version): lianah
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief 
-**
-** Bitblaster for the lazy bv solver. 
-**/
+/*! \file lazy_bitblaster.cpp
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Bitblaster for the lazy bv solver. 
+ **
+ ** Bitblaster for the lazy bv solver. 
+ **/
 
 #include "cvc4_private.h"
-
-#ifndef __CVC4__LAZY__BITBLASTER_H
-#define __CVC4__LAZY__BITBLASTER_H
-
-
 #include "bitblaster_template.h"
 #include "theory_bv_utils.h"
 #include "theory/rewriter.h"
@@ -31,16 +26,17 @@
 #include "theory/theory_model.h"
 #include "theory/bv/abstraction.h"
 
-namespace CVC4 {
-namespace theory {
-namespace bv {
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv; 
+
 
 TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
-  : TBitblaster()
+  : TBitblaster<Node>()
   , d_bv(bv)
   , d_ctx(c)
-  , d_assertedAtoms(c)
-  , d_explanations(c)
+  , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(c))
+  , d_explanations(new(true) ExplanationMap(c))
   , d_variables()
   , d_bbAtoms()
   , d_abstraction(NULL)
@@ -192,8 +188,8 @@ void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
 
   ++(d_statistics.d_numExplainedPropagations);
   if (options::bvEagerExplanations()) {
-    Assert (d_explanations.find(lit) != d_explanations.end());
-    const std::vector<prop::SatLiteral>& literal_explanation = d_explanations[lit].get();
+    Assert (d_explanations->find(lit) != d_explanations->end());
+    const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
     for (unsigned i = 0; i < literal_explanation.size(); ++i) {
       explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
     }
@@ -241,7 +237,7 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
 
   prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
-  d_assertedAtoms.push_back(markerLit);
+  d_assertedAtoms->push_back(markerLit);
 
   return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN;
 }
@@ -256,24 +252,24 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
 bool TLazyBitblaster::solve() {
   if (Trace.isOn("bitvector")) {
     Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms ";
-    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin();
-    for (; it != d_assertedAtoms.end(); ++it) {
+    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
+    for (; it != d_assertedAtoms->end(); ++it) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
+  Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
 prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
   if (Trace.isOn("bitvector")) {
     Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms ";
-    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin();
-    for (; it != d_assertedAtoms.end(); ++it) {
+    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
+    for (; it != d_assertedAtoms->end(); ++it) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms.size() <<"\n";
+  Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
   return d_satSolver->solve(budget);
 }
 
@@ -327,10 +323,10 @@ TLazyBitblaster::Statistics::~Statistics() {
 bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
   if(options::bvEagerExplanations()) {
     // compute explanation
-    if (d_lazyBB->d_explanations.find(lit) == d_lazyBB->d_explanations.end()) {
+    if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
       std::vector<prop::SatLiteral> literal_explanation;
       d_lazyBB->d_satSolver->explain(lit, literal_explanation);
-      d_lazyBB->d_explanations.insert(lit, literal_explanation);
+      d_lazyBB->d_explanations->insert(lit, literal_explanation);
     } else {
       // we propagated it at a lower level
       return true; 
@@ -453,7 +449,7 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
 }
 
 void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
+  TNodeSet::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
@@ -478,8 +474,10 @@ void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0); 
   delete d_satSolver;
   delete d_cnfStream;
-  d_assertedAtoms = context::CDList<prop::SatLiteral>(d_ctx);
-  d_explanations = ExplanationMap(d_ctx);
+  d_assertedAtoms->deleteSelf();
+  d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
+  d_explanations->deleteSelf();
+  d_explanations = new(true) ExplanationMap(d_ctx);
   d_bbAtoms.clear();
   d_variables.clear();
   d_termCache.clear(); 
@@ -495,9 +493,3 @@ void TLazyBitblaster::clearSolver() {
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
   d_satSolver->setNotify(notify);
 }
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-#endif
diff --git a/src/theory/bv/options b/src/theory/bv/options
index b5a4fea93..81d88421b 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -5,14 +5,14 @@
 
 module BV "theory/bv/options.h" Bitvector theory
 
-# Option to set the bit-blasting mode (lazy, eager, eager-aig)
+# Option to set the bit-blasting mode (lazy, eager)
 
 option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h"
  choose bitblasting mode, see --bitblast=help
 
 # Options for eager bit-blasting
  
-option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager
+option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager :link --bv-aig-simp="balance;drw"
  bitblast by first converting to AIG (only if --bitblast=eager)
 
 expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig
diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h
index 5d85a1be0..c917aa9dd 100644
--- a/src/theory/bv/options_handlers.h
+++ b/src/theory/bv/options_handlers.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -56,9 +56,6 @@ lazy (default)\n\
 \n\
 eager\n\
 + Bitblast eagerly to bv SAT solver\n\
-\n\
-aig\n\
-+ Bitblast eagerly to bv SAT solver by converting to AIG\n\
 ";
 
 inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
@@ -70,7 +67,8 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
       options::bitvectorEqualitySolver.set(true);
     }
     if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
-      if (options::incrementalSolving()) {
+      if (options::incrementalSolving() ||
+          options::produceModels()) {
         options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF);
       } else {
         options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO);
@@ -85,10 +83,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
     }
     return BITBLAST_MODE_LAZY;
   } else if(optarg == "eager") {
-    if (options::produceModels()) {
-      throw OptionException(std::string("Eager bit-blasting does not currently support model generation. \n\
-                                         Try --bitblast=lazy")); 
-    }
 
     if (options::incrementalSolving() &&
         options::incrementalSolving.wasSetByUser()) {
@@ -96,14 +90,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
                                          Try --bitblast=lazy"));
     }
     
-    if (!options::bitvectorAig.wasSetByUser()) {
-      options::bitvectorAig.set(true);
-      abcEnabledBuild("--bitblast-aig", true, NULL); 
-    }
-    if (!options::bitvectorAigSimplifications.wasSetByUser()) {
-      // due to a known bug in abc switching to using drw instead of rw
-      options::bitvectorAigSimplifications.set("balance;drw");
-    }
     if (!options::bitvectorToBool.wasSetByUser()) {
       options::bitvectorToBool.set(true);
     }
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index c37c8089d..a7587bedf 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 15c0b9c0b..7b55054bc 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d3da10a90..4abf25bb1 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -1,18 +1,16 @@
 /*********************                                                        */
 /*! \file theory_bv.cpp
-** \verbatim
-** Original author: Dejan Jovanovic
-** Major contributors: Morgan Deters, Liana Hadarean
-** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief [[ Add one-line brief description here ]]
-**
-** [[ Add lengthier description here ]]
-** \todo document this file
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: Liana Hadarean
+ ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds, Morgan Deters, Martin Brain <>
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
 **/
 
 #include "smt/options.h"
@@ -61,7 +59,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
 {
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver = new EagerBitblastSolver();
+    d_eagerSolver = new EagerBitblastSolver(this);
     return; 
   }
 
@@ -434,7 +432,9 @@ 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); 
+  }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
       d_subtheories[i]->collectModelInfo(m, fullModel);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 26ed8c296..22d9f6775 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic, Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds
+ ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds, Martin Brain <>
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -105,7 +105,7 @@ private:
 
 
   /**
-   * Return the uinterpreted function symbol corresponding to division-by-zero
+   * Return the uninterpreted function symbol corresponding to division-by-zero
    * for this particular bit-width
    * @param k should be UREM or UDIV
    * @param width
@@ -121,7 +121,7 @@ private:
   NodeSet d_staticLearnCache;
   
   /**
-   * Maps from bit-vector width to divison-by-zero uninterpreted
+   * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
    */
   __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
@@ -209,6 +209,7 @@ private:
  
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
+  friend class EagerBitblaster;
   friend class BitblastSolver;
   friend class EqualitySolver;
   friend class CoreSolver;
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 5e85cb145..bc9095f03 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -5,7 +5,7 @@
  ** Major contributors: Liana Hadarean
  ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index db774ebe3..1f8799682 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -5,7 +5,7 @@
  ** Major contributors: Clark Barrett
  ** Minor contributors (to current version): Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 43acfef75..676df5dde 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Tim King, Clark Barrett, Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 3e6e02952..21b59fa8c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -5,7 +5,7 @@
  ** Major contributors: Clark Barrett
  ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 6c0ba90d4..0442c47d9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Clark Barrett
  ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index c8705e121..3bf390ded 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -2,10 +2,10 @@
 /*! \file theory_bv_rewrite_rules_simplification.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic, Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic, Tim King, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 4a0da44cc..306a3bd97 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Liana Hadarean
  ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index def8e24fe..42bccb534 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Liana Hadarean
  ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index c1829ce69..81a2d9a27 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,16 +2,16 @@
 /*! \file theory_bv_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Christopher L. Conway, Morgan Deters
+ ** Major contributors: Christopher L. Conway, Liana Hadarean, Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Bitvector theory.
+ ** \brief Bitvector theory typing rules
  **
- ** Bitvector theory.
+ ** Bitvector theory typing rules.
  **/
 
 #include "cvc4_private.h"
@@ -36,18 +36,17 @@ public:
     }
     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
-};
-
+};/* class BitVectorConstantTypeRule */
 
 class BitVectorBitOfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate) {
-    
+
     if(check) {
       BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
       TypeNode t = n[0].getType(check);
-      
+
       if (!t.isBitVector()) {
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
@@ -55,12 +54,11 @@ public:
         throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size");
       }
     }
-    return nodeManager->booleanType(); 
+    return nodeManager->booleanType();
   }
-};
-
+};/* class BitVectorBitOfTypeRule */
 
-class BitVectorCompRule {
+class BitVectorCompTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
@@ -73,7 +71,7 @@ public:
     }
     return nodeManager->mkBitVectorType(1);
   }
-};
+};/* class BitVectorCompTypeRule */
 
 class BitVectorFixedWidthTypeRule {
 public:
@@ -94,7 +92,7 @@ public:
     }
     return t;
   }
-};
+};/* class BitVectorFixedWidthTypeRule */
 
 class BitVectorPredicateTypeRule {
 public:
@@ -112,7 +110,7 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class BitVectorPredicateTypeRule */
 
 class BitVectorEagerAtomTypeRule {
 public:
@@ -126,7 +124,7 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class BitVectorEagerAtomTypeRule */
 
 class BitVectorAckermanizationUdivTypeRule {
 public:
@@ -138,9 +136,9 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
     }
-    return lhsType; 
+    return lhsType;
   }
-};
+};/* class BitVectorAckermanizationUdivTypeRule */
 
 class BitVectorAckermanizationUremTypeRule {
 public:
@@ -152,10 +150,9 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
     }
-    return lhsType; 
+    return lhsType;
   }
-};
-
+};/* class BitVectorAckermanizationUremTypeRule */
 
 class BitVectorExtractTypeRule {
 public:
@@ -181,7 +178,7 @@ public:
     }
     return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
   }
-};
+};/* class BitVectorExtractTypeRule */
 
 class BitVectorExtractOpTypeRule {
 public:
@@ -190,9 +187,9 @@ public:
     Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
     return nodeManager->builtinOperatorType();
   }
-};
+};/* class BitVectorExtractOpTypeRule */
 
-class BitVectorConcatRule {
+class BitVectorConcatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
@@ -211,7 +208,7 @@ public:
     }
     return nodeManager->mkBitVectorType(size);
   }
-};
+};/* class BitVectorConcatTypeRule */
 
 class BitVectorRepeatTypeRule {
 public:
@@ -227,7 +224,7 @@ public:
     unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
     return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
   }
-};
+};/* class BitVectorRepeatTypeRule */
 
 class BitVectorExtendTypeRule {
 public:
@@ -245,7 +242,7 @@ public:
         (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
     return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
   }
-};
+};/* class BitVectorExtendTypeRule */
 
 class BitVectorConversionTypeRule {
 public:
@@ -268,7 +265,7 @@ public:
 
     InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
   }
-};
+};/* class BitVectorConversionTypeRule */
 
 class CardinalityComputer {
 public:
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 705a784f2..824dc5b92 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_bv_utils.h
+/*! \file theory_bv_utils.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Morgan Deters, Kshitij Bansal
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 9679c0260..6ebc9db92 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Morgan Deters, Kshitij Bansal
+ ** Minor contributors (to current version): Kshitij Bansal, Clark Barrett, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -24,10 +24,13 @@
 #include <sstream>
 #include "expr/node_manager.h"
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
+
+typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
 namespace utils {
 
 inline uint32_t pow2(uint32_t power) {
@@ -254,8 +257,6 @@ inline unsigned isPow2Const(TNode node) {
   return bv.isPow2(); 
 }
 
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-
 inline Node mkOr(const std::vector<Node>& nodes) {
   std::set<TNode> all;
   all.insert(nodes.begin(), nodes.end());
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 01741737f..1d835dd23 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **