Index: src/ResolvExpr/SatisfyAssertions.cpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.cpp	(revision 0c840fc175421beff77fdd02802dd0b5c1da973c)
+++ src/ResolvExpr/SatisfyAssertions.cpp	(revision 34b42682a27d035cf271583e53b685bd4ba02119)
@@ -452,7 +452,7 @@
 			for (unsigned resetCount = 0; ; ++resetCount) {
 				ast::AssertionList next;
-				resetTyVarRenaming();
 				// make initial pass at matching assertions
 				for ( auto & assn : sat.need ) {
+					resetTyVarRenaming();
 					// fail early if any assertion is not satisfiable
 					auto result = satisfyAssertion( assn, sat, !next.empty() );