Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 22cad76794e5f8af3acf12849043146f8d4538c4)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 89b686a4ac22722b03a7db23b65b5685e881a672)
@@ -411,9 +411,9 @@
 	}
 
-	/// 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;
+	// /// 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
-	static const unsigned recursionParentLimit = 1;  ///< Limit to the number of times an assertion can recursively use itself
+	static const int recursionLimit = /*10*/ 3;  ///< Limit to depth of recursion satisfaction
+	//static const unsigned recursionParentLimit = 1;  ///< Limit to the number of times an assertion can recursively use itself
 
 	void addToIndexer( AssertionSet &assertSet, SymTab::Indexer &indexer ) {
@@ -426,5 +426,5 @@
 	
 	template< typename ForwardIterator, typename OutputIterator >
-	void inferRecursive( ForwardIterator begin, ForwardIterator end, const Alternative &newAlt, OpenVarSet &openVars, const SymTab::Indexer &decls, const AssertionSet &newNeed, const AssertionParentSet &needParents, 
+	void inferRecursive( ForwardIterator begin, ForwardIterator end, const Alternative &newAlt, OpenVarSet &openVars, const SymTab::Indexer &decls, const AssertionSet &newNeed, /*const AssertionParentSet &needParents,*/ 
 						 int level, const SymTab::Indexer &indexer, OutputIterator out ) {
 		if ( begin == end ) {
@@ -440,5 +440,5 @@
 					printAssertionSet( newNeed, std::cerr, 8 );
 				)
-				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, needParents, level+1, indexer, out );
+				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, /*needParents,*/ level+1, indexer, out );
 				return;
 			}
@@ -447,5 +447,5 @@
 		ForwardIterator cur = begin++;
 		if ( ! cur->second ) {
-			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, needParents, level, indexer, out );
+			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, /*needParents,*/ level, indexer, out );
 		}
 		DeclarationWithType *curDecl = cur->first;
@@ -488,7 +488,8 @@
 				assert( (*candidate)->get_uniqueId() );
 				DeclarationWithType *candDecl = static_cast< DeclarationWithType* >( Declaration::declFromId( (*candidate)->get_uniqueId() ) );
-				AssertionParentSet newNeedParents( needParents );
+				//AssertionParentSet newNeedParents( needParents );
 				// skip repeatingly-self-recursive assertion satisfaction
-				if ( newNeedParents[ curDecl->get_uniqueId() ][ candDecl->get_uniqueId() ]++ > recursionParentLimit ) continue;
+				// DOESN'T WORK: grandchild nodes conflict with their cousins
+				//if ( newNeedParents[ curDecl->get_uniqueId() ][ candDecl->get_uniqueId() ]++ > recursionParentLimit ) continue;
 				Expression *varExpr = new VariableExpr( candDecl );
 				deleteAll( varExpr->get_results() );
@@ -505,5 +506,5 @@
 				// XXX: this is a memory leak, but adjType can't be deleted because it might contain assertions
 				appExpr->get_inferParams()[ curDecl->get_uniqueId() ] = ParamEntry( (*candidate)->get_uniqueId(), adjType->clone(), curDecl->get_type()->clone(), varExpr );
-				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, newNeedParents, level, indexer, out );
+				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, /*newNeedParents,*/ level, indexer, out );
 			} else {
 				delete adjType;
@@ -527,6 +528,6 @@
 		addToIndexer( have, decls );
 		AssertionSet newNeed;
-		AssertionParentSet needParents;
-		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, needParents, 0, indexer, out );
+		//AssertionParentSet needParents;
+		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, /*needParents,*/ 0, indexer, out );
 //	PRINT(
 //	    std::cerr << "declaration 14 is ";