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 /src/theory/bv | |
| parent | d9533928947a207b795d90a97879b8212e99c50e (diff) | |
Fix AIG bitblaster for unsat cores.
Diffstat (limited to 'src/theory/bv')
| -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); } } |