diff options
author | Guy <katz911@gmail.com> | 2016-07-01 14:21:13 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-01 14:21:13 -0700 |
commit | 1d4ad74ca90641bd9165f9a2c019c54cde6e80c1 (patch) | |
tree | f6d1db1ca667a9c0e70b4a8f8b655e1a92a08627 /src/proof/bitvector_proof.cpp | |
parent | e252f83e7298fdbad1ac8882763e7571e7a83235 (diff) |
Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 171085d7f..f557d5063 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -605,6 +605,20 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os } } + // We failed to find a matching sub conflict. The last hope is that the + // conflict has a FALSE assertion in it; this can happen in some corner cases, + // where the FALSE is the result of a rewrite. + + for (unsigned i = 0; i < lemma.size(); ++i) { + if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) { + Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; + os << "(clausify_false "; + os << ProofManager::getLitName(lemma[i]); + os << ")"; + return; + } + } + Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl << "Dumping existing conflicts:" << std::endl; |