From 1d4ad74ca90641bd9165f9a2c019c54cde6e80c1 Mon Sep 17 00:00:00 2001 From: Guy Date: Fri, 1 Jul 2016 14:21:13 -0700 Subject: [PATCH] Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict --- src/proof/bitvector_proof.cpp | 14 ++++++++++++++ src/proof/theory_proof.cpp | 3 ++- 2 files changed, 16 insertions(+), 1 deletion(-) 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& 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; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 473152647..e70cd60b9 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -354,7 +354,8 @@ void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, Node n1 = it->first; Node n2 = it->second; - Assert(theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + Assert(n1.toExpr() == utils::mkFalse() || + theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); std::ostringstream rewriteRule; rewriteRule << ".lrr" << d_assertionToRewrite.size(); -- 2.30.2