Improvement. We missed an unusual case when deciding whether to substitute variables.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1530 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 064fe918b9aadf965ecdb83562b371a588924291..08bb9d061eefb70f27208ef80a963e1164307f3a 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -40,7 +40,7 @@ class SubstitutionMap  : boost::noncopyable
 
        void buildDepends(const ASTNode& n0, const ASTNode& n1);
        void loops_helper(const set<ASTNode>& varsToCheck, set<ASTNode>& visited);
-       bool loops(const ASTNode& n0, const ASTNode& n1);
+        bool loops(const ASTNode& n0, const ASTNode& n1);
 
        int substitutionsLastApplied;
 public:
@@ -153,10 +153,17 @@ public:
                if (e0.GetKind() == SYMBOL)
                {
                        if (CheckSubstitutionMap(e0))
-                               return false; // already in the map.
+                         {
+                           // e0 and e1 might both be variables, e0 is already substituted for,
+                           // but maybe not e1.
+                           if (e1.GetKind() == SYMBOL)
+                              i = -1;
+                            else
+                              return false; // already in the map.
+                         }
 
                        if (loops(e0,e1))
-                               return false; // loops.
+                           return false; // loops.
                }
 
                if (e1.GetKind() == SYMBOL)