Handle bitvector lemmas where a literal gets rewritten into false, and consequently...

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 171085d7ffc2b3a19cdef8dd9272dbc8899007ec..f557d506317e55626cd8a3c437c827a6d23471b2 100644 (file)
--- 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;
 

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 4731526471b82018b385f0e513768fdec28285f5..e70cd60b9fd6993599300aaebf7c7bcfae3382e7 100644 (file)
--- 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();