From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 26 Sep 2014 11:25:47 +0000 (-0400)
Subject: Fix AIG bitblaster for unsat cores.
X-Git-Tag: cvc5-1.0.0~6617
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba9d9d0cfab0e23aa2bb11ff4f9cd7b20550a97b;p=cvc5.git

Fix AIG bitblaster for unsat cores.
---

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index ce775874f..6270995ef 100644
--- 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);
   }
 }