Index: src/Makefile.in
===================================================================
--- src/Makefile.in	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/Makefile.in	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -203,4 +203,5 @@
 	ResolvExpr/Resolver.$(OBJEXT) \
 	ResolvExpr/ResolveTypeof.$(OBJEXT) \
+	ResolvExpr/SatisfyAssertions.$(OBJEXT) \
 	ResolvExpr/SpecCost.$(OBJEXT) \
 	ResolvExpr/TypeEnvironment.$(OBJEXT) \
@@ -641,4 +642,5 @@
       ResolvExpr/Resolver.cc \
       ResolvExpr/ResolveTypeof.cc \
+      ResolvExpr/SatisfyAssertions.cpp \
       ResolvExpr/SpecCost.cc \
       ResolvExpr/TypeEnvironment.cc \
@@ -911,4 +913,6 @@
 ResolvExpr/ResolveTypeof.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
 	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
+ResolvExpr/SatisfyAssertions.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
+	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
 ResolvExpr/SpecCost.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
 	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
@@ -1282,4 +1286,5 @@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/ResolveTypeof.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/Resolver.Po@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/SatisfyAssertions.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/SpecCost.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/TypeEnvironment.Po@am__quote@
Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -266,5 +266,5 @@
 			SemanticError( expr, "No reasonable alternatives for expression " );
 		}
-		if ( mode.resolveAssns || mode.prune ) {
+		if ( mode.satisfyAssns || mode.prune ) {
 			// trim candidates just to those where the assertions resolve
 			// - necessary pre-requisite to pruning
Index: src/ResolvExpr/CandidateFinder.cpp
===================================================================
--- src/ResolvExpr/CandidateFinder.cpp	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/CandidateFinder.cpp	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -16,12 +16,115 @@
 #include "CandidateFinder.hpp"
 
+#include <sstream>
+
+#include "Candidate.hpp"
+#include "CompilationState.h"
+#include "SatisfyAssertions.hpp"
 #include "AST/Expr.hpp"
+#include "AST/Node.hpp"
+#include "AST/Pass.hpp"
+
+#define PRINT( text ) if ( resolvep ) { text }
 
 namespace ResolvExpr {
 
+namespace {
+
+	/// Actually visits expressions to find their candidate interpretations
+	struct Finder {
+		CandidateFinder & candFinder;
+		const ast::SymbolTable & symtab;
+		CandidateList & candidates;
+		const ast::TypeEnvironment & tenv;
+		ast::ptr< ast::Type > & targetType;
+
+		Finder( CandidateFinder & f )
+		: candFinder( f ), symtab( f.symtab ), candidates( f.candidates ), tenv( f.env ), 
+		  targetType( f.targetType ) {}
+		
+		#warning unimplemented
+	};
+
+	/// Prunes a list of candidates down to those that have the minimum conversion cost for a given 
+	/// return type. Skips ambiguous candidates.
+	CandidateList pruneCandidates( CandidateList & candidates ) {
+		#warning unimplemented
+		(void)candidates;
+		assert(false);
+		return {};
+	}
+
+} // anonymous namespace
+
 void CandidateFinder::find( const ast::Expr * expr, ResolvMode mode ) {
+	// Find alternatives for expression
+	ast::Pass<Finder> finder{ *this };
+	expr->accept( finder );
+
+	if ( mode.failFast && candidates.empty() ) {
+		SemanticError( expr, "No reasonable alternatives for expression " );
+	}
+
+	if ( mode.satisfyAssns || mode.prune ) {
+		// trim candidates to just those where the assertions are satisfiable
+		// - necessary pre-requisite to pruning
+		CandidateList satisfied;
+		std::vector< std::string > errors;
+		for ( auto & candidate : candidates ) {
+			satisfyAssertions( *candidate, symtab, satisfied, errors );
+		}
+
+		// fail early if none such
+		if ( mode.failFast && satisfied.empty() ) {
+			std::ostringstream stream;
+			stream << "No alternatives with satisfiable assertions for " << expr << "\n";
+			for ( const auto& err : errors ) {
+				stream << err;
+			}
+			SemanticError( expr->location, stream.str() );
+		}
+
+		// reset candidates
+		candidates = std::move( satisfied );
+	}
+
+	if ( mode.prune ) {
+		// trim candidates to single best one
+		auto oldsize = candidates.size();
+		PRINT(
+			std::cerr << "alternatives before prune:" << std::endl;
+			print( std::cerr, candidates );
+		)
+
+		CandidateList pruned = pruneCandidates( candidates );
+		if ( mode.failFast && pruned.empty() ) {
+			std::ostringstream stream;
+			CandidateList winners;
+			
+			#warning unimplemented
+			assert(false);
+		}
+	}
+
 	#warning unimplemented
-	(void)expr; (void)mode;
 	assert(false);
+}
+
+std::vector< CandidateFinder > CandidateFinder::findSubExprs( 
+	const std::vector< ast::ptr< ast::Expr > > & xs 
+) {
+	std::vector< CandidateFinder > out;
+
+	for ( const auto & x : xs ) {
+		out.emplace_back( symtab, env );
+		out.back().find( x, ResolvMode::withAdjustment() );
+		
+		PRINT(
+			std::cerr << "findSubExprs" << std::endl;
+			print( std::cerr, out.back().candidates );
+		)
+	}
+
+	return out;
 }
 
Index: src/ResolvExpr/CandidateFinder.hpp
===================================================================
--- src/ResolvExpr/CandidateFinder.hpp	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/CandidateFinder.hpp	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -19,4 +19,5 @@
 #include "ResolvMode.h"
 #include "AST/Fwd.hpp"
+#include "AST/Node.hpp"
 #include "AST/SymbolTable.hpp"
 #include "AST/TypeEnvironment.hpp"
@@ -29,5 +30,5 @@
 	const ast::SymbolTable & symtab;         ///< Symbol table to lookup candidates
 	const ast::TypeEnvironment & env;        ///< Substitutions performed in this resolution
-	const ast::Type * targetType = nullptr;  ///< Target type for resolution
+	ast::ptr< ast::Type > targetType = nullptr;  ///< Target type for resolution
 
 	CandidateFinder( const ast::SymbolTable & symtab, const ast::TypeEnvironment & env )
@@ -36,4 +37,17 @@
 	/// Fill candidates with feasible resolutions for `expr`
 	void find( const ast::Expr * expr, ResolvMode mode = {} );
+
+	/// Runs new candidate finder on each element in xs, returning the list of finders
+	std::vector< CandidateFinder > findSubExprs( const std::vector< ast::ptr< ast::Expr > > & xs );
+
+	using value_type = CandidateList::value_type;
+	using iterator = CandidateList::iterator;
+	using const_iterator = CandidateList::const_iterator;
+
+	iterator begin() { return candidates.begin(); }
+	const_iterator begin() const { return candidates.begin(); }
+	
+	iterator end() { return candidates.end(); }
+	const_iterator end() const { return candidates.end(); }
 };
 
Index: src/ResolvExpr/ResolvMode.h
===================================================================
--- src/ResolvExpr/ResolvMode.h	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/ResolvMode.h	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -22,13 +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 resolveAssns;     ///< Resolve assertions? [false]
+		const bool satisfyAssns;     ///< Satisfy assertions? [false]
 
 	private:
-		constexpr ResolvMode(bool a, bool p, bool ff, bool ra) 
-		: adjust(a), prune(p), failFast(ff), resolveAssns(ra) {}
+		constexpr ResolvMode(bool a, bool p, bool ff, bool sa) 
+		: adjust(a), prune(p), failFast(ff), satisfyAssns(sa) {}
 
 	public:
 		/// Default settings
-		constexpr ResolvMode() : adjust(false), prune(true), failFast(true), resolveAssns(false) {}
+		constexpr ResolvMode() : adjust(false), prune(true), failFast(true), satisfyAssns(false) {}
 		
 		/// With adjust flag set; turns array and function types into equivalent pointers
@@ -43,5 +43,5 @@
 		static constexpr ResolvMode withoutFailFast() { return { true, true, false, false }; }
 
-		/// The same mode, but with resolveAssns turned on; for top-level calls
+		/// The same mode, but with satisfyAssns turned on; for top-level calls
 		ResolvMode atTopLevel() const { return { adjust, prune, failFast, true }; }
 	};
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/Resolver.cc	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -35,4 +35,5 @@
 #include "AST/Print.hpp"
 #include "AST/SymbolTable.hpp"
+#include "AST/Type.hpp"
 #include "Common/PassVisitor.h"          // for PassVisitor
 #include "Common/SemanticError.h"        // for SemanticError
@@ -1146,4 +1147,11 @@
 		}
 
+		/// Resolve `untyped` to the single expression whose candidate is the best match
+		ast::ptr< ast::Expr > findSingleExpression( 
+			const ast::Expr * untyped, const ast::SymbolTable & symtab 
+		) {
+			return findKindExpression( untyped, symtab );
+		}
+
 		/// Resolve `untyped` to the single expression whose candidate is the best match for the 
 		/// given type.
@@ -1152,6 +1160,6 @@
 		) {
 			assert( untyped && type );
-			const ast::Expr * castExpr = new ast::CastExpr{ untyped->location, untyped, type };
-			ast::ptr< ast::Expr > newExpr = findKindExpression( castExpr, symtab );
+			ast::ptr< ast::Expr > castExpr = new ast::CastExpr{ untyped->location, untyped, type };
+			ast::ptr< ast::Expr > newExpr = findSingleExpression( castExpr, symtab );
 			removeExtraneousCast( newExpr, symtab );
 			return newExpr;
@@ -1189,4 +1197,11 @@
 			return false;
 		}
+
+		/// Advance a type itertor to the next mutex parameter
+		template<typename Iter>
+		inline bool nextMutex( Iter & it, const Iter & end ) {
+			while ( it != end && ! (*it)->get_type()->is_mutex() ) { ++it; }
+			return it != end;
+		}
 	}
 
@@ -1213,17 +1228,17 @@
 		void previsit( const ast::PointerType * );
 
-		const ast::ExprStmt *   previsit( const ast::ExprStmt * );
-		const ast::AsmExpr *    previsit( const ast::AsmExpr * );
-		const ast::AsmStmt *    previsit( const ast::AsmStmt * );
-		const ast::IfStmt *     previsit( const ast::IfStmt * );
-		const ast::WhileStmt *  previsit( const ast::WhileStmt * );
-		const ast::ForStmt *    previsit( const ast::ForStmt * );
-		const ast::SwitchStmt * previsit( const ast::SwitchStmt * );
-		const ast::CaseStmt *   previsit( const ast::CaseStmt * );
-		const ast::BranchStmt * previsit( const ast::BranchStmt * );
-		const ast::ReturnStmt * previsit( const ast::ReturnStmt * );
-		const ast::ThrowStmt *  previsit( const ast::ThrowStmt * );
-		const ast::CatchStmt *  previsit( const ast::CatchStmt * );
-		void previsit( const ast::WaitForStmt * );
+		const ast::ExprStmt *        previsit( const ast::ExprStmt * );
+		const ast::AsmExpr *         previsit( const ast::AsmExpr * );
+		const ast::AsmStmt *         previsit( const ast::AsmStmt * );
+		const ast::IfStmt *          previsit( const ast::IfStmt * );
+		const ast::WhileStmt *       previsit( const ast::WhileStmt * );
+		const ast::ForStmt *         previsit( const ast::ForStmt * );
+		const ast::SwitchStmt *      previsit( const ast::SwitchStmt * );
+		const ast::CaseStmt *        previsit( const ast::CaseStmt * );
+		const ast::BranchStmt *      previsit( const ast::BranchStmt * );
+		const ast::ReturnStmt *      previsit( const ast::ReturnStmt * );
+		const ast::ThrowStmt *       previsit( const ast::ThrowStmt * );
+		const ast::CatchStmt *       previsit( const ast::CatchStmt * );
+		const ast::WaitForStmt *     previsit( const ast::WaitForStmt * );
 
 		const ast::SingleInit *      previsit( const ast::SingleInit * );
@@ -1381,7 +1396,7 @@
 				"expression." );
 			
-			const ast::Expr * untyped = 
+			ast::ptr< ast::Expr > untyped = 
 				new ast::CastExpr{ caseStmt->location, caseStmt->cond, initAlts.front().type };
-			ast::ptr< ast::Expr > newExpr = findKindExpression( untyped, symtab );
+			ast::ptr< ast::Expr > newExpr = findSingleExpression( untyped, symtab );
 			
 			// case condition cannot have a cast in C, so it must be removed here, regardless of 
@@ -1401,9 +1416,8 @@
 		if ( branchStmt->kind == ast::BranchStmt::Goto && branchStmt->computedTarget ) {
 			// computed goto argument is void*
+			ast::ptr< ast::Type > target = new ast::PointerType{ new ast::VoidType{} };
 			branchStmt = ast::mutate_field(
 				branchStmt, &ast::BranchStmt::computedTarget, 
-				findSingleExpression( 
-					branchStmt->computedTarget, new ast::PointerType{ new ast::VoidType{} }, 
-					symtab ) );
+				findSingleExpression( branchStmt->computedTarget, target, symtab ) );
 		}
 		return branchStmt;
@@ -1445,8 +1459,254 @@
 	}
 
-	void Resolver_new::previsit( const ast::WaitForStmt * stmt ) {
-		#warning unimplemented; Resolver port in progress
-		(void)stmt;
-		assert(false);
+	const ast::WaitForStmt * Resolver_new::previsit( const ast::WaitForStmt * stmt ) {
+		visit_children = false;
+
+		// Resolve all clauses first
+		for ( unsigned i = 0; i < stmt->clauses.size(); ++i ) {
+			const ast::WaitForStmt::Clause & clause = stmt->clauses[i];
+
+			ast::TypeEnvironment env;
+			CandidateFinder funcFinder{ symtab, env };
+
+			// Find all candidates for a function in canonical form
+			funcFinder.find( clause.target.func, ResolvMode::withAdjustment() );
+
+			if ( funcFinder.candidates.empty() ) {
+				stringstream ss;
+				ss << "Use of undeclared indentifier '";
+				ss << clause.target.func.strict_as< ast::NameExpr >()->name;
+				ss << "' in call to waitfor";
+				SemanticError( stmt->location, ss.str() );
+			}
+
+			if ( clause.target.args.empty() ) {
+				SemanticError( stmt->location, 
+					"Waitfor clause must have at least one mutex parameter");
+			}
+
+			// Find all alternatives for all arguments in canonical form
+			std::vector< CandidateFinder > argFinders = 
+				funcFinder.findSubExprs( clause.target.args );
+			
+			// List all combinations of arguments
+			std::vector< CandidateList > possibilities;
+			combos( argFinders.begin(), argFinders.end(), back_inserter( possibilities ) );
+
+			// For every possible function:
+			// * try matching the arguments to the parameters, not the other way around because 
+			//   more arguments than parameters
+			CandidateList funcCandidates;
+			std::vector< CandidateList > argsCandidates;
+			SemanticErrorException errors;
+			for ( CandidateRef & func : funcFinder.candidates ) {
+				try {
+					auto pointerType = dynamic_cast< const ast::PointerType * >( 
+						func->expr->result->stripReferences() );
+					if ( ! pointerType ) {
+						SemanticError( stmt->location, func->expr->result.get(), 
+							"candidate not viable: not a pointer type\n" );
+					}
+
+					auto funcType = pointerType->base.as< ast::FunctionType >();
+					if ( ! funcType ) {
+						SemanticError( stmt->location, func->expr->result.get(), 
+							"candidate not viable: not a function type\n" );
+					}
+
+					{
+						auto param    = funcType->params.begin();
+						auto paramEnd = funcType->params.end();
+
+						if( ! nextMutex( param, paramEnd ) ) {
+							SemanticError( stmt->location, funcType, 
+								"candidate function not viable: no mutex parameters\n");
+						}
+					}
+
+					CandidateRef func2{ new Candidate{ *func } };
+					// strip reference from function
+					func2->expr = referenceToRvalueConversion( func->expr, func2->cost );
+
+					// Each argument must be matched with a parameter of the current candidate
+					for ( auto & argsList : possibilities ) {
+						try {
+							// Declare data structures needed for resolution
+							ast::OpenVarSet open;
+							ast::AssertionSet need, have;
+							ast::TypeEnvironment resultEnv{ func->env };
+							// Add all type variables as open so that those not used in the 
+							// parameter list are still considered open
+							resultEnv.add( funcType->forall );
+
+							// load type variables from arguments into one shared space
+							for ( auto & arg : argsList ) {
+								resultEnv.simpleCombine( arg->env );
+							}
+
+							// Make sure we don't widen any existing bindings
+							resultEnv.forbidWidening();
+
+							// Find any unbound type variables
+							resultEnv.extractOpenVars( open );
+
+							auto param = funcType->params.begin();
+							auto paramEnd = funcType->params.end();
+
+							unsigned n_mutex_param = 0;
+
+							// For every argument of its set, check if it matches one of the 
+							// parameters. The order is important
+							for ( auto & arg : argsList ) {
+								// Ignore non-mutex arguments
+								if ( ! nextMutex( param, paramEnd ) ) {
+									// We ran out of parameters but still have arguments.
+									// This function doesn't match
+									SemanticError( stmt->location, funcType, 
+										toString("candidate function not viable: too many mutex "
+										"arguments, expected ", n_mutex_param, "\n" ) );
+								}
+
+								++n_mutex_param;
+
+								// Check if the argument matches the parameter type in the current 
+								// scope
+								ast::ptr< ast::Type > paramType = (*param)->get_type();
+								if ( 
+									! unify( 
+										arg->expr->result, paramType, resultEnv, need, have, open, 
+										symtab ) 
+								) {
+									// Type doesn't match
+									stringstream ss;
+									ss << "candidate function not viable: no known conversion "
+										"from '";
+									ast::print( ss, (*param)->get_type() );
+									ss << "' to '";
+									ast::print( ss, arg->expr->result );
+									ss << "' with env '";
+									ast::print( ss, resultEnv );
+									ss << "'\n";
+									SemanticError( stmt->location, funcType, ss.str() );
+								}
+
+								++param;
+							}
+
+							// All arguments match!
+
+							// Check if parameters are missing
+							if ( nextMutex( param, paramEnd ) ) {
+								do {
+									++n_mutex_param;
+									++param;
+								} while ( nextMutex( param, paramEnd ) );
+
+								// We ran out of arguments but still have parameters left; this 
+								// function doesn't match
+								SemanticError( stmt->location, funcType, 
+									toString( "candidate function not viable: too few mutex "
+									"arguments, expected ", n_mutex_param, "\n" ) );
+							}
+
+							// All parameters match!
+
+							// Finish the expressions to tie in proper environments
+							finishExpr( func2->expr, resultEnv );
+							for ( CandidateRef & arg : argsList ) {
+								finishExpr( arg->expr, resultEnv );
+							}
+
+							// This is a match, store it and save it for later
+							funcCandidates.emplace_back( std::move( func2 ) );
+							argsCandidates.emplace_back( std::move( argsList ) );
+
+						} catch ( SemanticErrorException & e ) {
+							errors.append( e );
+						}
+					}
+				} catch ( SemanticErrorException & e ) {
+					errors.append( e );
+				}
+			}
+
+			// Make sure correct number of arguments
+			if( funcCandidates.empty() ) {
+				SemanticErrorException top( stmt->location, 
+					"No alternatives for function in call to waitfor" );
+				top.append( errors );
+				throw top;
+			}
+
+			if( argsCandidates.empty() ) {
+				SemanticErrorException top( stmt->location, 
+					"No alternatives for arguments in call to waitfor" ); 
+				top.append( errors );
+				throw top;
+			}
+
+			if( funcCandidates.size() > 1 ) {
+				SemanticErrorException top( stmt->location, 
+					"Ambiguous function in call to waitfor" );
+				top.append( errors );
+				throw top;
+			}
+			if( argsCandidates.size() > 1 ) {
+				SemanticErrorException top( stmt->location,
+					"Ambiguous arguments in call to waitfor" );
+				top.append( errors );
+				throw top;
+			}
+			// TODO: need to use findDeletedExpr to ensure no deleted identifiers are used.
+
+			// build new clause
+			ast::WaitForStmt::Clause clause2;
+			
+			clause2.target.func = funcCandidates.front()->expr;
+			
+			clause2.target.args.reserve( clause.target.args.size() );
+			for ( auto arg : argsCandidates.front() ) {
+				clause2.target.args.emplace_back( std::move( arg->expr ) );
+			}
+
+			// Resolve the conditions as if it were an IfStmt, statements normally
+			clause2.cond = findSingleExpression( clause.cond, symtab );
+			clause2.stmt = clause.stmt->accept( *visitor );
+
+			// set results into stmt
+			auto n = mutate( stmt );
+			n->clauses[i] = std::move( clause2 );
+			stmt = n;
+		}
+
+		if ( stmt->timeout.stmt ) {
+			// resolve the timeout as a size_t, the conditions like IfStmt, and stmts normally
+			ast::WaitForStmt::Timeout timeout2;
+
+			ast::ptr< ast::Type > target = 
+				new ast::BasicType{ ast::BasicType::LongLongUnsignedInt };
+			timeout2.time = findSingleExpression( stmt->timeout.time, target, symtab );
+			timeout2.cond = findSingleExpression( stmt->timeout.cond, symtab );
+			timeout2.stmt = stmt->timeout.stmt->accept( *visitor );
+
+			// set results into stmt
+			auto n = mutate( stmt );
+			n->timeout = std::move( timeout2 );
+			stmt = n;
+		}
+
+		if ( stmt->orElse.stmt ) {
+			// resolve the condition like IfStmt, stmts normally
+			ast::WaitForStmt::OrElse orElse2;
+
+			orElse2.cond = findSingleExpression( stmt->orElse.cond, symtab );
+			orElse2.stmt = stmt->orElse.stmt->accept( *visitor );
+
+			// set results into stmt
+			auto n = mutate( stmt );
+			n->orElse = std::move( orElse2 );
+			stmt = n;
+		}
+
+		return stmt;
 	}
 
@@ -1457,7 +1717,7 @@
 		// resolve initialization using the possibilities as determined by the `currentObject` 
 		// cursor.
-		ast::Expr * untyped = new ast::UntypedInitExpr{ 
+		ast::ptr< ast::Expr > untyped = new ast::UntypedInitExpr{ 
 			singleInit->location, singleInit->value, currentObject.getOptions() };
-		ast::ptr<ast::Expr> newExpr = findKindExpression( untyped, symtab );
+		ast::ptr<ast::Expr> newExpr = findSingleExpression( untyped, symtab );
 		const ast::InitExpr * initExpr = newExpr.strict_as< ast::InitExpr >();
 
Index: src/ResolvExpr/SatisfyAssertions.cpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.cpp	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
+++ src/ResolvExpr/SatisfyAssertions.cpp	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -0,0 +1,37 @@
+//
+// 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.
+//
+// SatisfyAssertions.cpp --
+//
+// Author           : Aaron B. Moss
+// Created On       : Mon Jun 10 17:45:00 2019
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Mon Jun 10 17:45:00 2019
+// Update Count     : 1
+//
+
+#include "SatisfyAssertions.hpp"
+
+#include <cassert>
+
+namespace ResolvExpr {
+
+void satisfyAssertions( 
+	Candidate & alt, const ast::SymbolTable & symtab, CandidateList & out, 
+	std::vector<std::string> & errors
+) {
+	#warning unimplemented
+	(void)alt; (void)symtab; (void)out; (void)errors;
+	assert(false);
+}
+
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/SatisfyAssertions.hpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.hpp	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
+++ src/ResolvExpr/SatisfyAssertions.hpp	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -0,0 +1,40 @@
+//
+// 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.
+//
+// SatisfyAssertions.hpp --
+//
+// Author           : Aaron B. Moss
+// Created On       : Mon Jun 10 17:45:00 2019
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Mon Jun 10 17:45:00 2019
+// Update Count     : 1
+//
+
+#pragma once
+
+#include <string>
+#include <vector>
+
+#include "Candidate.hpp"  // for Candidate, CandidateList
+
+namespace ast {
+	class SymbolTable;
+}
+
+namespace ResolvExpr {
+
+/// Recursively satisfies all assertions provided in a candidate; returns true if succeeds
+void satisfyAssertions( 
+	Candidate & alt, const ast::SymbolTable & symtab, CandidateList & out, 
+	std::vector<std::string> & errors );
+
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/Unify.cc
===================================================================
--- src/ResolvExpr/Unify.cc	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/Unify.cc	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -1143,4 +1143,13 @@
 			const ast::ptr<ast::Type> & type1, const ast::ptr<ast::Type> & type2, 
 			ast::TypeEnvironment & env, ast::AssertionSet & need, ast::AssertionSet & have, 
+			ast::OpenVarSet & open, const ast::SymbolTable & symtab
+	) {
+		ast::ptr<ast::Type> common;
+		return unify( type1, type2, env, need, have, open, symtab, common );
+	}
+
+	bool unify( 
+			const ast::ptr<ast::Type> & type1, const ast::ptr<ast::Type> & type2, 
+			ast::TypeEnvironment & env, ast::AssertionSet & need, ast::AssertionSet & have, 
 			ast::OpenVarSet & open, const ast::SymbolTable & symtab, ast::ptr<ast::Type> & common 
 	) {
Index: src/ResolvExpr/Unify.h
===================================================================
--- src/ResolvExpr/Unify.h	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/Unify.h	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -72,4 +72,9 @@
 		const ast::ptr<ast::Type> & type1, const ast::ptr<ast::Type> & type2, 
 		ast::TypeEnvironment & env, ast::AssertionSet & need, ast::AssertionSet & have, 
+		ast::OpenVarSet & open, const ast::SymbolTable & symtab );
+
+	bool unify( 
+		const ast::ptr<ast::Type> & type1, const ast::ptr<ast::Type> & type2, 
+		ast::TypeEnvironment & env, ast::AssertionSet & need, ast::AssertionSet & have, 
 		ast::OpenVarSet & open, const ast::SymbolTable & symtab, ast::ptr<ast::Type> & common );
 
Index: src/ResolvExpr/module.mk
===================================================================
--- src/ResolvExpr/module.mk	(revision b32627728210f82121049430d14a1cd3280a3994)
+++ src/ResolvExpr/module.mk	(revision 6ad19fdc923abd4817508c234b4db0cadde59dbd)
@@ -35,4 +35,5 @@
       ResolvExpr/Resolver.cc \
       ResolvExpr/ResolveTypeof.cc \
+      ResolvExpr/SatisfyAssertions.cpp \
       ResolvExpr/SpecCost.cc \
       ResolvExpr/TypeEnvironment.cc \