When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties

1 files changed, 9 insertions, 5 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index e70cd60b9..d12b561a6 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -948,11 +948,15 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->ProduceProofs() DONE" << std::endl;
 
   MyPreRegisterVisitor preRegVisitor(th);
-  for( unsigned i=0; i<lemma.size(); i++ ){
-    Node lit = Node::fromExpr( lemma[i] ).negate();
-    Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl;
-    NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit);
-    th->assertFact(lit, false);
+  for (unsigned i=0; i<lemma.size(); i++) {
+    Node strippedLit = (lemma[i].getKind() == kind::NOT) ? lemma[i][0] : lemma[i];
+    if (strippedLit.getKind() == kind::EQUAL ||
+        d_theory->getId() == theory::Theory::theoryOf(strippedLit)) {
+      Node lit = Node::fromExpr( lemma[i] ).negate();
+      Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl;
+      NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit);
+      th->assertFact(lit, false);
+    }
   }
 
   Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->check()" << std::endl;