5 files changed, 29 insertions, 8 deletions
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 1f698de0f..669cbe9e0 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -32,4 +32,5 @@ libbv_la_SOURCES = \
 	theory_bv_rewriter.cpp \
 	cd_set_collection.h 
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 60a98e6e5..c86f14398 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -25,6 +25,7 @@
 #include "prop/sat_solver_factory.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv.h"
+#include "theory/bv/options.h"
 
 using namespace std;
 
@@ -98,7 +99,7 @@ void Bitblaster::bbAtom(TNode node) {
   // asserting that the atom is true iff the definition holds
   Node atom_definition = mkNode(kind::IFF, node, atom_bb);
 
-  if (!Options::current()->bitvectorEagerBitblast) {
+  if (!options::bitvectorEagerBitblast()) {
     d_cnfStream->convertAndAssert(atom_definition, true, false);
     d_bitblastedAtoms.insert(node);
   } else {
@@ -150,7 +151,7 @@ Node Bitblaster::bbOptimize(TNode node) {
 /// Public methods
 
 void Bitblaster::addAtom(TNode atom) {
-  if (!Options::current()->bitvectorEagerBitblast) {
+  if (!options::bitvectorEagerBitblast()) {
     d_cnfStream->ensureLiteral(atom);
     SatLiteral lit = d_cnfStream->getLiteral(atom);
     d_satSolver->addMarkerLiteral(lit);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 24d6b300b..b0d04f952 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -20,6 +20,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/bv/bitblaster.h"
+#include "theory/bv/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -57,7 +58,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
 
   //// Eager bit-blasting
-  if (Options::current()->bitvectorEagerBitblast) {
+  if (options::bitvectorEagerBitblast()) {
     for (unsigned i = 0; i < assertions.size(); ++i) {
       TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
       if (atom.getKind() != kind::BITVECTOR_BITOF) {
@@ -105,7 +106,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   }
 
   // solving
-  if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
+  if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
     Assert(!d_bv->inConflict());
     BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
     bool ok = d_bitblaster->solve();
diff --git a/src/theory/bv/options b/src/theory/bv/options
new file mode 100644
index 000000000..72db63c09
--- /dev/null
+++ b/src/theory/bv/options
@@ -0,0 +1,17 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module BV "theory/bv/options.h" Bitvector theory
+
+option bitvectorEagerBitblast --bitblast-eager bool
+ eagerly bitblast the bitvectors to the main SAT solver
+
+option bitvectorShareLemmas --bitblast-share-lemmas bool
+ share lemmas from the bitblasting solver with the main solver
+
+option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
+ check the bitblasting eagerly
+
+endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index da2dd77f6..b6dcc6662 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/valuation.h"
 #include "theory/bv/bitblaster.h"
+#include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 
 using namespace CVC4;
@@ -69,7 +70,7 @@ TheoryBV::Statistics::~Statistics() {
 void TheoryBV::preRegisterTerm(TNode node) {
   BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
-  if (Options::current()->bitvectorEagerBitblast) {
+  if (options::bitvectorEagerBitblast()) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
@@ -261,7 +262,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::current()->bitvectorEagerBitblast && d_useEqualityEngine) {
+  if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
     d_equalitySolver.addSharedTerm(t);
   }
 }
@@ -269,7 +270,7 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  if (Options::current()->bitvectorEagerBitblast) {
+  if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }