Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 466149ddfc7aec2d46cbff0b24e228964a48a7aa)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 22cad76794e5f8af3acf12849043146f8d4538c4)
@@ -411,6 +411,6 @@
 	}
 
-	/// Map of declarations (intended to be the assertions in an AssertionSet) to their parents and the number of times they've been included
-	typedef std::unordered_map< DeclarationWithType*, std::unordered_map< DeclarationWithType*, unsigned > > AssertionParentSet;
+	/// Map of declaration uniqueIds (intended to be the assertions in an AssertionSet) to their parents and the number of times they've been included
+	typedef std::unordered_map< UniqueId, std::unordered_map< UniqueId, unsigned > > AssertionParentSet;
 	
 	static const int recursionLimit = 10;  ///< Limit to depth of recursion satisfaction
@@ -464,7 +464,4 @@
 				std::cerr << std::endl;
 			)
-			AssertionParentSet newNeedParents( needParents );
-			// skip repeatingly-self-recursive assertion satisfaction
-			if ( newNeedParents[ curDecl ][ *candidate ]++ > recursionParentLimit ) return;
 			
 			AssertionSet newHave, newerNeed( newNeed );
@@ -490,5 +487,9 @@
 				newerAlt.env = newEnv;
 				assert( (*candidate)->get_uniqueId() );
-				Expression *varExpr = new VariableExpr( static_cast< DeclarationWithType* >( Declaration::declFromId( (*candidate)->get_uniqueId() ) ) );
+				DeclarationWithType *candDecl = static_cast< DeclarationWithType* >( Declaration::declFromId( (*candidate)->get_uniqueId() ) );
+				AssertionParentSet newNeedParents( needParents );
+				// skip repeatingly-self-recursive assertion satisfaction
+				if ( newNeedParents[ curDecl->get_uniqueId() ][ candDecl->get_uniqueId() ]++ > recursionParentLimit ) continue;
+				Expression *varExpr = new VariableExpr( candDecl );
 				deleteAll( varExpr->get_results() );
 				varExpr->get_results().clear();