diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-26 07:25:47 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-26 07:25:47 -0400 |
commit | ba9d9d0cfab0e23aa2bb11ff4f9cd7b20550a97b (patch) | |
tree | 42226500a8f92a112af19ac15ade733c928c58b8 | |
parent | d9533928947a207b795d90a97879b8212e99c50e (diff) |
Fix AIG bitblaster for unsat cores.
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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); } } |