diff options
Diffstat (limited to 'src/theory/bv/bitblast/lazy_bitblaster.cpp')
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 7f38c61a2..f3adc4b21 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -416,9 +416,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { lemmab << d_cnf->getNode(clause[i]); } Node lemma = lemmab; - d_bv->d_inferManager.lemma(lemma); + d_bv->d_inferManager.lemma(lemma, InferenceId::UNKNOWN); } else { - d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0])); + d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]), InferenceId::UNKNOWN); } } |