1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 102e8b27d..3eaf2c17d 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -42,6 +42,11 @@ void InferProofCons::notifyFact(const InferInfo& ii)
 {
   Trace("strings-ipc-debug")
       << "InferProofCons::notifyFact: " << ii << std::endl;
+  if (d_lazyFactMap.find(ii.d_conc)!=d_lazyFactMap.end())
+  {
+    Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
+    return;
+  }
   std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii);
   d_lazyFactMap.insert(ii.d_conc, iic);
 }