From 3dacabb2a08a43c9bc01067208623d460a1eed89 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 12 Mar 2012 04:04:57 +0000
Subject: [PATCH] Improvements. Better preventing infinite loops when rewriting
 replacements through.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1588 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/SubstitutionMap.cpp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 9eea3e9..1f78584 100644
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -107,9 +107,19 @@ namespace BEEV
       {
       const ASTNode& r = it->second;
       assert(r.GetIndexWidth() == n.GetIndexWidth());
+
+      if (preventInfinite)
+        cache.insert(make_pair(n, r));
+
       ASTNode replaced = replace(r, fromTo, cache, nf, stopAtArrays, preventInfinite);
       if (replaced != r)
-        fromTo[n] = replaced;
+        {
+          fromTo.erase(n);
+          fromTo[n] = replaced;
+        }
+
+      if (preventInfinite)
+        cache.erase(n);
 
       cache.insert(make_pair(n, replaced));
       return replaced;
-- 
2.47.3