Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 2de162daa1fcda58a389901441ff013e4fda051a)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision ebf5689b72f9bf111b7bb9c1c8b3c47899528e7f)
@@ -19,4 +19,7 @@
 #include <functional>
 #include <cassert>
+#include <unordered_map>
+#include <utility>
+#include <vector>
 
 #include "AlternativeFinder.h"
@@ -408,5 +411,9 @@
 	}
 
-	static const int recursionLimit = 10;
+	/// 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;
+	
+	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
 
 	void addToIndexer( AssertionSet &assertSet, SymTab::Indexer &indexer ) {
@@ -417,7 +424,8 @@
 		}
 	}
-
+	
 	template< typename ForwardIterator, typename OutputIterator >
-	void inferRecursive( ForwardIterator begin, ForwardIterator end, const Alternative &newAlt, OpenVarSet &openVars, const SymTab::Indexer &decls, const AssertionSet &newNeed, int level, const SymTab::Indexer &indexer, OutputIterator out ) {
+	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 ) {
 			if ( newNeed.empty() ) {
@@ -432,5 +440,5 @@
 					printAssertionSet( newNeed, std::cerr, 8 );
 				)
-				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, level+1, indexer, out );
+				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, needParents, level+1, indexer, out );
 				return;
 			}
@@ -439,5 +447,5 @@
 		ForwardIterator cur = begin++;
 		if ( ! cur->second ) {
-			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, level, indexer, out );
+			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, needParents, level, indexer, out );
 		}
 		DeclarationWithType *curDecl = cur->first;
@@ -456,4 +464,8 @@
 				std::cerr << std::endl;
 			)
+			AssertionParentSet newNeedParents( needParents );
+			// skip repeatingly-self-recursive assertion satisfaction
+			if ( needParents[ curDecl ][ *candidate ]++ > recursionParentLimit ) return;
+			
 			AssertionSet newHave, newerNeed( newNeed );
 			TypeEnvironment newEnv( newAlt.env );
@@ -492,5 +504,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, level, indexer, out );
+				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, newNeedParents, level, indexer, out );
 			} else {
 				delete adjType;
@@ -514,5 +526,6 @@
 		addToIndexer( have, decls );
 		AssertionSet newNeed;
-		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, 0, indexer, out );
+		AssertionParentSet needParents;
+		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, needParents, 0, indexer, out );
 //	PRINT(
 //	    std::cerr << "declaration 14 is ";