Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision 3cd5fdde9ed74eb5131706e7f87dc45dcdd63a34)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision d3b2c32a655466c4084655c0fb259f5b8b1d0eb5)
@@ -342,5 +342,7 @@
 
 	/// Limit to depth of recursion of assertion satisfaction
-	static const int recursionLimit = /* 10 */ 4;
+	static const int recursionLimit = 4;
+	/// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
+	static const int deferLimit = 10;
 
 	void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out, std::list<std::string>& errors ) {
@@ -369,6 +371,6 @@
 						ss << tabs << "Unsatisfiable alternative:\n";
 						resn.alt.print( ss, ++tabs );
-						ss << --tabs << "Could not satisfy assertion:\n";
-						assn.decl->print( ss, ++tabs );
+						ss << (tabs-1) << "Could not satisfy assertion:\n";
+						assn.decl->print( ss, tabs );
 						
 						errors.emplace_back( ss.str() );
@@ -384,4 +386,18 @@
 						new_resns.emplace_back( std::move(resn), IterateState );
 					}
+				} else if ( resn.deferred.size() > deferLimit ) {
+					// too many deferred assertions to attempt mutual compatibility
+					Indenter tabs{ 3 };
+					std::ostringstream ss;
+					ss << tabs << "Unsatisfiable alternative:\n";
+					resn.alt.print( ss, ++tabs );
+					ss << (tabs-1) << "Too many non-unique satisfying assignments for "
+						"assertions:\n";
+					for ( const auto& d : resn.deferred ) {
+						d.decl->print( ss, tabs );
+					}
+
+					errors.emplace_back( ss.str() );
+					goto nextResn;
 				} else {
 					// resolve deferred assertions by mutual compatibility
@@ -395,6 +411,5 @@
 						ss << tabs << "Unsatisfiable alternative:\n";
 						resn.alt.print( ss, ++tabs );
-						ss << --tabs << "No mutually-compatible satisfaction for assertions:\n";
-						++tabs;
+						ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
 						for ( const auto& d : resn.deferred ) {
 							d.decl->print( ss, tabs );