Merged cryptominisat from experimental branch.

1 files changed, 17 insertions, 4 deletions

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 887daa1bd..80a9396ac 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -140,10 +140,23 @@ AigBitblaster::AigBitblaster()
   , d_bbAtoms()
   , d_aigOutputNode(NULL)
 {
-  d_nullContext = new context::Context(); 
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster");
-  MinisatEmptyNotify* notify = new MinisatEmptyNotify();
-  d_satSolver->setNotify(notify);
+  d_nullContext = new context::Context();
+  switch(options::bvSatSolver()) {
+  case SAT_SOLVER_MINISAT: {
+    prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext,
+										"AigBitblaster");
+    MinisatEmptyNotify* notify = new MinisatEmptyNotify();
+    minisat->setNotify(notify);
+    d_satSolver = minisat;
+    break;
+  }
+  case SAT_SOLVER_CRYPTOMINISAT:
+    d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
+                                                              "AigBitblaster");
+    break;
+  default:
+    Unreachable("Unknown SAT solver type");
+  }
 }
 
 AigBitblaster::~AigBitblaster() {