merged golden

20 files changed, 644 insertions, 465 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 8579012ab..d17dd588f 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -12,7 +12,7 @@
  ** \brief [[ Add one-line brief description here ]]
  **
  ** [[ Add lengthier description here ]]
- ** 
+ **
  **/
 
 #include "bitblaster.h"
@@ -29,7 +29,7 @@
 using namespace std;
 
 using namespace CVC4::theory::bv::utils;
-using namespace CVC4::context; 
+using namespace CVC4::context;
 using namespace CVC4::prop;
 
 namespace CVC4 {
@@ -37,20 +37,20 @@ namespace theory {
 namespace bv{
 
 std::string toString(Bits&  bits) {
-  ostringstream os; 
+  ostringstream os;
   for (int i = bits.size() - 1; i >= 0; --i) {
     TNode bit = bits[i];
     if (bit.getKind() == kind::CONST_BOOLEAN) {
       os << (bit.getConst<bool>() ? "1" : "0");
     } else {
-      os << bit<< " ";   
+      os << bit<< " ";
     }
   }
   os <<"\n";
-  
-  return os.str(); 
+
+  return os.str();
 }
-/////// Bitblaster 
+/////// Bitblaster
 
 Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_bv(bv),
@@ -64,38 +64,41 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context());
 
     MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
-    d_satSolver->setNotify(notify); 
+    d_satSolver->setNotify(notify);
     // initializing the bit-blasting strategies
-    initAtomBBStrategies(); 
-    initTermBBStrategies(); 
+    initAtomBBStrategies();
+    initTermBBStrategies();
   }
 
 Bitblaster::~Bitblaster() {
   delete d_cnfStream;
-  delete d_satSolver; 
+  delete d_satSolver;
 }
 
 
-/** 
+/**
  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
  * NOTE: duplicate clauses are not detected because of marker literal
  * @param node the atom to be bitblasted
- * 
+ *
  */
 void Bitblaster::bbAtom(TNode node) {
   node = node.getKind() == kind::NOT?  node[0] : node;
-  
+
   if (hasBBAtom(node)) {
-    return; 
+    return;
   }
 
   // make sure it is marked as an atom
-  addAtom(node); 
+  addAtom(node);
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
-  Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
+  Node normalized = Rewriter::rewrite(node);
+  Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
+      Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
+      normalized;
   // asserting that the atom is true iff the definition holds
   Node atom_definition = mkNode(kind::IFF, node, atom_bb);
 
@@ -123,14 +126,14 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
-  
+
   Assert (bits.size() == utils::getSize(node));
 
-  cacheTermDef(node, bits); 
+  cacheTermDef(node, bits);
 }
 
 Node Bitblaster::bbOptimize(TNode node) {
@@ -139,21 +142,21 @@ Node Bitblaster::bbOptimize(TNode node) {
    if (node.getKind() == kind::BITVECTOR_PLUS) {
     if (RewriteRule<BBPlusNeg>::applies(node)) {
       Node res = RewriteRule<BBPlusNeg>::run<false>(node);
-      return res; 
+      return res;
     }
     //  if (RewriteRule<BBFactorOut>::applies(node)) {
     //   Node res = RewriteRule<BBFactorOut>::run<false>(node);
-    //   return res; 
-    // } 
+    //   return res;
+    // }
 
   } else if (node.getKind() == kind::BITVECTOR_MULT) {
     if (RewriteRule<MultPow2>::applies(node)) {
       Node res = RewriteRule<MultPow2>::run<false>(node);
-      return res; 
+      return res;
     }
   }
-  
-  return node; 
+
+  return node;
 }
 
 /// Public methods
@@ -170,31 +173,31 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
   std::vector<SatLiteral> literal_explanation;
   d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation);
   for (unsigned i = 0; i < literal_explanation.size(); ++i) {
-    explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); 
+    explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
   }
 }
 
 
-/** 
+/*
  * Asserts the clauses corresponding to the atom to the Sat Solver
  * by turning on the marker literal (i.e. setting it to false)
  * @param node the atom to be asserted
- * 
+ *
  */
- 
+
 bool Bitblaster::propagate() {
   return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
 }
 
 bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   // strip the not
-  TNode atom; 
+  TNode atom;
   if (lit.getKind() == kind::NOT) {
-    atom = lit[0]; 
+    atom = lit[0];
   } else {
-    atom = lit; 
+    atom = lit;
   }
-  
+
   Assert (hasBBAtom(atom));
 
   SatLiteral markerLit = d_cnfStream->getLiteral(atom);
@@ -202,9 +205,9 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   if(lit.getKind() == kind::NOT) {
     markerLit = ~markerLit;
   }
-  
+
   Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
-  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";
 
   SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
@@ -214,13 +217,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   return ret == prop::SAT_VALUE_TRUE;
 }
 
-/** 
- * Calls the solve method for the Sat Solver. 
+/**
+ * Calls the solve method for the Sat Solver.
  * passing it the marker literals to be asserted
- * 
+ *
  * @return true for sat, and false for unsat
  */
- 
+
 bool Bitblaster::solve(bool quick_solve) {
   if (Trace.isOn("bitvector")) {
     Trace("bitvector") << "Bitblaster::solve() asserted atoms ";
@@ -229,24 +232,24 @@ bool Bitblaster::solve(bool quick_solve) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
-  return SAT_VALUE_TRUE == d_satSolver->solve(); 
+  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
+  return SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
 void Bitblaster::getConflict(std::vector<TNode>& conflict) {
   SatClause conflictClause;
   d_satSolver->getUnsatCore(conflictClause);
-  
+
   for (unsigned i = 0; i < conflictClause.size(); i++) {
-    SatLiteral lit = conflictClause[i]; 
+    SatLiteral lit = conflictClause[i];
     TNode atom = d_cnfStream->getNode(lit);
-    Node  not_atom; 
+    Node  not_atom;
     if (atom.getKind() == kind::NOT) {
       not_atom = atom[0];
     } else {
-      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); 
+      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom);
     }
-    conflict.push_back(not_atom); 
+    conflict.push_back(not_atom);
   }
 }
 
@@ -256,9 +259,9 @@ void Bitblaster::getConflict(std::vector<TNode>& conflict) {
 
 void Bitblaster::initAtomBBStrategies() {
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_atomBBStrategies[i] = UndefinedAtomBBStrategy; 
+    d_atomBBStrategies[i] = UndefinedAtomBBStrategy;
   }
-  
+
   /// setting default bb strategies for atoms
   d_atomBBStrategies [ kind::EQUAL ]           = DefaultEqBB;
   d_atomBBStrategies [ kind::BITVECTOR_ULT ]   = DefaultUltBB;
@@ -269,7 +272,7 @@ void Bitblaster::initAtomBBStrategies() {
   d_atomBBStrategies [ kind::BITVECTOR_SLE ]   = DefaultSleBB;
   d_atomBBStrategies [ kind::BITVECTOR_SGT ]   = DefaultSgtBB;
   d_atomBBStrategies [ kind::BITVECTOR_SGE ]   = DefaultSgeBB;
-  
+
 }
 
 void Bitblaster::initTermBBStrategies() {
@@ -278,7 +281,7 @@ void Bitblaster::initTermBBStrategies() {
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
     d_termBBStrategies[i] = DefaultVarBB;
   }
-  
+
   /// setting default bb strategies for terms:
   //  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
   d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB;
@@ -295,13 +298,13 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_PLUS ]         = DefaultPlusBB;
   d_termBBStrategies [ kind::BITVECTOR_SUB ]          = DefaultSubBB;
   d_termBBStrategies [ kind::BITVECTOR_NEG ]          = DefaultNegBB;
-  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy;
   d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ]   = DefaultUdivBB;
   d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ]   = DefaultUremBB;
-  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy;
   d_termBBStrategies [ kind::BITVECTOR_SHL ]          = DefaultShlBB;
   d_termBBStrategies [ kind::BITVECTOR_LSHR ]         = DefaultLshrBB;
   d_termBBStrategies [ kind::BITVECTOR_ASHR ]         = DefaultAshrBB;
@@ -313,22 +316,22 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ]  = DefaultRotateLeftBB;
 
 }
- 
+
 bool Bitblaster::hasBBAtom(TNode atom) const {
   return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end();
 }
 
 void Bitblaster::cacheTermDef(TNode term, Bits def) {
   Assert (d_termCache.find(term) == d_termCache.end());
-  d_termCache[term] = def; 
+  d_termCache[term] = def;
 }
 
 bool Bitblaster::hasBBTerm(TNode node) const {
-  return d_termCache.find(node) != d_termCache.end(); 
+  return d_termCache.find(node) != d_termCache.end();
 }
 
 void Bitblaster::getBBTerm(TNode node, Bits& bits) const {
-  Assert (hasBBTerm(node)); 
+  Assert (hasBBTerm(node));
   // copy?
   bits = d_termCache.find(node)->second;
 }
@@ -337,7 +340,7 @@ Bitblaster::Statistics::Statistics() :
   d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0),
   d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0),
   d_numTerms("theory::bv::NumberOfBitblastedTerms", 0),
-  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), 
+  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0),
   d_bitblastTimer("theory::bv::BitblastTimer")
 {
   StatisticsRegistry::registerStat(&d_numTermClauses);
@@ -374,7 +377,7 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
 };
 
 void Bitblaster::MinisatNotify::safePoint() {
-  d_bv->d_out->safePoint(); 
+  d_bv->d_out->safePoint();
 }
 
 EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
@@ -417,70 +420,77 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
 
 
 bool Bitblaster::isSharedTerm(TNode node) {
-  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
+  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
 
 bool Bitblaster::hasValue(TNode a) {
-  Assert (d_termCache.find(a) != d_termCache.end()); 
+  Assert (d_termCache.find(a) != d_termCache.end());
   Bits bits = d_termCache[a];
   for (int i = bits.size() -1; i >= 0; --i) {
-    SatValue bit_value; 
-    if (d_cnfStream->hasLiteral(bits[i])) { 
+    SatValue bit_value;
+    if (d_cnfStream->hasLiteral(bits[i])) {
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
       if (bit_value == SAT_VALUE_UNKNOWN)
-        return false; 
+        return false;
     } else {
-      return false; 
+      return false;
     }
   }
-  return true; 
+  return true;
 }
-/** 
+/**
  * Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned. 
- * 
- * @param a 
- * 
- * @return 
+ * 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 Bitblaster::getVarValue(TNode a) {
+Node Bitblaster::getVarValue(TNode a, bool fullModel) {
   if (d_termCache.find(a) == d_termCache.end()) {
     Assert(isSharedTerm(a));
-    return Node(); 
+    return Node();
   }
   Bits bits = d_termCache[a];
-  Integer value(0); 
+  Integer value(0);
   for (int i = bits.size() -1; i >= 0; --i) {
     SatValue bit_value;
-    if (d_cnfStream->hasLiteral(bits[i])) { 
+    if (d_cnfStream->hasLiteral(bits[i])) {
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != SAT_VALUE_UNKNOWN); 
+      Assert (bit_value != SAT_VALUE_UNKNOWN);
     } else {
-      // the bit is unconstrainted so we can give it an arbitrary value 
+      //TODO: return Node() if fullModel=false?
+      // the bit is unconstrainted so we can give it an arbitrary value
       bit_value = SAT_VALUE_FALSE;
     }
-    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); 
-    value = value * 2 + bit_int;  
+    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+    value = value * 2 + bit_int;
   }
-  return utils::mkConst(BitVector(bits.size(), value));  
+  return utils::mkConst(BitVector(bits.size(), value));
 }
 
-void Bitblaster::collectModelInfo(TheoryModel* m) {
+void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::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);
+      Node const_value = getVarValue(var, fullModel);
       if(const_value == Node()) {
-        // if the value is unassigned just set it to zero
-        const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); 
+        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") << "Bitblaster::collectModelInfo (assert (= "
+                                  << var << " "
+                                  << const_value << "))\n";
+        m->assertEquality(var, const_value, true);
       }
-      Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
-                                << var << " "
-                                << const_value << "))\n";
-      m->assertEquality(var, const_value, true); 
     }
   }
 }
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index c122c407d..6fab0369c 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -55,14 +55,14 @@ namespace bv {
 
 typedef std::vector<Node> Bits;
 
-std::string toString (Bits& bits); 
+std::string toString (Bits& bits);
 
 class TheoryBV;
 
-/** 
- * The Bitblaster that manages the mapping between Nodes 
- * and their bitwise definition 
- * 
+/**
+ * The Bitblaster that manages the mapping between Nodes
+ * and their bitwise definition
+ *
  */
 class Bitblaster {
 
@@ -79,26 +79,26 @@ class Bitblaster {
     void notify(prop::SatClause& clause);
     void safePoint();
   };
-  
-  
+
+
   typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      VarSet; 
-  
-  typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*); 
-  typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*); 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      VarSet;
+
+  typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*);
+  typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*);
 
   TheoryBV *d_bv;
-  
+
   // sat solver used for bitblasting and associated CnfStream
   theory::OutputChannel*             d_bvOutput;
-  prop::BVSatSolverInterface*        d_satSolver; 
+  prop::BVSatSolverInterface*        d_satSolver;
   prop::CnfStream*                   d_cnfStream;
 
   // caches and mappings
   TermDefMap                   d_termCache;
   AtomSet                      d_bitblastedAtoms;
-  VarSet                       d_variables; 
+  VarSet                       d_variables;
   context::CDList<prop::SatLiteral>  d_assertedAtoms; /**< context dependent list storing the atoms
                                                        currently asserted by the DPLL SAT solver. */
 
@@ -111,79 +111,80 @@ class Bitblaster {
 
   /// function tables for the various bitblasting strategies indexed by node kind
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
-  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; 
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
 
   // helper methods to initialize function tables
   void initAtomBBStrategies();
-  void initTermBBStrategies(); 
+  void initTermBBStrategies();
 
   // returns a node that might be easier to bitblast
-  Node bbOptimize(TNode node); 
-  
-  void addAtom(TNode atom); 
+  Node bbOptimize(TNode node);
+
+  void addAtom(TNode atom);
   // division is bitblasted in terms of constraints
   // so it needs to use private bitblaster interface
   void bbUdiv(TNode node, Bits& bits);
   void bbUrem(TNode node, Bits& bits);
-  bool hasValue(TNode a); 
+  bool hasValue(TNode a);
 public:
   void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
-  
-  Bitblaster(context::Context* c, bv::TheoryBV* bv); 
+
+  Bitblaster(context::Context* c, bv::TheoryBV* bv);
   ~Bitblaster();
   bool assertToSat(TNode node, bool propagate = true);
   bool propagate();
   bool solve(bool quick_solve = false);
-  void getConflict(std::vector<TNode>& conflict); 
+  void getConflict(std::vector<TNode>& conflict);
   void explain(TNode atom, std::vector<TNode>& explanation);
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  /** 
+  /**
    * Return a constant Node representing the value of a variable
-   * in the current model. 
-   * @param a 
-   * 
-   * @return 
+   * in the current model.
+   * @param a
+   *
+   * @return
    */
-  Node getVarValue(TNode a);
-  /** 
-   * Adds a constant value for each bit-blasted variable in the model. 
-   * 
-   * @param m the model 
+  Node getVarValue(TNode a, bool fullModel=true);
+  /**
+   * Adds a constant value for each bit-blasted variable in the model.
+   *
+   * @param m the model
+   * @param fullModel whether to create a "full model," i.e., add
+   * constants to equivalence classes that don't already have them
    */
-  void collectModelInfo(TheoryModel* m); 
-  /** 
-   * Stores the variable (or non-bv term) and its corresponding bits. 
-   * 
-   * @param var 
-   * @param bits 
+  void collectModelInfo(TheoryModel* m, bool fullModel);
+  /**
+   * Stores the variable (or non-bv term) and its corresponding bits.
+   *
+   * @param var
    */
   void storeVariable(TNode var) {
-    d_variables.insert(var); 
+    d_variables.insert(var);
   }
 
   bool isSharedTerm(TNode node);
   uint64_t computeAtomWeight(TNode node);
 
 private:
- 
+
   class Statistics {
   public:
     IntStat d_numTermClauses, d_numAtomClauses;
-    IntStat d_numTerms, d_numAtoms; 
+    IntStat d_numTerms, d_numAtoms;
     TimerStat d_bitblastTimer;
     Statistics();
-    ~Statistics(); 
-  }; 
-  
+    ~Statistics();
+  };
+
   Statistics d_statistics;
 };
 
 
 
-} /* bv namespace */ 
+} /* bv namespace */
 
 } /* theory namespace */
 
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 8374a3f75..0b0551283 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Algebraic solver. 
+ ** \brief Algebraic solver.
  **
  ** Algebraic solver.
  **/
@@ -46,7 +46,7 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
     out << "BV_CORE_SUBTHEORY";
     break;
   case SUB_INEQUALITY:
-    out << "BV_INEQUALITY_SUBTHEORY"; 
+    out << "BV_INEQUALITY_SUBTHEORY";
   default:
     Unreachable();
     break;
@@ -55,13 +55,10 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
 }
 
 
-const bool d_useEqualityEngine = true;
-const bool d_useSatPropagation = true;
+// forward declaration
+class TheoryBV;
 
-// forward declaration 
-class TheoryBV; 
-
-typedef context::CDQueue<Node> AssertionQueue; 
+typedef context::CDQueue<Node> AssertionQueue;
 /**
  * Abstract base class for bit-vector subtheory solvers
  *
@@ -78,7 +75,7 @@ protected:
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t>  d_assertionIndex;
 public:
-  
+
   SubtheorySolver(context::Context* c, TheoryBV* bv) :
     d_context(c),
     d_bv(bv),
@@ -86,24 +83,24 @@ public:
     d_assertionIndex(c, 0)
   {}
   virtual ~SubtheorySolver() {}
-  virtual bool check(Theory::Effort e) = 0; 
+  virtual bool check(Theory::Effort e) = 0;
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void preRegister(TNode node) {}
   virtual void propagate(Theory::Effort e) {}
-  virtual void collectModelInfo(TheoryModel* m) = 0;
-  virtual Node getModelValue(TNode var) = 0; 
+  virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+  virtual Node getModelValue(TNode var) = 0;
   virtual bool isComplete() = 0;
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
-  virtual void addSharedTerm(TNode node) {} 
+  virtual void addSharedTerm(TNode node) {}
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
-    Assert (!done()); 
+    Assert (!done());
     TNode res = d_assertionQueue[d_assertionIndex];
     d_assertionIndex = d_assertionIndex + 1;
-    return res; 
+    return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-}; 
+};
 
 }
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 2308f36a3..5a0c17134 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -34,7 +34,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
     d_bitblaster(new Bitblaster(c, bv)),
     d_bitblastQueue(c),
     d_statistics(),
-    d_validModelCache(c, true)
+    d_validModelCache(c, true),
+    d_useSatPropagation(options::bvPropagate())
 {}
 
 BitblastSolver::~BitblastSolver() {
@@ -83,20 +84,20 @@ void BitblastSolver::bitblastQueue() {
 }
 
 bool BitblastSolver::check(Theory::Effort e) {
-  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; 
+  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
   Assert(!options::bitvectorEagerBitblast());
 
-  ++(d_statistics.d_numCallstoCheck); 
+  ++(d_statistics.d_numCallstoCheck);
 
   //// Lazy bit-blasting
   // bit-blast enqueued nodes
   bitblastQueue();
 
-  // Processing assertions  
+  // Processing assertions
   while (!done()) {
     TNode fact = get();
     d_validModelCache = false;
-    Debug("bv-bitblast") << "  fact " << fact << ")\n"; 
+    Debug("bv-bitblast") << "  fact " << fact << ")\n";
     if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
@@ -143,8 +144,8 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
   return d_bitblaster->getEqualityStatus(a, b);
 }
 
-void BitblastSolver::collectModelInfo(TheoryModel* m) {
-  return d_bitblaster->collectModelInfo(m); 
+void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
 Node BitblastSolver::getModelValue(TNode node)
@@ -188,5 +189,5 @@ Node BitblastSolver::getModelValueRec(TNode node)
   Assert(val.isConst());
   d_modelCache[node] = val;
   Debug("bitvector-model") << node << " => " << val <<"\n";
-  return val; 
+  return val;
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 819b3d62c..f1204dbdf 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -19,7 +19,6 @@
 #pragma once
 
 #include "theory/bv/bv_subtheory.h"
-#include "theory/substitutions.h"
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -33,20 +32,21 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics(); 
-  }; 
+    ~Statistics();
+  };
   /** Bitblaster */
   Bitblaster* d_bitblaster;
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
-  Statistics d_statistics; 
+  Statistics d_statistics;
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_modelCache;
   context::CDO<bool> d_validModelCache;
   Node getModelValueRec(TNode node);
 
+  bool  d_useSatPropagation;
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
@@ -55,7 +55,7 @@ public:
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo(TheoryModel* m); 
+  void collectModelInfo(TheoryModel* m, bool fullModel);
   Node getModelValue(TNode node);
   bool isComplete() { return true; }
   void bitblastQueue();
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c0546f892..45946b8c8 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -37,53 +37,48 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
     d_isCoreTheory(c, true),
     d_reasons(c)
 {
-  if (d_useEqualityEngine) {
-
-    // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
-  }
+
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
 }
 
 CoreSolver::~CoreSolver() {
-  delete d_slicer; 
+  delete d_slicer;
 }
 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
 void CoreSolver::preRegister(TNode node) {
-  if (!d_useEqualityEngine)
-    return;
-
   if (node.getKind() == kind::EQUAL) {
       d_equalityEngine.addTriggerEquality(node);
       if (options::bitvectorCoreSolver()) {
@@ -109,51 +104,51 @@ Node CoreSolver::getBaseDecomposition(TNode a) {
   std::vector<Node> a_decomp;
   d_slicer->getBaseDecomposition(a, a_decomp);
   Node new_a = utils::mkConcat(a_decomp);
-  Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n"; 
-  return new_a; 
+  Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
+  return new_a;
 }
 
 bool CoreSolver::decomposeFact(TNode fact) {
-  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;  
+  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
   // assert decompositions since the equality engine does not know the semantics of
   // concat:
   //   a == a_1 concat ... concat a_k
   //   b == b_1 concat ... concat b_k
-  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;  
-  // FIXME: are this the right things to assert? 
+  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
+  // FIXME: are this the right things to assert?
   // assert decompositions since the equality engine does not know the semantics of
   // concat:
   //   a == a_1 concat ... concat a_k
   //   b == b_1 concat ... concat b_k
-  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; 
+  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
 
   TNode a = eq[0];
   TNode b = eq[1];
   Node new_a = getBaseDecomposition(a);
-  Node new_b = getBaseDecomposition(b); 
-  
+  Node new_b = getBaseDecomposition(b);
+
   Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
-          utils::getSize(new_a) == utils::getSize(a)); 
-  
+          utils::getSize(new_a) == utils::getSize(a));
+
   NodeManager* nm = NodeManager::currentNM();
   Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
   Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 
   bool ok = true;
   ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
-  if (!ok) return false; 
+  if (!ok) return false;
   ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
-  if (!ok) return false; 
+  if (!ok) return false;
   ok = assertFactToEqualityEngine(fact, fact);
   if (!ok) return false;
-  
+
   if (fact.getKind() == kind::EQUAL) {
     // assert the individual equalities as well
     //    a_i == b_i
     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
         new_b.getKind() == kind::BITVECTOR_CONCAT) {
-      
-      Assert (new_a.getNumChildren() == new_b.getNumChildren()); 
+
+      Assert (new_a.getNumChildren() == new_b.getNumChildren());
       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
         ok = assertFactToEqualityEngine(eq_i, fact);
@@ -161,23 +156,23 @@ bool CoreSolver::decomposeFact(TNode fact) {
       }
     }
   }
-  return true; 
+  return true;
 }
 
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
   Assert (!d_bv->inConflict());
-  ++(d_statistics.d_numCallstoCheck); 
-  bool ok = true; 
+  ++(d_statistics.d_numCallstoCheck);
+  bool ok = true;
   std::vector<Node> core_eqs;
   while (! done()) {
-    TNode fact = get(); 
-    
+    TNode fact = get();
+
     // update whether we are in the core fragment
     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
-      d_isCoreTheory = false; 
+      d_isCoreTheory = false;
     }
-    
+
     // only reason about equalities
     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
       if (options::bitvectorCoreSolver()) {
@@ -186,31 +181,31 @@ bool CoreSolver::check(Theory::Effort e) {
         ok = assertFactToEqualityEngine(fact, fact);
       }
     } else {
-      ok = assertFactToEqualityEngine(fact, fact); 
+      ok = assertFactToEqualityEngine(fact, fact);
     }
     if (!ok)
-      return false; 
+      return false;
   }
-  
+
   if (Theory::fullEffort(e) && isComplete()) {
     buildModel();
   }
-  
+
   return true;
 }
 
 void CoreSolver::buildModel() {
   if (options::bitvectorCoreSolver()) {
     // FIXME
-    Unreachable(); 
-    return; 
+    Unreachable();
+    return;
   }
-  Debug("bv-core") << "CoreSolver::buildModel() \n"; 
-  d_modelValues.clear(); 
+  Debug("bv-core") << "CoreSolver::buildModel() \n";
+  d_modelValues.clear();
   TNodeSet constants;
-  TNodeSet constants_in_eq_engine; 
+  TNodeSet constants_in_eq_engine;
   // collect constants in equality engine
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); 
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
   while (!eqcs_i.isFinished()) {
     TNode repr = *eqcs_i;
     if  (repr.getKind() == kind::CONST_BITVECTOR) {
@@ -218,39 +213,39 @@ void CoreSolver::buildModel() {
       eq::EqClassIterator it(repr, &d_equalityEngine);
       if (!(++it).isFinished() || true) {
         constants.insert(repr);
-        constants_in_eq_engine.insert(repr); 
+        constants_in_eq_engine.insert(repr);
       }
     }
-    ++eqcs_i; 
+    ++eqcs_i;
   }
   // build repr to value map
-  
+
   eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
   while (!eqcs_i.isFinished()) {
     TNode repr = *eqcs_i;
     ++eqcs_i;
-    
+
     if (repr.getKind() != kind::VARIABLE &&
         repr.getKind() != kind::SKOLEM &&
         repr.getKind() != kind::CONST_BITVECTOR &&
         !d_bv->isSharedTerm(repr)) {
-      continue; 
+      continue;
     }
-  
-    TypeNode type = repr.getType(); 
+
+    TypeNode type = repr.getType();
     if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
-      Debug("bv-core-model") << "   processing " << repr <<"\n"; 
+      Debug("bv-core-model") << "   processing " << repr <<"\n";
       // we need to assign a value for it
       TypeEnumerator te(type);
-      Node val; 
+      Node val;
       do {
-        val = *te; 
+        val = *te;
         ++te;
         // Debug("bv-core-model") << "  trying value " << val << "\n";
         // Debug("bv-core-model") << "  is in set? " << constants.count(val) << "\n";
-        // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n"; 
+        // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n";
       } while (constants.count(val) != 0 && !(te.isFinished()));
-      
+
       if (te.isFinished() && constants.count(val) != 0) {
         // if we cannot enumerate anymore values we just return the lemma stating that
         // at least two of the representatives are equal.
@@ -259,15 +254,15 @@ void CoreSolver::buildModel() {
 
         for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
              it != constants_in_eq_engine.end(); ++it) {
-          TNode constant = *it; 
+          TNode constant = *it;
           if (utils::getSize(constant) == utils::getSize(repr)) {
-            representatives.push_back(constant); 
+            representatives.push_back(constant);
           }
         }
         for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
           representatives.push_back(it->first);
         }
-        std::vector<Node> equalities; 
+        std::vector<Node> equalities;
         for (unsigned i = 0; i < representatives.size(); ++i) {
           for (unsigned j = i + 1; j < representatives.size(); ++j) {
             TNode a = representatives[i];
@@ -279,19 +274,19 @@ void CoreSolver::buildModel() {
         }
         Node lemma = utils::mkOr(equalities);
         d_bv->lemma(lemma);
-        Debug("bv-core") << "  lemma: " << lemma << "\n"; 
-        return; 
+        Debug("bv-core") << "  lemma: " << lemma << "\n";
+        return;
       }
       Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
       constants.insert(val);
-      d_modelValues[repr] = val; 
+      d_modelValues[repr] = val;
     }
   }
 }
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
-  // Notify the equality engine 
-  if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+  // Notify the equality engine
+  if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
     bool negated = fact.getKind() == kind::NOT;
@@ -315,8 +310,8 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // checking for a conflict
   if (d_bv->inConflict()) {
     return false;
-  }  
-  return true; 
+  }
+  return true;
 }
 
 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
@@ -361,10 +356,10 @@ void CoreSolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(conflict);
 }
 
-void CoreSolver::collectModelInfo(TheoryModel* m) {
+void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
   if (options::bitvectorCoreSolver()) {
     Unreachable();
-    return; 
+    return;
   }
   if (Debug.isOn("bitvector-model")) {
     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
@@ -377,11 +372,11 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
   d_bv->computeRelevantTerms(termSet);
   m->assertEqualityEngine(&d_equalityEngine, &termSet);
   if (isComplete()) {
-    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; 
+    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
       Node a = it->first;
       Node b = it->second;
-      m->assertEquality(a, b, true); 
+      m->assertEquality(a, b, true);
     }
   }
 }
@@ -390,23 +385,23 @@ Node CoreSolver::getModelValue(TNode var) {
   // we don't need to evaluate bv expressions and only look at variable values
   // because this only gets called when the core theory is complete (i.e. no other bv
   // function symbols are currently asserted)
-  Assert (d_slicer->isCoreTerm(var)); 
-  
-  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";  
+  Assert (d_slicer->isCoreTerm(var));
+
+  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
   Assert (isComplete());
   TNode repr = d_equalityEngine.getRepresentative(var);
-  Node result = Node(); 
+  Node result = Node();
   if (repr.getKind() == kind::CONST_BITVECTOR) {
-    result = repr; 
+    result = repr;
   } else if (d_modelValues.find(repr) == d_modelValues.end()) {
     // it may be a shared term that never gets asserted
     // result is just Null
     Assert(d_bv->isSharedTerm(var));
   } else {
-    result = d_modelValues[repr]; 
+    result = d_modelValues[repr];
   }
-  Debug("bitvector-model") << " => " << result <<"\n"; 
-  return result; 
+  Debug("bitvector-model") << " => " << result <<"\n";
+  return result;
 }
 
 CoreSolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 423408a7c..b886bbdd5 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -25,21 +25,21 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class Slicer; 
-class Base; 
+class Slicer;
+class Base;
 /**
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
   typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
 
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics(); 
-  }; 
-  
+    ~Statistics();
+  };
+
   // NotifyClass: handles call-back from congruence closure module
   class NotifyClass : public eq::EqualityEngineNotify {
     CoreSolver& d_solver;
@@ -59,13 +59,13 @@ class CoreSolver : public SubtheorySolver {
 
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
-  
+
   /** Equality engine */
   eq::EqualityEngine d_equalityEngine;
 
   /** Store a propagation to the bv solver */
   bool storePropagation(TNode literal);
-  
+
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
@@ -74,12 +74,12 @@ class CoreSolver : public SubtheorySolver {
   /** To make sure we keep the explanations */
   context::CDHashSet<Node, NodeHashFunction> d_reasons;
   ModelValue d_modelValues;
-  void buildModel(); 
-  bool assertFactToEqualityEngine(TNode fact, TNode reason);  
+  void buildModel();
+  bool assertFactToEqualityEngine(TNode fact, TNode reason);
   bool decomposeFact(TNode fact);
   Node getBaseDecomposition(TNode a);
-  Statistics d_statistics; 
-public: 
+  Statistics d_statistics;
+public:
   CoreSolver(context::Context* c, TheoryBV* bv);
   ~CoreSolver();
   bool  isComplete() { return d_isCoreTheory; }
@@ -87,8 +87,8 @@ public:
   void  preRegister(TNode node);
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
-  void  collectModelInfo(TheoryModel* m);
-  Node  getModelValue(TNode var); 
+  void  collectModelInfo(TheoryModel* m, bool fullModel);
+  Node  getModelValue(TNode var);
   void  addSharedTerm(TNode t) {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index f45250f5b..a3970c9e3 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -29,17 +29,17 @@ using namespace CVC4::theory::bv::utils;
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
   ++(d_statistics.d_numCallstoCheck);
-  
-  bool ok = true; 
+
+  bool ok = true;
   while (!done() && ok) {
     TNode fact = get();
-    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n"; 
+    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n";
     if (fact.getKind() == kind::EQUAL) {
       TNode a = fact[0];
       TNode b = fact[1];
       ok = d_inequalityGraph.addInequality(a, b, false, fact);
       if (ok)
-        ok = d_inequalityGraph.addInequality(b, a, false, fact); 
+        ok = d_inequalityGraph.addInequality(b, a, false, fact);
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
       TNode a = fact[0][0];
       TNode b = fact[0][1];
@@ -47,40 +47,40 @@ bool InequalitySolver::check(Theory::Effort e) {
     }
     if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0][1];
-      TNode b = fact[0][0]; 
+      TNode b = fact[0][0];
       ok = d_inequalityGraph.addInequality(a, b, true, fact);
       // propagate
       // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
-      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
       //   d_bv->storePropagation(neq, SUB_INEQUALITY);
       //   d_explanations[neq] = fact;
       // }
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0][1];
-      TNode b = fact[0][0]; 
+      TNode b = fact[0][0];
       ok = d_inequalityGraph.addInequality(a, b, false, fact);
     } else if (fact.getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0];
-      TNode b = fact[1]; 
+      TNode b = fact[1];
       ok = d_inequalityGraph.addInequality(a, b, true, fact);
       // propagate
       // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
-      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
       //   d_bv->storePropagation(neq, SUB_INEQUALITY);
       //   d_explanations[neq] = fact;
       // }
     } else if (fact.getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0];
-      TNode b = fact[1]; 
+      TNode b = fact[1];
       ok = d_inequalityGraph.addInequality(a, b, false, fact);
     }
   }
-  
+
   if (!ok) {
     std::vector<TNode> conflict;
-    d_inequalityGraph.getConflict(conflict); 
+    d_inequalityGraph.getConflict(conflict);
     d_bv->setConflict(utils::flattenAnd(conflict));
-    return false; 
+    return false;
   }
 
   if (isComplete() && Theory::fullEffort(e)) {
@@ -89,36 +89,39 @@ bool InequalitySolver::check(Theory::Effort e) {
     std::vector<Node> lemmas;
     d_inequalityGraph.checkDisequalities(lemmas);
     for(unsigned i = 0; i < lemmas.size(); ++i) {
-      d_bv->lemma(lemmas[i]); 
+      d_bv->lemma(lemmas[i]);
     }
   }
-  return true; 
+  return true;
 }
 
 EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
+  if (!isComplete())
+    return EQUALITY_UNKNOWN;
+
   Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
   Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
 
   // if an inequality containing the terms has been asserted then we know
   // the equality is false
   if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) {
-    return EQUALITY_FALSE; 
+    return EQUALITY_FALSE;
   }
-  
+
   if (!d_inequalityGraph.hasValueInModel(a) ||
       !d_inequalityGraph.hasValueInModel(b)) {
-    return EQUALITY_UNKNOWN; 
+    return EQUALITY_UNKNOWN;
   }
 
   // TODO: check if this disequality is entailed by inequalities via transitivity
-  
+
   BitVector a_val = d_inequalityGraph.getValueInModel(a);
   BitVector b_val = d_inequalityGraph.getValueInModel(b);
-  
+
   if (a_val == b_val) {
-    return EQUALITY_TRUE_IN_MODEL; 
+    return EQUALITY_TRUE_IN_MODEL;
   } else {
-    return EQUALITY_FALSE_IN_MODEL; 
+    return EQUALITY_FALSE_IN_MODEL;
   }
 }
 
@@ -126,19 +129,19 @@ void InequalitySolver::assertFact(TNode fact) {
   d_assertionQueue.push_back(fact);
   d_assertionSet.insert(fact);
   if (!isInequalityOnly(fact)) {
-    d_isComplete = false; 
+    d_isComplete = false;
   }
 }
 
 bool InequalitySolver::isInequalityOnly(TNode node) {
   if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
-    return d_ineqTermCache[node]; 
+    return d_ineqTermCache[node];
   }
-  
+
   if (node.getKind() == kind::NOT) {
-    node = node[0]; 
+    node = node[0];
   }
-  
+
   if (node.getKind() != kind::EQUAL &&
       node.getKind() != kind::BITVECTOR_ULT &&
       node.getKind() != kind::BITVECTOR_ULE &&
@@ -146,50 +149,50 @@ bool InequalitySolver::isInequalityOnly(TNode node) {
       node.getKind() != kind::SELECT &&
       node.getKind() != kind::STORE &&
       node.getMetaKind() != kind::metakind::VARIABLE) {
-    return false; 
+    return false;
   }
-  bool res = true; 
+  bool res = true;
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     res = res && isInequalityOnly(node[i]);
   }
-  d_ineqTermCache[node] = res; 
-  return res; 
+  d_ineqTermCache[node] = res;
+  return res;
 }
 
 void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   Assert (d_explanations.find(literal) != d_explanations.end());
   TNode explanation = d_explanations[literal];
   assumptions.push_back(explanation);
-  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; 
+  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
 }
 
 void InequalitySolver::propagate(Theory::Effort e) {
-  Assert (false); 
+  Assert (false);
 }
 
-void InequalitySolver::collectModelInfo(TheoryModel* m) {
-  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; 
+void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
   std::vector<Node> model;
   d_inequalityGraph.getAllValuesInModel(model);
   for (unsigned i = 0; i < model.size(); ++i) {
-    Assert (model[i].getKind() == kind::EQUAL); 
-    m->assertEquality(model[i][0], model[i][1], true); 
+    Assert (model[i].getKind() == kind::EQUAL);
+    m->assertEquality(model[i][0], model[i][1], true);
   }
 }
 
 Node InequalitySolver::getModelValue(TNode var) {
-  Assert (isInequalityOnly(var)); 
-  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";  
+  Assert (isInequalityOnly(var));
+  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
   Assert (isComplete());
-  Node result = Node(); 
+  Node result = Node();
   if (!d_inequalityGraph.hasValueInModel(var)) {
     Assert (d_bv->isSharedTerm(var));
   } else {
     BitVector val = d_inequalityGraph.getValueInModel(var);
     result = utils::mkConst(val);
   }
-  Debug("bitvector-model") << " => " << result <<"\n";  
-  return result; 
+  Debug("bitvector-model") << " => " << result <<"\n";
+  return result;
 }
 
 InequalitySolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 390a329ff..6e0139e09 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Algebraic solver. 
+ ** \brief Algebraic solver.
  **
  ** Algebraic solver.
  **/
@@ -31,16 +31,16 @@ class InequalitySolver: public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics(); 
-  }; 
+    ~Statistics();
+  };
 
-  context::CDHashSet<Node, NodeHashFunction> d_assertionSet; 
+  context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
   InequalityGraph d_inequalityGraph;
-  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; 
+  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
   context::CDO<bool> d_isComplete;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; 
-  bool isInequalityOnly(TNode node); 
-  Statistics d_statistics; 
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
+  bool isInequalityOnly(TNode node);
+  Statistics d_statistics;
 public:
   InequalitySolver(context::Context* c, TheoryBV* bv)
     : SubtheorySolver(c, bv),
@@ -51,19 +51,19 @@ public:
       d_ineqTermCache(),
       d_statistics()
   {}
-  
+
   bool check(Theory::Effort e);
-  void propagate(Theory::Effort e); 
+  void propagate(Theory::Effort e);
   void explain(TNode literal, std::vector<TNode>& assumptions);
   bool isComplete() { return d_isComplete; }
-  void collectModelInfo(TheoryModel* m); 
-  Node getModelValue(TNode var); 
+  void collectModelInfo(TheoryModel* m, bool fullModel);
+  Node getModelValue(TNode var);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void assertFact(TNode fact); 
-}; 
+  void assertFact(TNode fact);
+};
 
 }
 }
 }
 
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ 
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 052e477ea..aeae1073e 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -120,6 +120,14 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-
 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"
 
+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"
+
 typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
 
 typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
@@ -166,4 +174,7 @@ typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 
+typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
+typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
+
 endtheory
diff --git a/src/theory/bv/options b/src/theory/bv/options
index 7b87baa21..077299d1f 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -22,5 +22,11 @@ option bitvectorCoreSolver --bv-core-solver bool
 
 option bvToBool --bv-to-bool bool
  lift bit-vectors of size 1 to booleans when possible
+
+option bvPropagate --bv-propagate bool :default true
+ use bit-vector propagation in the bit-blaster
+
+option bvEquality --bv-eq bool :default true
+ use the equality engine for the bit-vector theory
  
 endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index cb68a0f65..a2de951aa 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -49,29 +49,32 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c)
   {
-    SubtheorySolver* core_solver = new CoreSolver(c, this); 
-    d_subtheories.push_back(core_solver);
-    d_subtheoryMap[SUB_CORE] = core_solver;
-
+    if (options::bvEquality()) {
+      SubtheorySolver* core_solver = new CoreSolver(c, this);
+      d_subtheories.push_back(core_solver);
+      d_subtheoryMap[SUB_CORE] = core_solver;
+    }
     if (options::bitvectorInequalitySolver()) {
-      SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
+      SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
       d_subtheories.push_back(ineq_solver);
       d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
     }
-    
-    SubtheorySolver* bb_solver = new BitblastSolver(c, this); 
+
+    SubtheorySolver* bb_solver = new BitblastSolver(c, this);
     d_subtheories.push_back(bb_solver);
     d_subtheoryMap[SUB_BITBLAST] = bb_solver;
   }
 
 TheoryBV::~TheoryBV() {
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    delete d_subtheories[i]; 
+    delete d_subtheories[i];
   }
 }
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
+  if (options::bvEquality()) {
+    dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
+  }
 }
 
 TheoryBV::Statistics::Statistics():
@@ -110,7 +113,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
     return;
   }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    d_subtheories[i]->preRegister(node); 
+    d_subtheories[i]->preRegister(node);
   }
 }
 
@@ -131,22 +134,22 @@ void TheoryBV::checkForLemma(TNode fact) {
     if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) {
       TNode urem = fact[0];
       TNode result = fact[1];
-      TNode divisor = urem[1]; 
+      TNode divisor = urem[1];
       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
       Node divisor_eq_0 = mkNode(kind::EQUAL,
                                  divisor,
-                                 mkConst(BitVector(getSize(divisor), 0u)));  
+                                 mkConst(BitVector(getSize(divisor), 0u)));
       Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
     if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
       TNode urem = fact[1];
       TNode result = fact[0];
-      TNode divisor = urem[1]; 
+      TNode divisor = urem[1];
       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
       Node divisor_eq_0 = mkNode(kind::EQUAL,
                                   divisor,
-                                  mkConst(BitVector(getSize(divisor), 0u)));  
+                                  mkConst(BitVector(getSize(divisor), 0u)));
       Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
@@ -162,9 +165,9 @@ void TheoryBV::check(Effort e)
   }
 
   if (Theory::fullEffort(e)) {
-    ++(d_statistics.d_numCallsToCheckFullEffort); 
+    ++(d_statistics.d_numCallsToCheckFullEffort);
   } else {
-    ++(d_statistics.d_numCallsToCheckStandardEffort); 
+    ++(d_statistics.d_numCallsToCheckStandardEffort);
   }
   // if we are already in conflict just return the conflict
   if (inConflict()) {
@@ -174,28 +177,29 @@ void TheoryBV::check(Effort e)
 
   while (!done()) {
     TNode fact = get().assertion;
-    checkForLemma(fact); 
+    checkForLemma(fact);
+
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-      d_subtheories[i]->assertFact(fact); 
+      d_subtheories[i]->assertFact(fact);
     }
   }
 
   bool ok = true;
   bool complete = false;
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    Assert (!inConflict()); 
+    Assert (!inConflict());
     ok = d_subtheories[i]->check(e);
-    complete = d_subtheories[i]->isComplete(); 
+    complete = d_subtheories[i]->isComplete();
 
     if (!ok) {
       // if we are in a conflict no need to check with other theories
       Assert (inConflict());
       sendConflict();
-      return; 
+      return;
     }
     if (complete) {
       // if the last subtheory was complete we stop
-      return; 
+      return;
     }
   }
 }
@@ -205,8 +209,8 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   //  Assert (fullModel); // can only query full model
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
-      d_subtheories[i]->collectModelInfo(m);
-      return; 
+      d_subtheories[i]->collectModelInfo(m, fullModel);
+      return;
     }
   }
 }
@@ -215,10 +219,10 @@ Node TheoryBV::getModelValue(TNode var) {
   Assert(!inConflict());
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
-      return d_subtheories[i]->getModelValue(var); 
+      return d_subtheories[i]->getModelValue(var);
     }
   }
-  Unreachable(); 
+  Unreachable();
 }
 
 void TheoryBV::propagate(Effort e) {
@@ -236,7 +240,7 @@ void TheoryBV::propagate(Effort e) {
   bool ok = true;
   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    // temporary fix for incremental bit-blasting 
+    // temporary fix for incremental bit-blasting
     if (d_valuation.isSatLiteral(literal)) {
       Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
       ok = d_out->propagate(literal);
@@ -286,14 +290,14 @@ Node TheoryBV::ppRewrite(TNode t)
   if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
     std::vector<Node> equalities;
     Slicer::splitEqualities(t, equalities);
-    return utils::mkAnd(equalities); 
+    return utils::mkAnd(equalities);
   }
-  
+
   return t;
 }
 
 void TheoryBV::presolve() {
-  Debug("bitvector") << "TheoryBV::presolve" << endl; 
+  Debug("bitvector") << "TheoryBV::presolve" << endl;
 }
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
@@ -318,7 +322,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
       // Safe to ignore this one, subtheory should produce a conflict
       return true;
     }
- 
+
     d_propagatedBy[literal] = subtheory;
   }
 
@@ -366,7 +370,7 @@ Node TheoryBV::explain(TNode node) {
 void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
-  if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
+  if (!options::bitvectorEagerBitblast() && options::bvEquality()) {
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
       d_subtheories[i]->addSharedTerm(t);
     }
@@ -379,11 +383,11 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
   if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }
-  
+
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
-      return status; 
+      return status;
     }
   }
   return EQUALITY_UNKNOWN; ;
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index baaf7e133..8426afb59 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -66,6 +66,9 @@ enum RewriteRuleId {
   SremEliminate,
   ZeroExtendEliminate,
   SignExtendEliminate,
+  BVToNatEliminate,
+  IntToBVEliminate,
+
   /// ground term evaluation
   EvalEquals,
   EvalConcat, 
@@ -173,13 +176,15 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case FailEq:              out << "FailEq";              return out;
   case SimplifyEq:          out << "SimplifyEq";          return out;
   case ReflexivityEq:       out << "ReflexivityEq";       return out;
-  case UgtEliminate:            out << "UgtEliminate";            return out;
-  case SgtEliminate:            out << "SgtEliminate";            return out;
-  case UgeEliminate:            out << "UgeEliminate";            return out;
-  case SgeEliminate:            out << "SgeEliminate";            return out;
+  case UgtEliminate:        out << "UgtEliminate";        return out;
+  case SgtEliminate:        out << "SgtEliminate";        return out;
+  case UgeEliminate:        out << "UgeEliminate";        return out;
+  case SgeEliminate:        out << "SgeEliminate";        return out;
   case RepeatEliminate:     out << "RepeatEliminate";     return out;
   case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
   case RotateRightEliminate:out << "RotateRightEliminate";return out;
+  case BVToNatEliminate:    out << "BVToNatEliminate";    return out;
+  case IntToBVEliminate:    out << "IntToBVEliminate";    return out;
   case NandEliminate:       out << "NandEliminate";       return out;
   case NorEliminate :       out << "NorEliminate";        return out;
   case SdivEliminate :      out << "SdivEliminate";       return out;
@@ -214,7 +219,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case ExtractBitwise :     out << "ExtractBitwise";      return out;
   case ExtractNot :         out << "ExtractNot";          return out;
   case ExtractArith :       out << "ExtractArith";        return out;
-  case ExtractArith2 :       out << "ExtractArith2";       return out;
+  case ExtractArith2 :      out << "ExtractArith2";       return out;
   case DoubleNeg :          out << "DoubleNeg";           return out;
   case NotConcat :          out << "NotConcat";           return out;
   case NotAnd :             out << "NotAnd";              return out;
@@ -226,7 +231,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case BitwiseNotOr :       out << "BitwiseNotOr";        return out;
   case XorNot :             out << "XorNot";              return out;
   case LtSelf :             out << "LtSelf";              return out;
-  case LteSelf :            out << "LteSelf";              return out;
+  case LteSelf :            out << "LteSelf";             return out;
   case UltZero :            out << "UltZero";             return out;
   case UleZero :            out << "UleZero";             return out;
   case ZeroUle :            out << "ZeroUle";             return out;
@@ -491,7 +496,8 @@ struct AllRewriteRules {
   RewriteRule<BitwiseEq> rule113;
   RewriteRule<UltOne> rule114;
   RewriteRule<SltZero> rule115;
-  
+  RewriteRule<BVToNatEliminate>  rule116;
+  RewriteRule<IntToBVEliminate>  rule117;
 };
 
 template<> inline
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 a5368d2c9..9f3d12415 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -198,8 +198,9 @@ Node RewriteRule<EvalNeg>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUdiv>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
-          utils::isBVGroundTerm(node));
+  return (utils::isBVGroundTerm(node) &&
+          (node.getKind() == kind::BITVECTOR_UDIV_TOTAL ||
+           (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst())));
 }
 
 template<> inline
@@ -213,8 +214,9 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUrem>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
-          utils::isBVGroundTerm(node));
+  return (utils::isBVGroundTerm(node) &&
+          (node.getKind() == kind::BITVECTOR_UREM_TOTAL ||
+           (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst())));
 }
 
 template<> inline
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 cf36633fa..b513dbf90 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -231,6 +231,57 @@ Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
 }
 
 template<>
+bool RewriteRule<BVToNatEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_TO_NAT);
+}
+
+template<>
+Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
+
+  const unsigned size = utils::getSize(node[0]);
+  NodeManager* const nm = NodeManager::currentNM();
+  const Node z = nm->mkConst(Rational(0));
+  const Node bvone = nm->mkConst(BitVector(1u, 1u));
+
+  NodeBuilder<> result(kind::PLUS);
+  Integer i = 1;
+  for(unsigned bit = 0; bit < size; ++bit, i *= 2) {
+    Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone);
+    result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
+  }
+
+  return Node(result);
+}
+
+template<>
+bool RewriteRule<IntToBVEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::INT_TO_BITVECTOR);
+}
+
+template<>
+Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
+
+  const unsigned size = node.getOperator().getConst<IntToBitVector>().size;
+  NodeManager* const nm = NodeManager::currentNM();
+  const Node bvzero = nm->mkConst(BitVector(1u, 0u));
+  const Node bvone = nm->mkConst(BitVector(1u, 1u));
+
+  std::vector<Node> v;
+  Integer i = 2;
+  while(v.size() < size) {
+    Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2)));
+    v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
+    i *= 2;
+  }
+
+  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  result.append(v.rbegin(), v.rend());
+  return Node(result);
+}
+
+template<>
 bool RewriteRule<NandEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NAND &&
           node.getNumChildren() == 2);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index d660dde29..ff7d67cb0 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -45,7 +45,9 @@ template<> inline
 Node RewriteRule<ShlByConst>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
-  
+  if (amount == 0) {
+    return node[0]; 
+  }  
   Node a = node[0]; 
   uint32_t size = utils::getSize(a);
   
@@ -59,6 +61,7 @@ Node RewriteRule<ShlByConst>::apply(TNode node) {
   Assert(amount < Integer(1).multiplyByPow2(32));
   
   uint32_t uint32_amount = amount.toUnsignedInt();
+
   Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
   Node right = utils::mkConst(BitVector(uint32_amount, Integer(0))); 
   return utils::mkConcat(left, right); 
@@ -81,6 +84,9 @@ template<> inline
 Node RewriteRule<LshrByConst>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
+  if (amount == 0) {
+    return node[0]; 
+  }  
   
   Node a = node[0]; 
   uint32_t size = utils::getSize(a);
@@ -117,7 +123,10 @@ template<> inline
 Node RewriteRule<AshrByConst>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
-  
+  if (amount == 0) {
+    return node[0]; 
+  }  
+
   Node a = node[0]; 
   uint32_t size = utils::getSize(a);
   Node sign_bit = utils::mkExtract(a, size-1, size-1);
@@ -812,7 +821,9 @@ Node RewriteRule<UdivPow2>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
   Node a = node[0];
   unsigned power = utils::isPow2Const(node[1]) -1;
-
+  if (power == 0) {
+    return a; 
+  }
   Node extract = utils::mkExtract(a, utils::getSize(node) - 1, power);
   Node zeros = utils::mkConst(power, 0);
   
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 7844e5b92..2467ae3f1 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -70,7 +70,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   return res; 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) {
   // reduce common subexpressions on both sides
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUlt>,
@@ -82,7 +82,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule < EvalSlt >
        >::apply(node);
@@ -97,7 +97,7 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
   // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUle>,
       RewriteRule<UleMax>,
@@ -109,7 +109,7 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
   return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule <EvalSle>, 
       RewriteRule <SleEliminate>
@@ -117,7 +117,7 @@ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
   return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<UgtEliminate>
     >::apply(node);
@@ -125,7 +125,7 @@ RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SgtEliminate>
       //RewriteRule<SltEliminate>
@@ -134,7 +134,7 @@ RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<UgeEliminate>
     >::apply(node);
@@ -142,7 +142,7 @@ RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SgeEliminate>
       //      RewriteRule<SleEliminate>
@@ -151,7 +151,7 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){
   Node resultNode = node;
   
   if(RewriteRule<NotXor>::applies(node)) {
@@ -166,7 +166,7 @@ RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
   Node resultNode = node;
 
   if (RewriteRule<ExtractConcat>::applies(node)) {
@@ -206,7 +206,7 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) {
   
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<ConcatFlatten>,
@@ -220,63 +220,70 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) {
    return RewriteResponse(REWRITE_DONE, resultNode);  
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
   Node resultNode = node;
-  
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<AndSimplify>,
-      RewriteRule<BitwiseSlicing>
+      RewriteRule<AndSimplify>
       >::apply(node);
 
-  if (resultNode.getKind() != node.getKind()) {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  if (!prerewrite) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<BitwiseSlicing>
+        >::apply(resultNode);
+  
+    if (resultNode.getKind() != node.getKind()) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
   
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){
   Node resultNode = node;
-
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<OrSimplify>,
-      RewriteRule<BitwiseSlicing>
-    >::apply(node);
+      RewriteRule<OrSimplify>
+      >::apply(node);
 
-  if (resultNode.getKind() != node.getKind()) {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  if (!prerewrite) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<BitwiseSlicing>
+        >::apply(resultNode);
+    
+    if (resultNode.getKind() != node.getKind()) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
   
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) {
   Node resultNode = node;
-
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>, // flatten the expression 
       RewriteRule<XorSimplify>,        // simplify duplicates and constants
       RewriteRule<XorZero>,            // checks if the constant part is zero and eliminates it
       RewriteRule<BitwiseSlicing>
-    >::apply(node);
-
-  // this simplification introduces new terms and might require further
-  // rewriting
-  if (RewriteRule<XorOne>::applies(resultNode)) {
-    resultNode = RewriteRule<XorOne>::run<false> (resultNode);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  }
+      >::apply(node);
 
-  if (resultNode.getKind() != node.getKind()) {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  if (!prerewrite) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<XorOne>, 
+      RewriteRule <BitwiseSlicing>
+        >::apply(resultNode);
+    
+    if (resultNode.getKind() != node.getKind()) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<XnorEliminate>
     >::apply(node);
@@ -284,7 +291,7 @@ RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<NandEliminate>
       >::apply(node);
@@ -292,7 +299,7 @@ RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<NorEliminate>
     >::apply(node);
@@ -300,7 +307,7 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<CompEliminate>
       >::apply(node);
@@ -308,7 +315,7 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
   Node resultNode = node; 
 
   resultNode = LinearRewriteStrategy
@@ -318,7 +325,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
     >::apply(node);
 
   // only apply if every subterm was already rewritten 
-  if (!preregister) {
+  if (!prerewrite) {
     // distributes multiplication by constant over +, - and unary -
     if(RewriteRule<MultDistribConst>::applies(resultNode)) {
       resultNode = RewriteRule<MultDistribConst>::run<false>(resultNode);
@@ -333,23 +340,28 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) {
-  if (preregister) {
-    return RewriteResponse(REWRITE_DONE, node);
+RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
+  Node resultNode = node;
+  if (prerewrite) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<FlattenAssocCommut>
+        >::apply(node);
+    return RewriteResponse(REWRITE_DONE, resultNode);
   }
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>, 
+  
+  resultNode =  LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
       RewriteRule<PlusCombineLikeTerms>
-      // RewriteRule<PlusLiftConcat> 
       >::apply(node);
-  if (resultNode == node) {
-    return RewriteResponse(REWRITE_DONE, resultNode);
-  } else {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+
+  if (node != resultNode) {
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
   }
+  
+  return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
   // return RewriteResponse(REWRITE_DONE, node); 
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SubEliminate>
@@ -358,7 +370,7 @@ RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
   Node resultNode = node; 
   
   resultNode = LinearRewriteStrategy
@@ -372,7 +384,7 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
   
-  if(!preregister) {
+  if(!prerewrite) {
     if (RewriteRule<NegMult>::applies(node)) {
       resultNode = RewriteRule<NegMult>::run<false>(node);
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -382,8 +394,27 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
+RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){
+  Node resultNode = node;
+
+  if(node[1].isConst() && node[1].getConst<BitVector>().getValue() != 0) {
+    return RewriteUdivTotal(node, prerewrite);
+  }
 
-RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){
+  return RewriteResponse(REWRITE_DONE, resultNode); 
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){
+  Node resultNode = node;
+
+  if(node[1].isConst() && node[1].getConst<BitVector>().getValue() != 0) {
+    return RewriteUremTotal(node, prerewrite);
+  }
+
+  return RewriteResponse(REWRITE_DONE, resultNode); 
+}
+
+RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){
   Node resultNode = node;
 
   if(RewriteRule<UdivPow2>::applies(node)) {
@@ -400,7 +431,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister)
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) {
   Node resultNode = node;
 
   if(RewriteRule<UremPow2>::applies(node)) {
@@ -416,7 +447,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister)
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SmodEliminate>
       >::apply(node);
@@ -424,7 +455,7 @@ RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SdivEliminate>
       >::apply(node);
@@ -432,14 +463,14 @@ RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SremEliminate>
        >::apply(node);
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<ShlByConst>::applies(node)) {
     resultNode = RewriteRule<ShlByConst>::run <false> (node);
@@ -454,7 +485,7 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<LshrByConst>::applies(node)) {
     resultNode = RewriteRule<LshrByConst>::run <false> (node);
@@ -469,7 +500,7 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<AshrByConst>::applies(node)) {
     resultNode = RewriteRule<AshrByConst>::run <false> (node);
@@ -485,7 +516,7 @@ RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RepeatEliminate >
     >::apply(node);
@@ -493,7 +524,7 @@ RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<ZeroExtendEliminate >
     >::apply(node);
@@ -501,7 +532,7 @@ RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalSignExtend>
     >::apply(node);
@@ -511,7 +542,7 @@ RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateRightEliminate >
     >::apply(node);
@@ -519,16 +550,32 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregiste
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateLeftEliminate >
-      >::apply(node);
+    >::apply(node);
   
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
-  if (preregister) {
+RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<BVToNatEliminate>
+    >::apply(node);
+
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<IntToBVEliminate>
+    >::apply(node);
+
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {
+  if (prerewrite) {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,
@@ -593,8 +640,8 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus;
   d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub;
   d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg;
-  // d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
-  // d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
+  d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
+  d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
   d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal;
   d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal;
   d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod;
@@ -609,6 +656,9 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend;
   d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight;
   d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
+
+  d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat;
+  d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;
 }
 
 Node TheoryBVRewriter::eliminateBVSDiv(TNode node) {
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 183b5e8d5..def8e24fe 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -78,6 +78,9 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
 
+  static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
+
 public:
 
   static RewriteResponse postRewrite(TNode node);
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 00284e7ae..67dae0cfa 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -29,6 +29,11 @@ class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if (check) {
+      if (n.getConst<BitVector>().getSize() == 0) {
+        throw TypeCheckingExceptionPrivate(n, "constant of size 0");
+      }
+    }
     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
 };
@@ -190,6 +195,29 @@ public:
   }
 };
 
+class BitVectorConversionTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if(n.getKind() == kind::BITVECTOR_TO_NAT) {
+      if(check && !n[0].getType(check).isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+      }
+      return nodeManager->integerType();
+    }
+
+    if(n.getKind() == kind::INT_TO_BITVECTOR) {
+      size_t bvSize = n.getOperator().getConst<IntToBitVector>();
+      if(check && !n[0].getType(check).isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting integer term");
+      }
+      return nodeManager->mkBitVectorType(bvSize);
+    }
+
+    InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+  }
+};
+
 class CardinalityComputer {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 5847bac3e..ab6a615a2 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -357,7 +357,7 @@ inline Node flattenAnd(std::vector<TNode>& queue) {
 }
 
 
-// neeed a better name, this is not technically a ground term 
+// need a better name, this is not technically a ground term 
 inline bool isBVGroundTerm(TNode node) {
   if (node.getNumChildren() == 0) {
     return node.isConst();