Index: src/ResolvExpr/Alternative.cc
===================================================================
--- src/ResolvExpr/Alternative.cc	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/Alternative.cc	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -9,7 +9,7 @@
 // Author           : Richard C. Bilson
 // Created On       : Sat May 16 23:44:23 2015
-// Last Modified By : Peter A. Buhr
-// Last Modified On : Sat May 16 23:54:23 2015
-// Update Count     : 2
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Thu Oct 11 10:55:00 2018
+// Update Count     : 3
 //
 
@@ -27,14 +27,28 @@
 
 namespace ResolvExpr {
-	Alternative::Alternative() : cost( Cost::zero ), cvtCost( Cost::zero ), expr( nullptr ) {}
+	Alternative::Alternative() 
+	: cost( Cost::zero ), cvtCost( Cost::zero ), expr( nullptr ), env(), openVars(), need() {}
 
-	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, const Cost& cost )
-		: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( env ) {}
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env )
+	: cost( Cost::zero ), cvtCost( Cost::zero ), expr( expr ), env( env ), openVars(), need() {}
+	
+	Alternative::Alternative( const Alternative &o, Expression *expr, const Cost &cost ) 
+	: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( o.env ), openVars( o.openVars ), 
+	  need( o.need ) {}
 
-	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, const Cost& cost, const Cost &cvtCost )
-		: cost( cost ), cvtCost( cvtCost ), expr( expr ), env( env ) {}
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, 
+		const OpenVarSet& openVars, const AssertionList& need, const Cost& cost )
+	: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( env ), openVars( openVars ), 
+	  need( need ) {}
 
-	Alternative::Alternative( const Alternative &other ) : cost( other.cost ), cvtCost( other.cvtCost ), expr( maybeClone( other.expr ) ), env( other.env ) {
-	}
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, 
+		const OpenVarSet& openVars, const AssertionList& need, const Cost& cost, 
+		const Cost &cvtCost )
+	: cost( cost ), cvtCost( cvtCost ), expr( expr ), env( env ), openVars( openVars ), 
+	  need( need ) {}
+
+	Alternative::Alternative( const Alternative &other ) 
+	: cost( other.cost ), cvtCost( other.cvtCost ), expr( maybeClone( other.expr ) ), 
+	  env( other.env ), openVars( other.openVars ), need( other.need ) {}
 
 	Alternative &Alternative::operator=( const Alternative &other ) {
@@ -45,8 +59,13 @@
 		expr = maybeClone( other.expr );
 		env = other.env;
+		openVars = other.openVars;
+		need = other.need;
 		return *this;
 	}
 
-	Alternative::Alternative( Alternative && other ) : cost( other.cost ), cvtCost( other.cvtCost ), expr( other.expr ), env( std::move( other.env ) ) {
+	Alternative::Alternative( Alternative && other ) 
+	: cost( other.cost ), cvtCost( other.cvtCost ), expr( other.expr ), 
+	  env( std::move( other.env ) ), openVars( std::move( other.openVars ) ), 
+	  need( std::move( other.need ) ) {
 		other.expr = nullptr;
 	}
@@ -59,4 +78,6 @@
 		expr = other.expr;
 		env = std::move( other.env );
+		openVars = std::move( other.openVars );
+		need = std::move( other.need );
 		other.expr = nullptr;
 		return *this;
Index: src/ResolvExpr/Alternative.h
===================================================================
--- src/ResolvExpr/Alternative.h	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/Alternative.h	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -9,7 +9,7 @@
 // Author           : Richard C. Bilson
 // Created On       : Sat May 16 23:45:43 2015
-// Last Modified By : Peter A. Buhr
-// Last Modified On : Sat Jul 22 09:36:36 2017
-// Update Count     : 3
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Thu Oct 11 10:55:00 2018
+// Update Count     : 4
 //
 
@@ -20,13 +20,32 @@
 
 #include "Cost.h"             // for Cost
-#include "TypeEnvironment.h"  // for TypeEnvironment
+#include "TypeEnvironment.h"  // for TypeEnvironment, AssertionSetValue
 
 class Expression;
 
 namespace ResolvExpr {
+	/// One assertion to resolve
+	struct AssertionItem {
+		DeclarationWithType* decl;
+		AssertionSetValue info;
+		
+		AssertionItem() = default;
+		AssertionItem( DeclarationWithType* decl, const AssertionSetValue& info ) 
+		: decl(decl), info(info) {}
+		AssertionItem( const AssertionSet::value_type& e ) : decl(e.first), info(e.second) {}
+		operator AssertionSet::value_type () const { return { decl, info }; }
+	};
+	/// A list of unresolved assertions
+	using AssertionList = std::vector<AssertionItem>;
+
+	/// One option for resolution of an expression
 	struct Alternative {
 		Alternative();
-		Alternative( Expression *expr, const TypeEnvironment &env, const Cost &cost );
-		Alternative( Expression *expr, const TypeEnvironment &env, const Cost &cost, const Cost &cvtCost );
+		Alternative( Expression *expr, const TypeEnvironment &env );
+		Alternative( const Alternative &o, Expression *expr, const Cost &cost );
+		Alternative( Expression *expr, const TypeEnvironment &env, const OpenVarSet& openVars, 
+			const AssertionList& need, const Cost &cost );
+		Alternative( Expression *expr, const TypeEnvironment &env, const OpenVarSet& openVars, 
+			const AssertionList& need, const Cost &cost, const Cost &cvtCost );
 		Alternative( const Alternative &other );
 		Alternative &operator=( const Alternative &other );
@@ -44,8 +63,13 @@
 		}
 
-		Cost cost;
-		Cost cvtCost;
-		Expression *expr;
-		TypeEnvironment env;
+		/// Sorts by cost
+		bool operator< ( const Alternative& o ) const { return cost < o.cost; }
+
+		Cost cost;            ///< Cost of the whole expression
+		Cost cvtCost;         ///< Cost of conversions to the satisfying expression
+		Expression *expr;     ///< Satisfying expression
+		TypeEnvironment env;  ///< Containing type environment
+		OpenVarSet openVars;  ///< Open variables for environment
+		AssertionList need;   ///< Assertions which need to be resolved
 	};
 
Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -34,4 +34,5 @@
 #include "InitTweak/InitTweak.h"   // for getFunctionName
 #include "RenameVars.h"            // for RenameVars, global_renamer
+#include "ResolveAssertions.h"     // for resolveAssertions
 #include "ResolveTypeof.h"         // for resolveTypeof
 #include "Resolver.h"              // for resolveStmtExpr
@@ -102,7 +103,7 @@
 		void addAnonConversions( const Alternative & alt );
 		/// Adds alternatives for member expressions, given the aggregate, conversion cost for that aggregate, and name of the member
-		template< typename StructOrUnionType > void addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Cost &newCost, const TypeEnvironment & env, const std::string & name );
+		template< typename StructOrUnionType > void addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Alternative &alt, const Cost &newCost, const std::string & name );
 		/// Adds alternatives for member expressions where the left side has tuple type
-		void addTupleMembers( TupleType * tupleType, Expression *expr, const Cost &newCost, const TypeEnvironment & env, Expression * member );
+		void addTupleMembers( TupleType *tupleType, Expression *expr, const Alternative &alt, const Cost &newCost, Expression *member );
 		/// Adds alternatives for offsetof expressions, given the base type and name of the member
 		template< typename StructOrUnionType > void addOffsetof( StructOrUnionType *aggInst, const std::string &name );
@@ -253,4 +254,21 @@
 			SemanticError( expr, "No reasonable alternatives for expression " );
 		}
+		if ( mode.resolveAssns ) {
+			// trim candidates just to those where the assertions resolve
+			AltList candidates;
+			for ( unsigned i = 0; i < alternatives.size(); ++i ) {
+				resolveAssertions( alternatives[i], indexer, candidates );
+			}
+			// fail early if none such
+			if ( mode.failFast && candidates.empty() ) {
+				std::ostringstream stream;
+				stream << "No resolvable alternatives for expression " << expr << "\n"
+				       << "Alternatives with failing assertions are:\n";
+				printAlts( alternatives, stream, 1 );
+				SemanticError( expr->location, stream.str() );
+			}
+			// reset alternatives
+			alternatives = std::move( candidates );
+		}
 		if ( mode.prune ) {
 			auto oldsize = alternatives.size();
@@ -317,12 +335,12 @@
 
 		if ( StructInstType *structInst = dynamic_cast< StructInstType* >( aggrExpr->result ) ) {
-			addAggMembers( structInst, aggrExpr.get(), alt.cost+Cost::safe, alt.env, "" );
+			addAggMembers( structInst, aggrExpr.get(), alt, alt.cost+Cost::safe, "" );
 		} else if ( UnionInstType *unionInst = dynamic_cast< UnionInstType* >( aggrExpr->result ) ) {
-			addAggMembers( unionInst, aggrExpr.get(), alt.cost+Cost::safe, alt.env, "" );
+			addAggMembers( unionInst, aggrExpr.get(), alt, alt.cost+Cost::safe, "" );
 		} // if
 	}
 
 	template< typename StructOrUnionType >
-	void AlternativeFinder::Finder::addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Cost &newCost, const TypeEnvironment & env, const std::string & name ) {
+	void AlternativeFinder::Finder::addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Alternative& alt, const Cost &newCost, const std::string & name ) {
 		std::list< Declaration* > members;
 		aggInst->lookup( name, members );
@@ -332,5 +350,5 @@
 				// addAnonAlternatives uses vector::push_back, which invalidates references to existing elements, so
 				// can't construct in place and use vector::back
-				Alternative newAlt( new MemberExpr( dwt, expr->clone() ), env, newCost );
+				Alternative newAlt{ alt, new MemberExpr{ dwt, expr->clone() }, newCost };
 				renameTypes( newAlt.expr );
 				addAnonConversions( newAlt ); // add anonymous member interpretations whenever an aggregate value type is seen as a member expression.
@@ -342,5 +360,5 @@
 	}
 
-	void AlternativeFinder::Finder::addTupleMembers( TupleType * tupleType, Expression *expr, const Cost &newCost, const TypeEnvironment & env, Expression * member ) {
+	void AlternativeFinder::Finder::addTupleMembers( TupleType *tupleType, Expression *expr, 			const Alternative &alt, const Cost &newCost, Expression *member ) {
 		if ( ConstantExpr * constantExpr = dynamic_cast< ConstantExpr * >( member ) ) {
 			// get the value of the constant expression as an int, must be between 0 and the length of the tuple type to have meaning
@@ -348,5 +366,6 @@
 			std::string tmp;
 			if ( val >= 0 && (unsigned long long)val < tupleType->size() ) {
-				alternatives.push_back( Alternative( new TupleIndexExpr( expr->clone(), val ), env, newCost ) );
+				alternatives.push_back( Alternative{ 
+					alt, new TupleIndexExpr( expr->clone(), val ), newCost } );
 			} // if
 		} // if
@@ -354,5 +373,5 @@
 
 	void AlternativeFinder::Finder::postvisit( ApplicationExpr *applicationExpr ) {
-		alternatives.push_back( Alternative( applicationExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ applicationExpr->clone(), env } );
 	}
 
@@ -484,145 +503,123 @@
 	}
 
-	static const int recursionLimit = /*10*/ 4;  ///< Limit to depth of recursion satisfaction
-
-	void addToIndexer( AssertionSet &assertSet, SymTab::Indexer &indexer ) {
-		for ( AssertionSet::iterator i = assertSet.begin(); i != assertSet.end(); ++i ) {
-			if ( i->second.isUsed ) {
-				indexer.addId( i->first );
-			}
-		}
-	}
-
-	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 ) {
-		if ( newAlt.cost == Cost::infinity ) return; // don't proceed down this dead end
-		if ( begin == end ) {
-			if ( newNeed.empty() ) {
-				PRINT(
-					std::cerr << "all assertions satisfied, output alternative: ";
-					newAlt.print( std::cerr );
-					std::cerr << std::endl;
-				);
-				*out++ = newAlt;
-				return;
-			} else if ( level >= recursionLimit ) {
-				SemanticError( newAlt.expr->location, "Too many recursive assertions" );
-			} else {
-				AssertionSet newerNeed;
-				PRINT(
-					std::cerr << "recursing with new set:" << std::endl;
-					printAssertionSet( newNeed, std::cerr, 8 );
-				)
-				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, level+1, indexer, out );
-				return;
-			}
-		}
-
-		ForwardIterator cur = begin++;
-		if ( ! cur->second.isUsed ) {
-			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, level, indexer, out );
-			return; // xxx - should this continue? previously this wasn't here, and it looks like it should be
-		}
-		DeclarationWithType *curDecl = cur->first;
-
-		PRINT(
-			std::cerr << "inferRecursive: assertion is ";
-			curDecl->print( std::cerr );
-			std::cerr << std::endl;
-		)
-		std::list< SymTab::Indexer::IdData > candidates;
-		decls.lookupId( curDecl->get_name(), candidates );
-///   if ( candidates.empty() ) { std::cerr << "no candidates!" << std::endl; }
-		for ( const auto & data : candidates ) {
-			DeclarationWithType * candidate = data.id;
-			PRINT(
-				std::cerr << "inferRecursive: candidate is ";
-				candidate->print( std::cerr );
-				std::cerr << std::endl;
-			)
-
-			AssertionSet newHave, newerNeed( newNeed );
-			TypeEnvironment newEnv( newAlt.env );
-			OpenVarSet newOpenVars( openVars );
-			Type *adjType = candidate->get_type()->clone();
-			adjustExprType( adjType, newEnv, indexer );
-			renameTyVars( adjType );
-			PRINT(
-				std::cerr << "unifying ";
-				curDecl->get_type()->print( std::cerr );
-				std::cerr << " with ";
-				adjType->print( std::cerr );
-				std::cerr << std::endl;
-			)
-			if ( unify( curDecl->get_type(), adjType, newEnv, newerNeed, newHave, newOpenVars, indexer ) ) {
-				PRINT(
-					std::cerr << "success!" << std::endl;
-				)
-				SymTab::Indexer newDecls( decls );
-				addToIndexer( newHave, newDecls );
-				Alternative newerAlt( newAlt );
-				newerAlt.env = newEnv;
-				assertf( candidate->get_uniqueId(), "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
-
-				// everything with an empty idChain was pulled in by the current assertion.
-				// add current assertion's idChain + current assertion's ID so that the correct inferParameters can be found.
-				for ( auto & a : newerNeed ) {
-					if ( a.second.idChain.empty() ) {
-						a.second.idChain = cur->second.idChain;
-						a.second.idChain.push_back( curDecl->get_uniqueId() );
-					}
-				}
-
-				Expression *varExpr = data.combine( newerAlt.cvtCost );
-				delete varExpr->get_result();
-				varExpr->set_result( adjType->clone() );
-				PRINT(
-					std::cerr << "satisfying assertion " << curDecl->get_uniqueId() << " ";
-					curDecl->print( std::cerr );
-					std::cerr << " with declaration " << candidate->get_uniqueId() << " ";
-					candidate->print( std::cerr );
-					std::cerr << std::endl;
-				)
-				// follow the current assertion's ID chain to find the correct set of inferred parameters to add the candidate to (i.e. the set of inferred parameters belonging to the entity which requested the assertion parameter).
-				InferredParams * inferParameters = &newerAlt.expr->get_inferParams();
-				for ( UniqueId id : cur->second.idChain ) {
-					inferParameters = (*inferParameters)[ id ].inferParams.get();
-				}
-				// XXX: this is a memory leak, but adjType can't be deleted because it might contain assertions
-				(*inferParameters)[ curDecl->get_uniqueId() ] = ParamEntry( candidate->get_uniqueId(), adjType->clone(), curDecl->get_type()->clone(), varExpr );
-				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, level, indexer, out );
-			} else {
-				delete adjType;
-			}
-		}
-	}
+// 	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 ) {
+// 		if ( newAlt.cost == Cost::infinity ) return; // don't proceed down this dead end
+// 		if ( begin == end ) {
+// 			if ( newNeed.empty() ) {
+// 				PRINT(
+// 					std::cerr << "all assertions satisfied, output alternative: ";
+// 					newAlt.print( std::cerr );
+// 					std::cerr << std::endl;
+// 				);
+// 				*out++ = newAlt;
+// 				return;
+// 			} else if ( level >= recursionLimit ) {
+// 				SemanticError( newAlt.expr->location, "Too many recursive assertions" );
+// 			} else {
+// 				AssertionSet newerNeed;
+// 				PRINT(
+// 					std::cerr << "recursing with new set:" << std::endl;
+// 					printAssertionSet( newNeed, std::cerr, 8 );
+// 				)
+// 				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, level+1, indexer, out );
+// 				return;
+// 			}
+// 		}
+
+// 		ForwardIterator cur = begin++;
+// 		if ( ! cur->second.isUsed ) {
+// 			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, level, indexer, out );
+// 			return; // xxx - should this continue? previously this wasn't here, and it looks like it should be
+// 		}
+// 		DeclarationWithType *curDecl = cur->first;
+
+// 		PRINT(
+// 			std::cerr << "inferRecursive: assertion is ";
+// 			curDecl->print( std::cerr );
+// 			std::cerr << std::endl;
+// 		)
+// 		std::list< SymTab::Indexer::IdData > candidates;
+// 		decls.lookupId( curDecl->get_name(), candidates );
+// ///   if ( candidates.empty() ) { std::cerr << "no candidates!" << std::endl; }
+// 		for ( const auto & data : candidates ) {
+// 			DeclarationWithType * candidate = data.id;
+// 			PRINT(
+// 				std::cerr << "inferRecursive: candidate is ";
+// 				candidate->print( std::cerr );
+// 				std::cerr << std::endl;
+// 			)
+
+// 			AssertionSet newHave, newerNeed( newNeed );
+// 			TypeEnvironment newEnv( newAlt.env );
+// 			OpenVarSet newOpenVars( openVars );
+// 			Type *adjType = candidate->get_type()->clone();
+// 			adjustExprType( adjType, newEnv, indexer );
+// 			renameTyVars( adjType );
+// 			PRINT(
+// 				std::cerr << "unifying ";
+// 				curDecl->get_type()->print( std::cerr );
+// 				std::cerr << " with ";
+// 				adjType->print( std::cerr );
+// 				std::cerr << std::endl;
+// 			)
+// 			if ( unify( curDecl->get_type(), adjType, newEnv, newerNeed, newHave, newOpenVars, indexer ) ) {
+// 				PRINT(
+// 					std::cerr << "success!" << std::endl;
+// 				)
+// 				SymTab::Indexer newDecls( decls );
+// 				addToIndexer( newHave, newDecls );
+// 				Alternative newerAlt( newAlt );
+// 				newerAlt.env = newEnv;
+// 				assertf( candidate->get_uniqueId(), "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
+
+// 				// everything with an empty idChain was pulled in by the current assertion.
+// 				// add current assertion's idChain + current assertion's ID so that the correct inferParameters can be found.
+// 				for ( auto & a : newerNeed ) {
+// 					if ( a.second.idChain.empty() ) {
+// 						a.second.idChain = cur->second.idChain;
+// 						a.second.idChain.push_back( curDecl->get_uniqueId() );
+// 					}
+// 				}
+
+// 				Expression *varExpr = data.combine( newerAlt.cvtCost );
+// 				delete varExpr->get_result();
+// 				varExpr->set_result( adjType->clone() );
+// 				PRINT(
+// 					std::cerr << "satisfying assertion " << curDecl->get_uniqueId() << " ";
+// 					curDecl->print( std::cerr );
+// 					std::cerr << " with declaration " << candidate->get_uniqueId() << " ";
+// 					candidate->print( std::cerr );
+// 					std::cerr << std::endl;
+// 				)
+// 				// follow the current assertion's ID chain to find the correct set of inferred parameters to add the candidate to (i.e. the set of inferred parameters belonging to the entity which requested the assertion parameter).
+// 				InferredParams * inferParameters = &newerAlt.expr->get_inferParams();
+// 				for ( UniqueId id : cur->second.idChain ) {
+// 					inferParameters = (*inferParameters)[ id ].inferParams.get();
+// 				}
+// 				// XXX: this is a memory leak, but adjType can't be deleted because it might contain assertions
+// 				(*inferParameters)[ curDecl->get_uniqueId() ] = ParamEntry( candidate->get_uniqueId(), adjType->clone(), curDecl->get_type()->clone(), varExpr );
+// 				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, level, indexer, out );
+// 			} else {
+// 				delete adjType;
+// 			}
+// 		}
+// 	}
 
 	template< typename OutputIterator >
-	void AlternativeFinder::Finder::inferParameters( const AssertionSet &need, AssertionSet &have, const Alternative &newAlt, OpenVarSet &openVars, OutputIterator out ) {
-//	PRINT(
-//	    std::cerr << "inferParameters: assertions needed are" << std::endl;
-//	    printAll( need, std::cerr, 8 );
-//	    )
-		SymTab::Indexer decls( indexer );
+	void AlternativeFinder::Finder::inferParameters( const AssertionSet &, AssertionSet &, const Alternative &newAlt, OpenVarSet &, OutputIterator out ) {
+		// SymTab::Indexer decls( indexer );
+		// addToIndexer( have, decls );
+		// AssertionSet newNeed;
 		// PRINT(
-		// 	std::cerr << "============= original indexer" << std::endl;
-		// 	indexer.print( std::cerr );
-		// 	std::cerr << "============= new indexer" << std::endl;
-		// 	decls.print( std::cerr );
+		// 	std::cerr << "env is: " << std::endl;
+		// 	newAlt.env.print( std::cerr, 0 );
+		// 	std::cerr << std::endl;
 		// )
-		addToIndexer( have, decls );
-		AssertionSet newNeed;
-		PRINT(
-			std::cerr << "env is: " << std::endl;
-			newAlt.env.print( std::cerr, 0 );
-			std::cerr << std::endl;
-		)
-
-		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, 0, indexer, out );
-//	PRINT(
-//	    std::cerr << "declaration 14 is ";
-//	    Declaration::declFromId
-//	    *out++ = newAlt;
-//	    )
+
+		// inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, 0, indexer, out );
+
+		// add to output list, assertion resolution is defered
+		*out++ = newAlt;
 	}
 
@@ -965,5 +962,7 @@
 		}
 		// build and validate new alternative
-		Alternative newAlt( appExpr, result.env, cost );
+		Alternative newAlt{ 
+			appExpr, result.env, result.openVars, 
+			AssertionList( result.need.begin(), result.need.end() ), cost };
 		PRINT(
 			std::cerr << "instantiate function success: " << appExpr << std::endl;
@@ -1248,5 +1247,5 @@
 			if ( isLvalue( alt.expr ) ) {
 				alternatives.push_back(
-					Alternative{ new AddressExpr( alt.expr->clone() ), alt.env, alt.cost } );
+					Alternative{ alt, new AddressExpr( alt.expr->clone() ), alt.cost } );
 			} // if
 		} // for
@@ -1254,5 +1253,5 @@
 
 	void AlternativeFinder::Finder::postvisit( LabelAddressExpr * expr ) {
-		alternatives.push_back( Alternative{ expr->clone(), env, Cost::zero } );
+		alternatives.push_back( Alternative{ expr->clone(), env } );
 	}
 
@@ -1299,6 +1298,7 @@
 		AltList candidates;
 		for ( Alternative & alt : finder.alternatives ) {
-			AssertionSet needAssertions, haveAssertions;
-			OpenVarSet openVars;
+			AssertionSet needAssertions( alt.need.begin(), alt.need.end() );
+			AssertionSet haveAssertions;
+			OpenVarSet openVars{ alt.openVars };
 
 			alt.env.extractOpenVars( openVars );
@@ -1328,6 +1328,9 @@
 				// count one safe conversion for each value that is thrown away
 				thisCost.incSafe( discardedValues );
-				Alternative newAlt( restructureCast( alt.expr->clone(), toType, castExpr->isGenerated ), alt.env,
-					alt.cost, thisCost );
+				Alternative newAlt{ 
+					restructureCast( alt.expr->clone(), toType, castExpr->isGenerated ), 
+					alt.env, openVars, 
+					AssertionList( needAssertions.begin(), needAssertions.end() ), alt.cost, 
+					thisCost };
 				inferParameters( needAssertions, haveAssertions, newAlt, openVars,
 					back_inserter( candidates ) );
@@ -1344,12 +1347,12 @@
 
 	void AlternativeFinder::Finder::postvisit( VirtualCastExpr * castExpr ) {
-		assertf( castExpr->get_result(), "Implicate virtual cast targets not yet supported." );
+		assertf( castExpr->get_result(), "Implicit virtual cast targets not yet supported." );
 		AlternativeFinder finder( indexer, env );
 		// don't prune here, since it's guaranteed all alternatives will have the same type
 		finder.findWithoutPrune( castExpr->get_arg() );
 		for ( Alternative & alt : finder.alternatives ) {
-			alternatives.push_back( Alternative(
-				new VirtualCastExpr( alt.expr->clone(), castExpr->get_result()->clone() ),
-				alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{
+				alt, new VirtualCastExpr{ alt.expr->clone(), castExpr->get_result()->clone() },
+				alt.cost } );
 		}
 	}
@@ -1376,9 +1379,9 @@
 			// find member of the given type
 			if ( StructInstType *structInst = dynamic_cast< StructInstType* >( aggrExpr->get_result() ) ) {
-				addAggMembers( structInst, aggrExpr, cost, agg->env, get_member_name(memberExpr) );
+				addAggMembers( structInst, aggrExpr, *agg, cost, get_member_name(memberExpr) );
 			} else if ( UnionInstType *unionInst = dynamic_cast< UnionInstType* >( aggrExpr->get_result() ) ) {
-				addAggMembers( unionInst, aggrExpr, cost, agg->env, get_member_name(memberExpr) );
+				addAggMembers( unionInst, aggrExpr, *agg, cost, get_member_name(memberExpr) );
 			} else if ( TupleType * tupleType = dynamic_cast< TupleType * >( aggrExpr->get_result() ) ) {
-				addTupleMembers( tupleType, aggrExpr, cost, agg->env, memberExpr->get_member() );
+				addTupleMembers( tupleType, aggrExpr, *agg, cost, memberExpr->get_member() );
 			} // if
 		} // for
@@ -1386,5 +1389,5 @@
 
 	void AlternativeFinder::Finder::postvisit( MemberExpr *memberExpr ) {
-		alternatives.push_back( Alternative( memberExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ memberExpr->clone(), env } );
 	}
 
@@ -1399,5 +1402,5 @@
 			// addAnonAlternatives uses vector::push_back, which invalidates references to existing elements, so
 			// can't construct in place and use vector::back
-			Alternative newAlt( newExpr, env, Cost::zero, cost );
+			Alternative newAlt{ newExpr, env, OpenVarSet{}, AssertionList{}, Cost::zero, cost };
 			PRINT(
 				std::cerr << "decl is ";
@@ -1417,9 +1420,9 @@
 		// not sufficient to clone here, because variable's type may have changed
 		// since the VariableExpr was originally created.
-		alternatives.push_back( Alternative( new VariableExpr( variableExpr->var ), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ new VariableExpr{ variableExpr->var }, env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( ConstantExpr *constantExpr ) {
-		alternatives.push_back( Alternative( constantExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ constantExpr->clone(), env } );
 	}
 
@@ -1427,5 +1430,6 @@
 		if ( sizeofExpr->get_isType() ) {
 			Type * newType = sizeofExpr->get_type()->clone();
-			alternatives.push_back( Alternative( new SizeofExpr( resolveTypeof( newType, indexer ) ), env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				new SizeofExpr{ resolveTypeof( newType, indexer ) }, env } );
 		} else {
 			// find all alternatives for the argument to sizeof
@@ -1441,5 +1445,6 @@
 			Alternative &choice = winners.front();
 			referenceToRvalueConversion( choice.expr, choice.cost );
-			alternatives.push_back( Alternative( new SizeofExpr( choice.expr->clone() ), choice.env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				choice, new SizeofExpr( choice.expr->clone() ), Cost::zero } );
 		} // if
 	}
@@ -1448,5 +1453,6 @@
 		if ( alignofExpr->get_isType() ) {
 			Type * newType = alignofExpr->get_type()->clone();
-			alternatives.push_back( Alternative( new AlignofExpr( resolveTypeof( newType, indexer ) ), env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				new AlignofExpr{ resolveTypeof( newType, indexer ) }, env } );
 		} else {
 			// find all alternatives for the argument to sizeof
@@ -1462,5 +1468,6 @@
 			Alternative &choice = winners.front();
 			referenceToRvalueConversion( choice.expr, choice.cost );
-			alternatives.push_back( Alternative( new AlignofExpr( choice.expr->clone() ), choice.env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				choice, new AlignofExpr{ choice.expr->clone() }, Cost::zero } );
 		} // if
 	}
@@ -1472,5 +1479,6 @@
 		for ( std::list< Declaration* >::const_iterator i = members.begin(); i != members.end(); ++i ) {
 			if ( DeclarationWithType *dwt = dynamic_cast< DeclarationWithType* >( *i ) ) {
-				alternatives.push_back( Alternative( new OffsetofExpr( aggInst->clone(), dwt ), env, Cost::zero ) );
+				alternatives.push_back( Alternative{ 
+					new OffsetofExpr{ aggInst->clone(), dwt }, env } );
 				renameTypes( alternatives.back().expr );
 			} else {
@@ -1491,9 +1499,9 @@
 
 	void AlternativeFinder::Finder::postvisit( OffsetofExpr *offsetofExpr ) {
-		alternatives.push_back( Alternative( offsetofExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ offsetofExpr->clone(), env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( OffsetPackExpr *offsetPackExpr ) {
-		alternatives.push_back( Alternative( offsetPackExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ offsetPackExpr->clone(), env } );
 	}
 
@@ -1515,5 +1523,7 @@
 				Cost cost = Cost::zero;
 				Expression * newExpr = data.combine( cost );
-				alternatives.push_back( Alternative( new AttrExpr( newExpr, argType->clone() ), env, Cost::zero, cost ) );
+				alternatives.push_back( Alternative{ 
+					new AttrExpr{ newExpr, argType->clone() }, env, OpenVarSet{}, AssertionList{},  
+					Cost::zero, cost } );
 				for ( DeclarationWithType * retVal : function->returnVals ) {
 					alternatives.back().expr->result = retVal->get_type()->clone();
@@ -1554,5 +1564,6 @@
 				Cost cost = Cost::zero;
 				Expression * newExpr = data.combine( cost );
-				alternatives.push_back( Alternative( newExpr, env, Cost::zero, cost ) );
+				alternatives.push_back( Alternative{ 
+					newExpr, env, OpenVarSet{}, AssertionList{}, Cost::zero, cost } );
 				renameTypes( alternatives.back().expr );
 			} // for
@@ -1569,10 +1580,15 @@
 		for ( const Alternative & first : firstFinder.alternatives ) {
 			for ( const Alternative & second : secondFinder.alternatives ) {
-				TypeEnvironment compositeEnv;
-				compositeEnv.simpleCombine( first.env );
+				TypeEnvironment compositeEnv{ first.env };
 				compositeEnv.simpleCombine( second.env );
-
-				LogicalExpr *newExpr = new LogicalExpr( first.expr->clone(), second.expr->clone(), logicalExpr->get_isAnd() );
-				alternatives.push_back( Alternative( newExpr, compositeEnv, first.cost + second.cost ) );
+				OpenVarSet openVars{ first.openVars };
+				mergeOpenVars( openVars, second.openVars );
+				AssertionList need{ first.need };
+				need.insert( need.end(), second.need.begin(), second.need.end() );
+
+				LogicalExpr *newExpr = new LogicalExpr{ 
+					first.expr->clone(), second.expr->clone(), logicalExpr->get_isAnd() };
+				alternatives.push_back( Alternative{ 
+					newExpr, compositeEnv, openVars, need, first.cost + second.cost } );
 			}
 		}
@@ -1595,21 +1611,32 @@
 			for ( const Alternative & second : secondFinder.alternatives ) {
 				for ( const Alternative & third : thirdFinder.alternatives ) {
-					TypeEnvironment compositeEnv;
-					compositeEnv.simpleCombine( first.env );
+					TypeEnvironment compositeEnv{ first.env };
 					compositeEnv.simpleCombine( second.env );
 					compositeEnv.simpleCombine( third.env );
-
+					OpenVarSet openVars{ first.openVars };
+					mergeOpenVars( openVars, second.openVars );
+					mergeOpenVars( openVars, third.openVars );
+					AssertionSet needAssertions( first.need.begin(), first.need.end() );
+					needAssertions.insert( second.need.begin(), second.need.end() );
+					needAssertions.insert( third.need.begin(), third.need.end() );
+					AssertionSet haveAssertions;
+					
 					// unify true and false types, then infer parameters to produce new alternatives
-					OpenVarSet openVars;
-					AssertionSet needAssertions, haveAssertions;
-					Alternative newAlt( 0, compositeEnv, first.cost + second.cost + third.cost );
 					Type* commonType = nullptr;
-					if ( unify( second.expr->result, third.expr->result, newAlt.env, needAssertions, haveAssertions, openVars, indexer, commonType ) ) {
-						ConditionalExpr *newExpr = new ConditionalExpr( first.expr->clone(), second.expr->clone(), third.expr->clone() );
+					if ( unify( second.expr->result, third.expr->result, compositeEnv, 
+							needAssertions, haveAssertions, openVars, indexer, commonType ) ) {
+						ConditionalExpr *newExpr = new ConditionalExpr{ 
+							first.expr->clone(), second.expr->clone(), third.expr->clone() };
 						newExpr->result = commonType ? commonType : second.expr->result->clone();
 						// convert both options to the conditional result type
-						newAlt.cost += computeExpressionConversionCost( newExpr->arg2, newExpr->result, indexer, newAlt.env );
-						newAlt.cost += computeExpressionConversionCost( newExpr->arg3, newExpr->result, indexer, newAlt.env );
-						newAlt.expr = newExpr;
+						Cost cost = first.cost + second.cost + third.cost;
+						cost += computeExpressionConversionCost( 
+							newExpr->arg2, newExpr->result, indexer, compositeEnv );
+						cost += computeExpressionConversionCost( 
+							newExpr->arg3, newExpr->result, indexer, compositeEnv );
+						// output alternative
+						Alternative newAlt{ 
+							newExpr, compositeEnv, openVars, 
+							AssertionList( needAssertions.begin(), needAssertions.end() ), cost };
 						inferParameters( needAssertions, haveAssertions, newAlt, openVars, back_inserter( alternatives ) );
 					} // if
@@ -1625,5 +1652,6 @@
 		secondFinder.findWithAdjustment( commaExpr->get_arg2() );
 		for ( const Alternative & alt : secondFinder.alternatives ) {
-			alternatives.push_back( Alternative( new CommaExpr( newFirstArg->clone(), alt.expr->clone() ), alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{ 
+				alt, new CommaExpr{ newFirstArg->clone(), alt.expr->clone() }, alt.cost } );
 		} // for
 		delete newFirstArg;
@@ -1640,15 +1668,22 @@
 		for ( const Alternative & first : firstFinder.alternatives ) {
 			for ( const Alternative & second : secondFinder.alternatives ) {
-				TypeEnvironment compositeEnv;
-				compositeEnv.simpleCombine( first.env );
+				TypeEnvironment compositeEnv{ first.env };
 				compositeEnv.simpleCombine( second.env );
-				OpenVarSet openVars;
-				AssertionSet needAssertions, haveAssertions;
-				Alternative newAlt( 0, compositeEnv, first.cost + second.cost );
+				OpenVarSet openVars{ first.openVars };
+				mergeOpenVars( openVars, second.openVars );
+				AssertionSet needAssertions( first.need.begin(), first.need.end() );
+				needAssertions.insert( second.need.begin(), second.need.end() );
+				AssertionSet haveAssertions;
+
 				Type* commonType = nullptr;
-				if ( unify( first.expr->result, second.expr->result, newAlt.env, needAssertions, haveAssertions, openVars, indexer, commonType ) ) {
-					RangeExpr * newExpr = new RangeExpr( first.expr->clone(), second.expr->clone() );
+				if ( unify( first.expr->result, second.expr->result, compositeEnv, needAssertions, 
+						haveAssertions, openVars, indexer, commonType ) ) {
+					RangeExpr * newExpr = 
+						new RangeExpr{ first.expr->clone(), second.expr->clone() };
 					newExpr->result = commonType ? commonType : first.expr->result->clone();
-					newAlt.expr = newExpr;
+					Alternative newAlt{ 
+						newExpr, compositeEnv, openVars, 
+						AssertionList( needAssertions.begin(), needAssertions.end() ), 
+						first.cost + second.cost };
 					inferParameters( needAssertions, haveAssertions, newAlt, openVars, back_inserter( alternatives ) );
 				} // if
@@ -1669,16 +1704,24 @@
 
 			TypeEnvironment compositeEnv;
-			simpleCombineEnvironments( alts.begin(), alts.end(), compositeEnv );
-			alternatives.push_back(
-				Alternative{ new TupleExpr( exprs ), compositeEnv, sumCost( alts ) } );
+			OpenVarSet openVars;
+			AssertionSet need;
+			for ( const Alternative& alt : alts ) {
+				compositeEnv.simpleCombine( alt.env );
+				mergeOpenVars( openVars, alt.openVars );
+				need.insert( alt.need.begin(), alt.need.end() );
+			}
+			
+			alternatives.push_back( Alternative{ 
+				new TupleExpr{ exprs }, compositeEnv, openVars, 
+				AssertionList( need.begin(), need.end() ), sumCost( alts ) } );
 		} // for
 	}
 
 	void AlternativeFinder::Finder::postvisit( TupleExpr *tupleExpr ) {
-		alternatives.push_back( Alternative( tupleExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ tupleExpr->clone(), env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( ImplicitCopyCtorExpr * impCpCtorExpr ) {
-		alternatives.push_back( Alternative( impCpCtorExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ impCpCtorExpr->clone(), env } );
 	}
 
@@ -1689,14 +1732,15 @@
 		finder.findWithoutPrune( ctorExpr->get_callExpr() );
 		for ( Alternative & alt : finder.alternatives ) {
-			alternatives.push_back( Alternative( new ConstructorExpr( alt.expr->clone() ), alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{ 
+				alt, new ConstructorExpr( alt.expr->clone() ), alt.cost } );
 		}
 	}
 
 	void AlternativeFinder::Finder::postvisit( TupleIndexExpr *tupleExpr ) {
-		alternatives.push_back( Alternative( tupleExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ tupleExpr->clone(), env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( TupleAssignExpr *tupleAssignExpr ) {
-		alternatives.push_back( Alternative( tupleAssignExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ tupleAssignExpr->clone(), env } );
 	}
 
@@ -1707,5 +1751,5 @@
 			// ensure that the id is passed on to the UniqueExpr alternative so that the expressions are "linked"
 			UniqueExpr * newUnqExpr = new UniqueExpr( alt.expr->clone(), unqExpr->get_id() );
-			alternatives.push_back( Alternative( newUnqExpr, alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{ alt, newUnqExpr, alt.cost } );
 		}
 	}
@@ -1715,5 +1759,5 @@
 		ResolvExpr::resolveStmtExpr( newStmtExpr, indexer );
 		// xxx - this env is almost certainly wrong, and needs to somehow contain the combined environments from all of the statements in the stmtExpr...
-		alternatives.push_back( Alternative( newStmtExpr, env, Cost::zero ) );
+		alternatives.push_back( Alternative{ newStmtExpr, env } );
 	}
 
@@ -1737,19 +1781,27 @@
 			for ( Alternative & alt : finder.get_alternatives() ) {
 				TypeEnvironment newEnv( alt.env );
-				AssertionSet needAssertions, haveAssertions;
-				OpenVarSet openVars;  // find things in env that don't have a "representative type" and claim those are open vars?
+				AssertionSet needAssertions( alt.need.begin(), alt.need.end() );
+				AssertionSet haveAssertions;
+				OpenVarSet openVars( alt.openVars );  
+				// xxx - find things in env that don't have a "representative type" and claim 
+				// those are open vars?
 				PRINT(
 					std::cerr << "  @ " << toType << " " << initAlt.designation << std::endl;
 				)
-				// It's possible that a cast can throw away some values in a multiply-valued expression.  (An example is a
-				// cast-to-void, which casts from one value to zero.)  Figure out the prefix of the subexpression results
-				// that are cast directly.  The candidate is invalid if it has fewer results than there are types to cast
-				// to.
+				// It's possible that a cast can throw away some values in a multiply-valued 
+				// expression. (An example is a cast-to-void, which casts from one value to 
+				// zero.)  Figure out the prefix of the subexpression results that are cast 
+				// directly.  The candidate is invalid if it has fewer results than there are 
+				// types to cast to.
 				int discardedValues = alt.expr->result->size() - toType->size();
 				if ( discardedValues < 0 ) continue;
-				// xxx - may need to go into tuple types and extract relevant types and use unifyList. Note that currently, this does not
-				// allow casting a tuple to an atomic type (e.g. (int)([1, 2, 3]))
+				// xxx - may need to go into tuple types and extract relevant types and use 
+				// unifyList. Note that currently, this does not allow casting a tuple to an 
+				// atomic type (e.g. (int)([1, 2, 3]))
+				
 				// unification run for side-effects
-				unify( toType, alt.expr->result, newEnv, needAssertions, haveAssertions, openVars, indexer ); // xxx - do some inspecting on this line... why isn't result bound to initAlt.type??
+				unify( toType, alt.expr->result, newEnv, needAssertions, haveAssertions, openVars, 
+					indexer );
+				// xxx - do some inspecting on this line... why isn't result bound to initAlt.type?
 
 				Cost thisCost = castCost( alt.expr->result, toType, indexer, newEnv );
@@ -1757,5 +1809,10 @@
 					// count one safe conversion for each value that is thrown away
 					thisCost.incSafe( discardedValues );
-					Alternative newAlt( new InitExpr( restructureCast( alt.expr->clone(), toType, true ), initAlt.designation->clone() ), newEnv, alt.cost, thisCost );
+					Alternative newAlt{ 
+						new InitExpr{ 
+							restructureCast( alt.expr->clone(), toType, true ), initAlt.designation->clone() }, 
+						newEnv, openVars, 
+						AssertionList( needAssertions.begin(), needAssertions.end() ), 
+						alt.cost, thisCost };
 					inferParameters( needAssertions, haveAssertions, newAlt, openVars, back_inserter( candidates ) );
 				}
Index: src/ResolvExpr/Cost.h
===================================================================
--- src/ResolvExpr/Cost.h	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/Cost.h	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -10,6 +10,6 @@
 // Created On       : Sun May 17 09:39:50 2015
 // Last Modified By : Aaron B. Moss
-// Last Modified On : Tue Oct 02 14:40:00 2018
-// Update Count     : 6
+// Last Modified On : Fri Oct 05 14:32:00 2018
+// Update Count     : 7
 //
 
@@ -46,4 +46,6 @@
 		bool operator!=( const Cost &other ) const;
 		friend std::ostream &operator<<( std::ostream &os, const Cost &cost );
+		// returns negative for *this < other, 0 for *this == other, positive for *this > other
+		int compare( const Cost &other ) const;
 
 		static const Cost zero;
@@ -56,7 +58,6 @@
 		static const Cost safe;
 		static const Cost reference;
+
 	  private:
-		int compare( const Cost &other ) const;
-
 		int unsafeCost;     ///< Unsafe (narrowing) conversions
 		int polyCost;       ///< Count of parameters and return values bound to some poly type
@@ -172,4 +173,16 @@
 	}
 
+	inline int Cost::compare( const Cost &other ) const {
+		if ( *this == infinity ) return +1;
+		if ( other == infinity ) return -1;
+
+		int c = unsafeCost - other.unsafeCost; if ( c ) return c;
+		c = polyCost - other.polyCost; if ( c ) return c;
+		c = varCost - other.varCost; if ( c ) return c;
+		c = specCost - other.specCost; if ( c ) return c;
+		c = safeCost - other.safeCost; if ( c ) return c;
+		return referenceCost - other.referenceCost;
+	}
+
 	inline bool Cost::operator==( const Cost &other ) const {
 		return unsafeCost == other.unsafeCost
Index: src/ResolvExpr/ResolvMode.h
===================================================================
--- src/ResolvExpr/ResolvMode.h	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/ResolvMode.h	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -10,6 +10,6 @@
 // Created On       : Mon Jun 11 13:28:00 2018
 // Last Modified By : Aaron B. Moss
-// Last Modified On : Mon Jun 11 13:28:00 2018
-// Update Count     : 1
+// Last Modified On : Fri Oct 05 13:46:00 2018
+// Update Count     : 2
 //
 
@@ -22,14 +22,13 @@
 		const bool prune;            ///< Prune alternatives to min-cost per return type? [true]
 		const bool failFast;         ///< Fail on no resulting alternatives? [true]
-		const bool checkAssertions;  ///< Should assertions be checked? [false]
+		const bool resolveAssns;     ///< Resolve assertions? [false]
 
 	private:
-		constexpr ResolvMode(bool a, bool p, bool ff, bool ca)
-			: adjust(a), prune(p), failFast(ff), checkAssertions(ca) {}
+		constexpr ResolvMode(bool a, bool p, bool ff, bool ra) 
+		: adjust(a), prune(p), failFast(ff), resolveAssns(ra) {}
 
 	public:
 		/// Default settings
-		constexpr ResolvMode()
-			: adjust(false), prune(true), failFast(true), checkAssertions(false) {}
+		constexpr ResolvMode() : adjust(false), prune(true), failFast(true), resolveAssns(false) {}
 		
 		/// With adjust flag set; turns array and function types into equivalent pointers
@@ -43,4 +42,7 @@
 		/// one resulting alternative
 		static constexpr ResolvMode withoutFailFast() { return { true, true, false, false }; }
+
+		/// The same mode, but with resolveAssns turned on; for top-level calls
+		ResolvMode atTopLevel() const { return { adjust, prune, failFast, true }; }
 	};
 } // namespace ResolvExpr
Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -0,0 +1,322 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// ResolveAssertions.cc --
+//
+// Author           : Aaron B. Moss
+// Created On       : Fri Oct 05 13:46:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 13:46:00 2018
+// Update Count     : 1
+//
+
+#include "ResolveAssertions.h"
+
+#include <cassert>                // for assertf
+#include <list>                   // for list
+#include <utility>                // for move
+#include <vector>                 // for vector
+
+#include "Alternative.h"          // for Alternative, AssertionItem
+#include "Common/FilterCombos.h"  // for filterCombos
+#include "SymTab/Indexer.h"       // for Indexer
+#include "TypeEnvironment.h"      // for TypeEnvironment, etc.
+#include "typeops.h"              // for adjustExprType
+#include "Unify.h"                // for unify
+
+namespace ResolvExpr {
+	/// Unified assertion candidate
+	struct AssnCandidate {
+		SymTab::Indexer::IdData cdata;  ///< Satisfying declaration
+		Type* adjType;                  ///< Satisfying type
+		TypeEnvironment env;            ///< Post-unification environment
+		AssertionSet have;              ///< Post-unification have-set
+		AssertionSet need;              ///< Post-unification need-set
+		OpenVarSet openVars;            ///< Post-unification open-var set
+
+		AssnCandidate( const SymTab::Indexer::IdData& cdata, Type* adjType, TypeEnvironment&& env, 
+			AssertionSet&& have, AssertionSet&& need, OpenVarSet&& openVars ) 
+		: cdata(cdata), adjType(adjType), env(std::move(env)), have(std::move(have)), 
+			need(std::move(need)), openVars(std::move(openVars)) {}
+	};
+
+	/// List of candidate assertion resolutions
+	using CandidateList = std::vector<AssnCandidate>;
+
+	/// Reference to single deferred item
+	struct DeferRef {
+		const DeclarationWithType* decl;
+		const AssertionSetValue& info;
+		const AssnCandidate& match;
+	};
+
+	/// Wrapper for the deferred items from a single assertion resolution.
+	/// Acts like indexed list of DeferRef
+	struct DeferItem {
+		DeclarationWithType* decl;
+		AssertionSetValue info;
+		CandidateList matches;
+
+		DeferItem( DeclarationWithType* decl, const AssertionSetValue& info, 
+			CandidateList&& matches )
+		: decl(decl), info(info), matches(std::move(matches)) {}
+
+		bool empty() const { return matches.empty(); }
+
+		CandidateList::size_type size() const { return matches.size(); }
+
+		DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+	};
+
+	/// List of deferred resolution items
+	using DeferList = std::vector<DeferItem>;
+
+	/// Combo iterator that combines candidates into an output list, merging their environments. 
+	/// Rejects an appended candidate if the environments cannot be merged.
+	class CandidateEnvMerger {
+		/// Current list of merged candidates
+		std::vector<DeferRef> crnt;
+		/// Stack of environments to support backtracking
+		std::vector<TypeEnvironment> envs;
+		/// Stack of open variables to support backtracking
+		std::vector<OpenVarSet> varSets;
+		/// Indexer to use for merges
+		const SymTab::Indexer& indexer;
+	
+	public:
+		/// The merged environment/open variables and the list of candidates
+		struct OutType {
+			TypeEnvironment env;
+			OpenVarSet openVars;
+			std::vector<DeferRef> assns;
+
+			OutType( const TypeEnvironment& env, const OpenVarSet& openVars, 
+				const std::vector<DeferRef>& assns )
+			: env(env), openVars(openVars), assns(assns) {}
+		};
+
+		CandidateEnvMerger( const TypeEnvironment& env, const OpenVarSet& openVars, 
+			const SymTab::Indexer& indexer )
+		: crnt(), envs{ env }, varSets{ openVars }, indexer(indexer) {}
+
+		bool append( DeferRef i ) {
+			TypeEnvironment env = envs.back();
+			OpenVarSet openVars = varSets.back();
+			mergeOpenVars( openVars, i.match.openVars );
+
+			if ( ! env.combine( i.match.env, openVars, indexer ) ) return false;
+
+			crnt.emplace_back( i );
+			envs.emplace_back( env );
+			varSets.emplace_back( openVars );
+			return true;
+		}
+
+		void backtrack() {
+			crnt.pop_back();
+			envs.pop_back();
+			varSets.pop_back();
+		}
+
+		OutType finalize() { return { envs.back(), varSets.back(), crnt }; }
+	};
+
+	/// Flag for state iteration
+	enum IterateFlag { IterateState };
+
+	/// State needed to resolve a set of assertions
+	struct ResnState {
+		Alternative alt;                  ///< Alternative assertion is rooted on
+		std::vector<AssertionItem> need;  ///< Assertions to find
+		AssertionSet newNeed;             ///< New assertions for current resolutions
+		DeferList deferred;               ///< Deferred matches
+		SymTab::Indexer& indexer;         ///< Name lookup (depends on previous assertions)
+
+		/// Initial resolution state for an alternative
+		ResnState( Alternative& a, SymTab::Indexer& indexer )
+		: alt(a), need(), newNeed(), deferred(), indexer(indexer) {
+			need.swap( a.need );
+		}
+
+		/// Updated resolution state with new need-list
+		ResnState( ResnState&& o, IterateFlag )
+		: alt(std::move(o.alt)), need(o.newNeed.begin(), o.newNeed.end()), newNeed(), deferred(), 
+		  indexer(o.indexer) {}
+	};
+
+	/// Binds a single assertion, updating resolution state
+	void bindAssertion( const DeclarationWithType* decl, AssertionSetValue info, Alternative& alt, 
+			AssnCandidate& match ) {
+		
+		DeclarationWithType* candidate = match.cdata.id;
+		assertf( candidate->get_uniqueId(), "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
+
+		// everything with an empty idChain was pulled in by the current assertion.
+		// add current assertion's idChain + current assertion's ID so that the correct 
+		// inferParameters can be found.
+		for ( auto& a : match.need ) {
+			if ( a.second.idChain.empty() ) {
+				a.second.idChain = info.idChain;
+				a.second.idChain.push_back( decl->get_uniqueId() );
+			}
+		}
+
+		Expression* varExpr = match.cdata.combine( alt.cvtCost );
+		varExpr->result = match.adjType;
+
+		// follow the current assertion's ID chain to find the correct set of inferred parameters 
+		// to add the candidate o (i.e. the set of inferred parameters belonging to the entity 
+		// which requested the assertion parameter)
+		InferredParams* inferParams = &alt.expr->inferParams;
+		for ( UniqueId id : info.idChain ) {
+			inferParams = (*inferParams)[ id ].inferParams.get();
+		}
+
+		(*inferParams)[ decl->get_uniqueId() ] = ParamEntry{
+				candidate->get_uniqueId(), match.adjType, decl->get_type(), varExpr };
+	}
+
+	/// Adds a captured assertion to the symbol table
+	void addToIndexer( AssertionSet &assertSet, SymTab::Indexer &indexer ) {
+		for ( AssertionSet::iterator i = assertSet.begin(); i != assertSet.end(); ++i ) {
+			if ( i->second.isUsed ) {
+				indexer.addId( i->first );
+			}
+		}
+	}
+
+	/// Resolve a single assertion, in context
+	bool resolveAssertion( AssertionItem& assn, ResnState& resn ) {
+		// skip unused assertions
+		if ( ! assn.info.isUsed ) return true;
+
+		// lookup candidates for this assertion
+		std::list< SymTab::Indexer::IdData > candidates;
+		resn.indexer.lookupId( assn.decl->name, candidates );
+
+		// find the candidates that unify with the desired type
+		CandidateList matches;
+		for ( const auto& cdata : candidates ) {
+			DeclarationWithType* candidate = cdata.id;
+
+			// build independent unification context for candidate
+			AssertionSet have, newNeed;
+			TypeEnvironment newEnv{ resn.alt.env };
+			OpenVarSet newOpenVars{ resn.alt.openVars };
+			Type* adjType = candidate->get_type()->clone();
+			adjustExprType( adjType, newEnv, resn.indexer );
+
+			// keep unifying candidates
+			if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 
+					resn.indexer ) ) {
+				matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 
+					std::move(newNeed), std::move(newOpenVars) );
+			}
+		}
+
+		// break if no suitable assertion
+		if ( matches.empty() ) return false;
+
+		// defer if too many suitable assertions
+		if ( matches.size() > 1 ) {
+			resn.deferred.emplace_back( assn.decl, assn.info, std::move(matches) );
+			return true;
+		}
+
+		// otherwise bind current match in ongoing scope
+		AssnCandidate& match = matches.front();
+		addToIndexer( match.have, resn.indexer );
+		resn.newNeed.insert( match.need.begin(), match.need.end() );
+		resn.alt.env = std::move(match.env);
+		resn.alt.openVars = std::move(match.openVars);
+
+		bindAssertion( assn.decl, assn.info, resn.alt, match );
+		return true;
+	}
+
+	///< Limit to depth of recursion of assertion satisfaction
+	static const int recursionLimit = /* 10 */ 4;
+
+	void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out ) {
+		// finish early if no assertions to resolve
+		if ( alt.need.empty() ) {
+			out.emplace_back( alt );
+			return;
+		}
+
+		// build list of possible resolutions
+		using ResnList = std::vector<ResnState>;
+		SymTab::Indexer root_indexer{ indexer };
+		ResnList resns{ ResnState{ alt, root_indexer } };
+		ResnList new_resns{};
+
+		// resolve assertions in breadth-first-order up to a limited number of levels deep
+		for ( unsigned level = 0; level < recursionLimit; ++level ) {
+			// scan over all mutually-compatible resolutions
+			for ( auto& resn : resns ) {
+				// make initial pass at matching assertions
+				for ( auto& assn : resn.need ) {
+					// fail early if any assertion is not resolvable
+					if ( ! resolveAssertion( assn, resn ) ) goto nextResn;
+				}
+
+				if ( resn.deferred.empty() ) {
+					// either add successful match or push back next state
+					if ( resn.newNeed.empty() ) {
+						out.emplace_back( resn.alt );
+					} else {
+						new_resns.emplace_back( std::move(resn), IterateState );
+					}
+				} else {
+					// resolve deferred assertions by mutual compatibility
+					std::vector<CandidateEnvMerger::OutType> compatible = filterCombos(
+						resn.deferred, 
+						CandidateEnvMerger{ resn.alt.env, resn.alt.openVars, resn.indexer } );
+					
+					for ( auto& compat : compatible ) {
+						ResnState new_resn = resn;
+
+						// add compatible assertions to new resolution state
+						for ( DeferRef r : compat.assns ) {
+							AssnCandidate match = r.match;
+							addToIndexer( match.have, new_resn.indexer );
+							new_resn.newNeed.insert( match.need.begin(), match.need.end() );
+
+							bindAssertion( r.decl, r.info, new_resn.alt, match );
+						}
+
+						// set mutual environment into resolution state
+						new_resn.alt.env = std::move(compat.env);
+						new_resn.alt.openVars = std::move(compat.openVars);
+
+						// either add sucessful match or push back next state
+						if ( new_resn.newNeed.empty() ) {
+							out.emplace_back( new_resn.alt );
+						} else {
+							new_resns.emplace_back( std::move(new_resn), IterateState );
+						}
+					}
+				}
+			nextResn:; }
+
+			// finish or reset for next round
+			if ( new_resns.empty() ) return;
+			resns.swap( new_resns );
+			new_resns.clear();
+		}
+		
+		// exceeded recursion limit if reaches here
+		if ( out.empty() ) {
+			SemanticError( alt.expr->location, "Too many recursive assertions" );
+		}
+	}
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/ResolveAssertions.h
===================================================================
--- src/ResolvExpr/ResolveAssertions.h	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
+++ src/ResolvExpr/ResolveAssertions.h	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -0,0 +1,33 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// ResolveAssertions.h --
+//
+// Author           : Aaron B. Moss
+// Created On       : Fri Oct 05 13:46:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 13:46:00 2018
+// Update Count     : 1
+//
+
+#pragma once
+
+#include "Alternative.h"  // for Alternative, AltList
+
+namespace SymTab {
+	class Indexer;
+}
+
+namespace ResolvExpr {
+	/// Recursively resolves all assertions provided in an alternative; returns true iff succeeds
+	void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out );
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/Resolver.cc	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -14,9 +14,8 @@
 //
 
-#include <stddef.h>                      // for NULL
 #include <cassert>                       // for strict_dynamic_cast, assert
 #include <memory>                        // for allocator, allocator_traits<...
 #include <tuple>                         // for get
-#include <vector>
+#include <vector>                        // for vector
 
 #include "Alternative.h"                 // for Alternative, AltList
@@ -171,7 +170,13 @@
 		void findUnfinishedKindExpression(Expression * untyped, Alternative & alt, const SymTab::Indexer & indexer, const std::string & kindStr, std::function<bool(const Alternative &)> pred, ResolvMode mode = ResolvMode{} ) {
 			assertf( untyped, "expected a non-null expression." );
+
+			// xxx - this isn't thread-safe, but should work until we parallelize the resolver
+			static unsigned recursion_level = 0;
+
+			++recursion_level;
 			TypeEnvironment env;
 			AlternativeFinder finder( indexer, env );
-			finder.find( untyped, mode );
+			finder.find( untyped, recursion_level == 1 ? mode.atTopLevel() : mode );
+			--recursion_level;
 
 			#if 0
@@ -186,4 +191,5 @@
 			#endif
 
+			// produce filtered list of alternatives
 			AltList candidates;
 			for ( Alternative & alt : finder.get_alternatives() ) {
@@ -193,11 +199,43 @@
 			}
 
-			// xxx - if > 1 alternative with same cost, ignore deleted and pick from remaining
-			// choose the lowest cost expression among the candidates
+			// produce invalid error if no candidates
+			if ( candidates.empty() ) {
+				SemanticError( untyped, toString( "No reasonable alternatives for ", kindStr, (kindStr != "" ? " " : ""), "expression: ") );
+			}
+
+			// search for cheapest candidate
 			AltList winners;
-			findMinCost( candidates.begin(), candidates.end(), back_inserter( winners ) );
-			if ( winners.size() == 0 ) {
-				SemanticError( untyped, toString( "No reasonable alternatives for ", kindStr, (kindStr != "" ? " " : ""), "expression: ") );
-			} else if ( winners.size() != 1 ) {
+			bool seen_undeleted = false;
+			for ( unsigned i = 0; i < candidates.size(); ++i ) {
+				int c = winners.empty() ? -1 : candidates[i].cost.compare( winners.front().cost );
+
+				if ( c > 0 ) continue; // skip more expensive than winner
+
+				if ( c < 0 ) {
+					// reset on new cheapest
+					seen_undeleted = ! findDeletedExpr( candidates[i].expr );
+					winners.clear();
+				} else /* if ( c == 0 ) */ {
+					if ( findDeletedExpr( candidates[i].expr ) ) {
+						// skip deleted expression if already seen one equivalent-cost not
+						if ( seen_undeleted ) continue;
+					} else if ( ! seen_undeleted ) {
+						// replace list of equivalent-cost deleted expressions with one non-deleted
+						winners.clear();
+						seen_undeleted = true;
+					}
+				}
+
+				winners.emplace_back( candidates[i] );
+			}
+
+			// promote alternative.cvtCost to .cost
+			// xxx - I don't know why this is done, but I'm keeping the behaviour from findMinCost
+			for ( Alternative& winner : winners ) {
+				winner.cost = winner.cvtCost;
+			}
+			
+			// produce ambiguous errors, if applicable
+			if ( winners.size() != 1 ) {
 				std::ostringstream stream;
 				stream << "Cannot choose between " << winners.size() << " alternatives for " << kindStr << (kindStr != "" ? " " : "") << "expression\n";
@@ -208,9 +246,15 @@
 			}
 
-			// there is one unambiguous interpretation - move the expression into the with statement
-			Alternative & choice = winners.front();
-			if ( findDeletedExpr( choice.expr ) ) {
+			// single selected choice
+			Alternative& choice = winners.front();
+
+			// fail on only expression deleted
+			if ( ! seen_undeleted ) {
 				SemanticError( untyped->location, choice.expr, "Unique best alternative includes deleted identifier in " );
 			}
+
+			// xxx - check for ambiguous expressions
+			
+			// output selected choice
 			alt = std::move( choice );
 		}
@@ -358,9 +402,9 @@
 
 	void Resolver::previsit( ObjectDecl *objectDecl ) {
-		// To handle initialization of routine pointers, e.g., int (*fp)(int) = foo(), means that class-variable
-		// initContext is changed multiple time because the LHS is analysed twice. The second analysis changes
-		// initContext because of a function type can contain object declarations in the return and parameter types. So
-		// each value of initContext is retained, so the type on the first analysis is preserved and used for selecting
-		// the RHS.
+		// To handle initialization of routine pointers, e.g., int (*fp)(int) = foo(), means that 
+		// class-variable initContext is changed multiple time because the LHS is analysed twice. 
+		// The second analysis changes initContext because of a function type can contain object 
+		// declarations in the return and parameter types. So each value of initContext is 
+		// retained, so the type on the first analysis is preserved and used for selecting the RHS.
 		GuardValue( currentObject );
 		currentObject = CurrentObject( objectDecl->get_type() );
@@ -398,7 +442,8 @@
 
 	void Resolver::postvisit( FunctionDecl *functionDecl ) {
-		// default value expressions have an environment which shouldn't be there and trips up later passes.
-		// xxx - it might be necessary to somehow keep the information from this environment, but I can't currently
-		// see how it's useful.
+		// default value expressions have an environment which shouldn't be there and trips up 
+		// later passes.
+		// xxx - it might be necessary to somehow keep the information from this environment, but I 
+		// can't currently see how it's useful.
 		for ( Declaration * d : functionDecl->type->parameters ) {
 			if ( ObjectDecl * obj = dynamic_cast< ObjectDecl * >( d ) ) {
@@ -750,10 +795,12 @@
 		initExpr->expr = nullptr;
 		std::swap( initExpr->env, newExpr->env );
-		// InitExpr may have inferParams in the case where the expression specializes a function pointer,
-		// and newExpr may already have inferParams of its own, so a simple swap is not sufficient.
+		// InitExpr may have inferParams in the case where the expression specializes a function 
+		// pointer, and newExpr may already have inferParams of its own, so a simple swap is not 
+		// sufficient.
 		newExpr->spliceInferParams( initExpr );
 		delete initExpr;
 
-		// get the actual object's type (may not exactly match what comes back from the resolver due to conversions)
+		// get the actual object's type (may not exactly match what comes back from the resolver 
+		// due to conversions)
 		Type * initContext = currentObject.getCurrentType();
 
@@ -767,5 +814,6 @@
 					if ( isCharType( pt->get_base() ) ) {
 						if ( CastExpr *ce = dynamic_cast< CastExpr * >( newExpr ) ) {
-							// strip cast if we're initializing a char[] with a char *, e.g.  char x[] = "hello";
+							// strip cast if we're initializing a char[] with a char *, 
+							// e.g.  char x[] = "hello";
 							newExpr = ce->get_arg();
 							ce->set_arg( nullptr );
@@ -789,9 +837,10 @@
 		// move cursor into brace-enclosed initializer-list
 		currentObject.enterListInit();
-		// xxx - fix this so that the list isn't copied, iterator should be used to change current element
+		// xxx - fix this so that the list isn't copied, iterator should be used to change current 
+		// element
 		std::list<Designation *> newDesignations;
 		for ( auto p : group_iterate(listInit->get_designations(), listInit->get_initializers()) ) {
-			// iterate designations and initializers in pairs, moving the cursor to the current designated object and resolving
-			// the initializer against that object.
+			// iterate designations and initializers in pairs, moving the cursor to the current 
+			// designated object and resolving the initializer against that object.
 			Designation * des = std::get<0>(p);
 			Initializer * init = std::get<1>(p);
@@ -823,7 +872,7 @@
 		// fall back on C-style initializer
 		delete ctorInit->get_ctor();
-		ctorInit->set_ctor( NULL );
+		ctorInit->set_ctor( nullptr );
 		delete ctorInit->get_dtor();
-		ctorInit->set_dtor( NULL );
+		ctorInit->set_dtor( nullptr );
 		maybeAccept( ctorInit->get_init(), *visitor );
 	}
@@ -868,9 +917,9 @@
 
 		// xxx - todo -- what about arrays?
-		// if ( dtor == NULL && InitTweak::isIntrinsicCallStmt( ctorInit->get_ctor() ) ) {
+		// if ( dtor == nullptr && InitTweak::isIntrinsicCallStmt( ctorInit->get_ctor() ) ) {
 		// 	// can reduce the constructor down to a SingleInit using the
 		// 	// second argument from the ctor call, since
 		// 	delete ctorInit->get_ctor();
-		// 	ctorInit->set_ctor( NULL );
+		// 	ctorInit->set_ctor( nullptr );
 
 		// 	Expression * arg =
Index: src/ResolvExpr/TypeEnvironment.h
===================================================================
--- src/ResolvExpr/TypeEnvironment.h	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/TypeEnvironment.h	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -68,4 +68,9 @@
 	typedef std::map< DeclarationWithType*, AssertionSetValue, AssertCompare > AssertionSet;
 	typedef std::map< std::string, TypeDecl::Data > OpenVarSet;
+
+	/// merges one set of open vars into another
+	static inline void mergeOpenVars( OpenVarSet& dst, const OpenVarSet& src ) {
+		for ( const auto& entry : src ) { dst[ entry.first ] = entry.second; }
+	}
 
 	void printAssertionSet( const AssertionSet &, std::ostream &, int indent = 0 );
Index: src/ResolvExpr/module.mk
===================================================================
--- src/ResolvExpr/module.mk	(revision 59cf83bb18e6a60a3e089277ac400b992f2a16c2)
+++ src/ResolvExpr/module.mk	(revision da4818339a1056832238bbf1af3a1252de5a2ed3)
@@ -34,3 +34,4 @@
        ResolvExpr/CurrentObject.cc \
        ResolvExpr/ExplodedActual.cc \
-       ResolvExpr/SpecCost.cc
+       ResolvExpr/SpecCost.cc \
+       ResolvExpr/ResolveAssertions.cc
