From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 26 May 2016 22:19:51 +0000 (-0400)
Subject: Fix for aig_bitblaster.cpp
X-Git-Tag: cvc5-1.0.0~6049^2~30^2~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dcb73e70575406db5ef94eb48a9ad5b2bdf7b31a;p=cvc5.git

Fix for aig_bitblaster.cpp
---

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 80a9396ac..098582433 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -19,7 +19,7 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
-
+#include "smt/smt_statistics_registry.h"
 
 #ifdef CVC4_USE_ABC
 // Function is defined as static in ABC. Not sure how else to do this. 
@@ -140,23 +140,10 @@ AigBitblaster::AigBitblaster()
   , d_bbAtoms()
   , d_aigOutputNode(NULL)
 {
-  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");
-  }
+  d_nullContext = new context::Context(); 
+  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, smtStatisticsRegistry(), "AigBitblaster");
+  MinisatEmptyNotify* notify = new MinisatEmptyNotify();
+  d_satSolver->setNotify(notify);
 }
 
 AigBitblaster::~AigBitblaster() {
@@ -415,7 +402,7 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
       prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); 
       clause.push_back(lit); 
     }
-    d_satSolver->addClause(clause, false, RULE_INVALID);
+    d_satSolver->addClause(clause, false);
   }
 }