From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 28 Jan 2012 02:18:09 +0000 (+0000)
Subject: Improvement. We missed an unusual case when deciding whether to substitute variables.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d039de4aee4be62a69aff9d1d994bedcda9982b2;p=francis%2Fstp.git

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 064fe91..08bb9d0 100644
--- 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)