Fix AIG bitblaster for unsat cores.

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index ce775874f16e53e0e4db99d9c52b5bae31e243ca..6270995eff5df2e81f5542025ced34000fe48690 100644 (file)
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -402,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); 
+    d_satSolver->addClause(clause, false, RULE_INVALID);
   }
 }