added model generation to eager bit-blasting and turned abc off by default

1 files changed, 8 insertions, 2 deletions

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index af35c0499..166d43e35 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -24,11 +24,12 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
-EagerBitblastSolver::EagerBitblastSolver()
+EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv)
   : d_assertionSet()
   , d_bitblaster(NULL)
   , d_aigBitblaster(NULL)
   , d_useAig(options::bitvectorAig())
+  , d_bv(bv)
 {}
 
 EagerBitblastSolver::~EagerBitblastSolver() {
@@ -53,7 +54,7 @@ void EagerBitblastSolver::initialize() {
   if (d_useAig) {
     d_aigBitblaster = new AigBitblaster();
   } else {
-    d_bitblaster = new EagerBitblaster();
+    d_bitblaster = new EagerBitblaster(d_bv);
   }
 }
 
@@ -106,3 +107,8 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode> &formulas) {
   }
   return true; 
 }
+
+void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  AlwaysAssert(!d_useAig && d_bitblaster);
+  d_bitblaster->collectModelInfo(m, fullModel); 
+}