2 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index ea9867b0f..295090699 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -164,6 +164,10 @@ AigBitblaster::AigBitblaster()
       solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "AigBitblaster");
       break;
+    case options::SatSolverMode::KISSAT:
+      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
+                                                    "AigBitblaster");
+      break;
     default: CVC4_FATAL() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index bddde4cb7..0ba69c8b8 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -60,6 +60,10 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
       solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "EagerBitblaster");
       break;
+    case options::SatSolverMode::KISSAT:
+      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
+                                                    "EagerBitblaster");
+      break;
     default: Unreachable() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);