1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 16ccc45ec..83c7d212d 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -287,7 +287,8 @@ TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
 
 bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
 {
-  return d_lemmasSent.find(lem) != d_lemmasSent.end();
+  Node rewritten = Rewriter::rewrite(lem);
+  return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
 }
 
 uint32_t TheoryInferenceManager::numSentLemmas() const
@@ -445,11 +446,12 @@ bool TheoryInferenceManager::hasSentFact() const
 
 bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 {
-  if (d_lemmasSent.find(lem) != d_lemmasSent.end())
+  Node rewritten = Rewriter::rewrite(lem);
+  if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
   {
     return false;
   }
-  d_lemmasSent.insert(lem);
+  d_lemmasSent.insert(rewritten);
   return true;
 }