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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 9eea3e908992018af579fc4479355afa07444ed4..1f785843acf28d52696d3bd755bf95f990204063 100644 (file)
--- 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;