From a58abbe71fb1fc07129ff9c7568ac544145fb57c Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Fri, 1 Jul 2016 16:49:02 -0700
Subject: [PATCH] When proving a lemma, ignore literals that don't belong to
 the theory in question, except for equalties

---
 src/proof/theory_proof.cpp | 14 +++++++++-----
 1 file 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;
-- 
2.30.2