Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict

2 files changed, 16 insertions, 1 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;
 
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();