Index: doc/theses/aaron_moss_PhD/phd/background.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/background.tex	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ doc/theses/aaron_moss_PhD/phd/background.tex	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -213,5 +213,5 @@
 The ability of types to begin or cease to satisfy traits when declarations go into or out of scope makes caching of trait satisfaction judgements difficult, and the ability of traits to take multiple type parameters can lead to a combinatorial explosion of work in any attempt to pre-compute trait satisfaction relationships. 
 
-\subsection{Implicit Conversions}
+\subsection{Implicit Conversions} \label{implicit-conv-sec}
 
 In addition to the multiple interpretations of an expression produced by name overloading and polymorphic functions, for backward compatibility \CFA{} must support all of the implicit conversions present in C, producing further candidate interpretations for expressions. 
Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -2,5 +2,14 @@
 \label{resolution-chap}
 
-Talk about the resolution heuristics. This is the bulk of the thesis.
+The main task of the \CFACC{} type-checker is \emph{expression resolution}, determining which declarations the identifiers in each expression correspond to. 
+Resolution is a straightforward task in C, as each declaration has a unique identifier, but in \CFA{} the name overloading features discussed in Section~\ref{overloading-sec} generate multiple candidate declarations for each identifier.
+I refer to a given matching between identifiers and declarations in an expression as an \emph{interpretation}; an interpretation also includes information about polymorphic type bindings and implicit casts to support the \CFA{} features discussed in Sections~\ref{poly-func-sec} and~\ref{implicit-conv-sec}, each of which increase the proportion of feasible candidate interpretations. 
+To choose between feasible interpretations, \CFA{} defines a \emph{conversion cost} to rank interpretations; the expression resolution problem is thus to find the unique minimal-cost interpretation for an expression, reporting an error if no such interpretation exists.
+
+\section{Conversion Cost}
+
+
 
 % Discuss changes to cost model, as promised in Ch. 2
+
+% Mention relevance of work to C++20 concepts
Index: driver/cfa.cc
===================================================================
--- driver/cfa.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ driver/cfa.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -10,6 +10,6 @@
 // Created On       : Tue Aug 20 13:44:49 2002
 // Last Modified By : Peter A. Buhr
-// Last Modified On : Fri Sep 14 23:02:59 2018
-// Update Count     : 277
+// Last Modified On : Tue Jan 15 20:56:03 2019
+// Update Count     : 280
 //
 
@@ -384,4 +384,9 @@
 	nargs += 1;
 
+	for ( int i = 0; i < nlibs; i += 1 ) {				// copy non-user libraries after all user libraries
+		args[nargs] = libs[i];
+		nargs += 1;
+	} // for
+
 	if ( link ) {
 		args[nargs] = "-Xlinker";
@@ -414,4 +419,6 @@
 		nargs += 1;
 		args[nargs] = "-lrt";
+		nargs += 1;
+		args[nargs] = "-lm";
 		nargs += 1;
 	} // if
@@ -498,15 +505,8 @@
 		args[nargs] = ( *new string( string("-B") + Bprefix ) ).c_str();
 		nargs += 1;
-		args[nargs] = "-lm";
-		nargs += 1;
 	} else {
 		cerr << argv[0] << " error, compiler \"" << compiler_name << "\" unsupported." << endl;
 		exit( EXIT_FAILURE );
 	} // if
-
-	for ( int i = 0; i < nlibs; i += 1 ) {				// copy non-user libraries after all user libraries
-		args[nargs] = libs[i];
-		nargs += 1;
-	} // for
 
 	args[nargs] = NULL;									// terminate with NULL
Index: libcfa/src/concurrency/coroutine.cfa
===================================================================
--- libcfa/src/concurrency/coroutine.cfa	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ libcfa/src/concurrency/coroutine.cfa	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -83,5 +83,5 @@
 
 void ^?{}(coroutine_desc& this) {
-      if(this.state != Halted) {
+      if(this.state != Halted && this.state != Start) {
             coroutine_desc * src = TL_GET( this_coroutine );
             coroutine_desc * dst = &this;
Index: src/Concurrency/Keywords.cc
===================================================================
--- src/Concurrency/Keywords.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/Concurrency/Keywords.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -575,5 +575,5 @@
 
 		//in reverse order :
-		// monitor_guard_t __guard = { __monitors, #, func };
+		// monitor_dtor_guard_t __guard = { __monitors, func };
 		body->push_front(
 			new DeclStmt( new ObjectDecl(
@@ -634,5 +634,5 @@
 		assert(generic_func);
 
-		//in reverse order :
+		// in reverse order :
 		// monitor_guard_t __guard = { __monitors, #, func };
 		body->push_front(
Index: src/Concurrency/Waitfor.cc
===================================================================
--- src/Concurrency/Waitfor.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/Concurrency/Waitfor.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -66,33 +66,34 @@
 void foo() {
 	while( true ) {
-
-		acceptable_t acceptables[3];
-		if( a < 1 ) {
-			acceptables[0].func = f;
-			acceptables[0].mon = a;
-		}
-		acceptables[1].func = g;
-		acceptables[1].mon = a;
-
-		acceptables[2].func = f;
-		acceptables[2].mon = a;
-		acceptables[2].is_dtor = true;
-
-		int ret = waitfor_internal( acceptables, swagl() );
-
-		switch( ret ) {
-			case 0:
-			{
-				bar();
+		{
+			acceptable_t acceptables[3];
+			if( a < 1 ) {
+				acceptables[0].func = f;
+				acceptables[0].mon = a;
 			}
-			case 1:
-			{
-				baz();
+			acceptables[1].func = g;
+			acceptables[1].mon = a;
+
+			acceptables[2].func = f;
+			acceptables[2].mon = a;
+			acceptables[2].is_dtor = true;
+
+			int ret = waitfor_internal( acceptables, swagl() );
+
+			switch( ret ) {
+				case 0:
+				{
+					bar();
+				}
+				case 1:
+				{
+					baz();
+				}
+				case 2:
+					signal(a);
+					{
+						break;
+					}
 			}
-			case 2:
-				signal(a);
-				{
-					break;
-				}
 		}
 	}
@@ -555,9 +556,11 @@
 					new ConstantExpr( Constant::from_ulong( i++ ) ),
 					{
-						clause.statement,
-						new BranchStmt(
-							"",
-							BranchStmt::Break
-						)
+						new CompoundStmt({
+							clause.statement,
+							new BranchStmt(
+								"",
+								BranchStmt::Break
+							)
+						})
 					}
 				)
@@ -570,9 +573,11 @@
 					new ConstantExpr( Constant::from_int( -2 ) ),
 					{
-						waitfor->timeout.statement,
-						new BranchStmt(
-							"",
-							BranchStmt::Break
-						)
+						new CompoundStmt({
+							waitfor->timeout.statement,
+							new BranchStmt(
+								"",
+								BranchStmt::Break
+							)
+						})
 					}
 				)
@@ -585,9 +590,11 @@
 					new ConstantExpr( Constant::from_int( -1 ) ),
 					{
-						waitfor->orelse.statement,
-						new BranchStmt(
-							"",
-							BranchStmt::Break
-						)
+						new CompoundStmt({
+							waitfor->orelse.statement,
+							new BranchStmt(
+								"",
+								BranchStmt::Break
+							)
+						})
 					}
 				)
Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -474,8 +474,11 @@
 		}
 
-		// mark specialization cost of return types
-		for ( DeclarationWithType* returnVal : function->returnVals ) {
-			convCost.decSpec( specCost( returnVal->get_type() ) );
-		}
+		// specialization cost of return types can't be accounted for directly, it disables 
+		// otherwise-identical calls, like this example based on auto-newline in the I/O lib:
+		//
+		//   forall(otype OS) {
+		//     void ?|?(OS&, int);  // with newline
+		//     OS&  ?|?(OS&, int);  // no newline, always chosen due to more specialization
+		//   }
 
 		// mark type variable and specialization cost of forall clause
@@ -483,9 +486,4 @@
 		for ( TypeDecl* td : function->forall ) {
 			convCost.decSpec( td->assertions.size() );
-		}
-
-		// xxx -- replace with new costs in resolver
-		for ( InferredParams::const_iterator assert = appExpr->inferParams.begin(); assert != appExpr->inferParams.end(); ++assert ) {
-			convCost += computeConversionCost( assert->second.actualType, assert->second.formalType, indexer, alt.env );
 		}
 
@@ -1229,5 +1227,5 @@
 				Alternative newAlt{ 
 					restructureCast( alt.expr->clone(), toType, castExpr->isGenerated ), 
-					alt.env, openVars, needAssertions, alt.cost + thisCost, thisCost };
+					alt.env, openVars, needAssertions, alt.cost, alt.cost + thisCost };
 				inferParameters( newAlt, back_inserter( candidates ) );
 			} // if
Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -20,4 +20,5 @@
 #include <list>                     // for list
 #include <memory>                   // for unique_ptr
+#include <string>
 #include <unordered_map>            // for unordered_map, unordered_multimap
 #include <utility>                  // for move
@@ -55,8 +56,26 @@
 	using CandidateList = std::vector<AssnCandidate>;
 
+	/// Unique identifier for a yet-to-be-resolved assertion
+	struct AssnId {
+		DeclarationWithType* decl;  ///< Declaration of assertion
+		AssertionSetValue info;     ///< Information about assertion
+
+		AssnId(DeclarationWithType* decl, const AssertionSetValue& info) : decl(decl), info(info) {}
+	};
+
+	/// Cached assertion items
+	struct AssnCacheItem {
+		CandidateList matches;         ///< Possible matches for this assertion
+		std::vector<AssnId> deferIds;  ///< Deferred assertions which resolve to this item
+
+		AssnCacheItem( CandidateList&& m ) : matches(std::move(m)), deferIds() {}
+	};
+
+	/// Cache of resolved assertions
+	using AssnCache = std::unordered_map<std::string, AssnCacheItem>;
+
 	/// Reference to single deferred item
 	struct DeferRef {
-		const DeclarationWithType* decl;
-		const AssertionSetValue& info;
+		const AssnCacheItem& item;
 		const AssnCandidate& match;
 	};
@@ -65,17 +84,23 @@
 	/// 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] }; }
+		const AssnCache* cache;     ///< Cache storing assertion item
+		std::string key;            ///< Key into cache
+		
+		DeferItem( const AssnCache& cache, const std::string& key ) : cache(&cache), key(key) {}
+
+		bool empty() const { return cache->at(key).matches.empty(); }
+
+		CandidateList::size_type size() const { return cache->at(key).matches.size(); }
+
+		DeferRef operator[] ( unsigned i ) const {
+			const AssnCacheItem& item = cache->at(key);
+			return { item, item.matches[i] };
+		}
+
+		// sortable by key
+		// TODO look into optimizing combination process with other sort orders (e.g. by number 
+		// of matches in candidate)
+		bool operator< ( const DeferItem& o ) const { return key < o.key; }
+		bool operator== ( const DeferItem& o ) const { return key == o.key; }
 	};
 
@@ -152,5 +177,6 @@
 				for ( const auto& assn : x.assns ) {
 					k += computeConversionCost( 
-						assn.match.adjType, assn.decl->get_type(), indexer, x.env );
+						assn.match.adjType, assn.item.deferIds[0].decl->get_type(), indexer, 
+						x.env );
 				}
 				it = cache.emplace_hint( it, &x, k );
@@ -208,22 +234,11 @@
 				candidate->get_uniqueId(), match.adjType->clone(), decl->get_type()->clone(), 
 				varExpr };
-
-		// // 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()->clone(), 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 );
+		for ( auto&  i : assertSet ) {
+			if ( i.second.isUsed ) {
+				indexer.addId( i.first );
 			}
 		}
@@ -234,48 +249,54 @@
 
 	/// Resolve a single assertion, in context
-	bool resolveAssertion( AssertionItem& assn, ResnState& resn ) {
+	bool resolveAssertion( AssertionItem& assn, ResnState& resn, AssnCache& cache ) {
 		// 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 );
-			renameTyVars( adjType );
-
-			// keep unifying candidates
-			if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 
-					resn.indexer ) ) {
-				// set up binding slot for recursive assertions
-				UniqueId crntResnSlot = 0;
-				if ( ! newNeed.empty() ) {
-					crntResnSlot = ++globalResnSlot;
-					for ( auto& a : newNeed ) {
-						a.second.resnSlot = crntResnSlot;
+		// check cache for this assertion
+		std::string assnKey = SymTab::Mangler::mangleAssnKey( assn.decl, resn.alt.env );
+		auto it = cache.find( assnKey );
+
+		// attempt to resolve assertion if this is the first time seen
+		if ( it == cache.end() ) {
+			// 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 );
+				renameTyVars( adjType );
+
+				// keep unifying candidates
+				if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 
+						resn.indexer ) ) {
+					// set up binding slot for recursive assertions
+					UniqueId crntResnSlot = 0;
+					if ( ! newNeed.empty() ) {
+						crntResnSlot = ++globalResnSlot;
+						for ( auto& a : newNeed ) {
+							a.second.resnSlot = crntResnSlot;
+						}
 					}
-				}
-				// // set up idChain on new assertions
-				// for ( auto& a : newNeed ) {
-				// 	a.second.idChain = assn.info.idChain;
-				// 	a.second.idChain.push_back( assn.decl->get_uniqueId() );
-				// }
-
-				matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 
-					std::move(newNeed), std::move(newOpenVars), crntResnSlot );
-			} else {
-				delete adjType;
+
+					matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 
+						std::move(newNeed), std::move(newOpenVars), crntResnSlot );
+				} else {
+					delete adjType;
+				}
 			}
-		}
+
+			it = cache.emplace_hint( it, assnKey, AssnCacheItem{ std::move(matches) } );
+		}
+
+		CandidateList& matches = it->second.matches;
 
 		// break if no suitable assertion
@@ -284,5 +305,6 @@
 		// defer if too many suitable assertions
 		if ( matches.size() > 1 ) {
-			resn.deferred.emplace_back( assn.decl, assn.info, std::move(matches) );
+			it->second.deferIds.emplace_back( assn.decl, assn.info );
+			resn.deferred.emplace_back( cache, assnKey );
 			return true;
 		}
@@ -292,6 +314,6 @@
 		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);
+		resn.alt.env = match.env;
+		resn.alt.openVars = match.openVars;
 
 		bindAssertion( assn.decl, assn.info, resn.alt, match, resn.inferred );
@@ -354,4 +376,5 @@
 		ResnList resns{ ResnState{ alt, root_indexer } };
 		ResnList new_resns{};
+		AssnCache assnCache;
 
 		// resolve assertions in breadth-first-order up to a limited number of levels deep
@@ -362,5 +385,5 @@
 				for ( auto& assn : resn.need ) {
 					// fail early if any assertion is not resolvable
-					if ( ! resolveAssertion( assn, resn ) ) goto nextResn;
+					if ( ! resolveAssertion( assn, resn, assnCache ) ) goto nextResn;
 				}
 
@@ -373,4 +396,8 @@
 					}
 				} else {
+					// only resolve each deferred assertion once
+					std::sort( resn.deferred.begin(), resn.deferred.end() );
+					auto last = std::unique( resn.deferred.begin(), resn.deferred.end() );
+					resn.deferred.erase( last, resn.deferred.end() );
 					// resolve deferred assertions by mutual compatibility
 					std::vector<CandidateEnvMerger::OutType> compatible = filterCombos(
@@ -380,10 +407,4 @@
 					CandidateCost coster{ resn.indexer };
 					std::sort( compatible.begin(), compatible.end(), coster );
-					// // sort by cost if pruning
-					// if ( pruneAssertions ) {
-					// 	auto lmin = sort_mins( compatible.begin(), compatible.end(), 
-					// 		CandidateCost{resn.indexer} );
-					// 	compatible.erase( lmin, compatible.end() );
-					// }
 
 					// keep map of detected options
@@ -408,5 +429,9 @@
 							new_resn.newNeed.insert( match.need.begin(), match.need.end() );
 
-							bindAssertion( r.decl, r.info, new_resn.alt, match, new_resn.inferred );
+							// for each deferred assertion with the same form
+							for ( AssnId id : r.item.deferIds ) {
+								bindAssertion( 
+									id.decl, id.info, new_resn.alt, match, new_resn.inferred );
+							}
 						}
 
Index: src/SymTab/Mangler.cc
===================================================================
--- src/SymTab/Mangler.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/SymTab/Mangler.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -15,19 +15,20 @@
 #include "Mangler.h"
 
-#include <algorithm>                // for copy, transform
-#include <cassert>                  // for assert, assertf
-#include <functional>               // for const_mem_fun_t, mem_fun
-#include <iterator>                 // for ostream_iterator, back_insert_ite...
-#include <list>                     // for _List_iterator, list, _List_const...
-#include <string>                   // for string, char_traits, operator<<
-
-#include "CodeGen/OperatorTable.h"  // for OperatorInfo, operatorLookup
+#include <algorithm>                     // for copy, transform
+#include <cassert>                       // for assert, assertf
+#include <functional>                    // for const_mem_fun_t, mem_fun
+#include <iterator>                      // for ostream_iterator, back_insert_ite...
+#include <list>                          // for _List_iterator, list, _List_const...
+#include <string>                        // for string, char_traits, operator<<
+
+#include "CodeGen/OperatorTable.h"       // for OperatorInfo, operatorLookup
 #include "Common/PassVisitor.h"
-#include "Common/SemanticError.h"   // for SemanticError
-#include "Common/utility.h"         // for toString
-#include "Parser/LinkageSpec.h"     // for Spec, isOverridable, AutoGen, Int...
-#include "SynTree/Declaration.h"    // for TypeDecl, DeclarationWithType
-#include "SynTree/Expression.h"     // for TypeExpr, Expression, operator<<
-#include "SynTree/Type.h"           // for Type, ReferenceToType, Type::Fora...
+#include "Common/SemanticError.h"        // for SemanticError
+#include "Common/utility.h"              // for toString
+#include "Parser/LinkageSpec.h"          // for Spec, isOverridable, AutoGen, Int...
+#include "ResolvExpr/TypeEnvironment.h"  // for TypeEnvironment
+#include "SynTree/Declaration.h"         // for TypeDecl, DeclarationWithType
+#include "SynTree/Expression.h"          // for TypeExpr, Expression, operator<<
+#include "SynTree/Type.h"                // for Type, ReferenceToType, Type::Fora...
 
 namespace SymTab {
@@ -37,4 +38,5 @@
 			struct Mangler : public WithShortCircuiting, public WithVisitorRef<Mangler>, public WithGuards {
 				Mangler( bool mangleOverridable, bool typeMode, bool mangleGenericParams );
+				Mangler( const ResolvExpr::TypeEnvironment& env );
 				Mangler( const Mangler & ) = delete;
 
@@ -65,7 +67,8 @@
 			  private:
 				std::ostringstream mangleName;  ///< Mangled name being constructed
-				typedef std::map< std::string, std::pair< int, int > > VarMapType;
+				typedef std::map< std::string, std::pair< std::string, int > > VarMapType;
 				VarMapType varNums;             ///< Map of type variables to indices
 				int nextVarNum;                 ///< Next type variable index
+				const ResolvExpr::TypeEnvironment* env;  ///< optional environment for substitutions
 				bool isTopLevel;                ///< Is the Mangler at the top level
 				bool mangleOverridable;         ///< Specially mangle overridable built-in methods
@@ -75,4 +78,10 @@
 				bool inQualifiedType = false;   ///< Add start/end delimiters around qualified type
 
+			  public:
+				Mangler( bool mangleOverridable, bool typeMode, bool mangleGenericParams, 
+					int nextVarNum, const ResolvExpr::TypeEnvironment* env, 
+					const VarMapType& varNums );
+
+			  private:
 				void mangleDecl( DeclarationWithType *declaration );
 				void mangleRef( ReferenceToType *refType, std::string prefix );
@@ -100,7 +109,27 @@
 		}
 
+		std::string mangleAssnKey( DeclarationWithType* decl, 
+				const ResolvExpr::TypeEnvironment& env ) {
+			PassVisitor<Mangler> mangler( env );
+			maybeAccept( decl, mangler );
+			return mangler.pass.get_mangleName();
+		}
+
 		namespace {
 			Mangler::Mangler( bool mangleOverridable, bool typeMode, bool mangleGenericParams )
-				: nextVarNum( 0 ), isTopLevel( true ), mangleOverridable( mangleOverridable ), typeMode( typeMode ), mangleGenericParams( mangleGenericParams ) {}
+				: nextVarNum( 0 ), env(nullptr), isTopLevel( true ), 
+				mangleOverridable( mangleOverridable ), typeMode( typeMode ), 
+				mangleGenericParams( mangleGenericParams ) {}
+			
+			Mangler::Mangler( const ResolvExpr::TypeEnvironment& env )
+				: nextVarNum( 0 ), env( &env ), isTopLevel( true ), mangleOverridable( false ),
+				typeMode( false ), mangleGenericParams( true ) {}
+			
+			Mangler::Mangler( bool mangleOverridable, bool typeMode, bool mangleGenericParams, 
+				int nextVarNum, const ResolvExpr::TypeEnvironment* env, 
+				const VarMapType& varNums )
+				: varNums( varNums ), nextVarNum( nextVarNum ), env( env ), isTopLevel( false ), 
+				mangleOverridable( mangleOverridable ), typeMode( typeMode ), 
+				mangleGenericParams( mangleGenericParams ) {}
 
 			void Mangler::mangleDecl( DeclarationWithType * declaration ) {
@@ -329,12 +358,27 @@
 							assert( false );
 						} // switch
-						varNums[ (*i)->name ] = std::pair< int, int >( nextVarNum++, (int)(*i)->get_kind() );
+						std::string varName;
+						// replace type with substitution name if environment is available and bound
+						if ( env ) {
+							const ResolvExpr::EqvClass* varClass = env->lookup( (*i)->name );
+							if ( varClass && varClass->type ) {
+								PassVisitor<Mangler> sub_mangler(
+									mangleOverridable, typeMode, mangleGenericParams, nextVarNum, 
+									env, varNums );
+								varClass->type->accept( sub_mangler );
+								varName = std::string{"%"} + sub_mangler.pass.get_mangleName();
+							}
+						}
+						// otherwise just give type numeric name
+						if ( varName.empty() ) {
+							varName = std::to_string( nextVarNum++ );
+						}
+						varNums[ (*i)->name ] = std::make_pair( varName, (int)(*i)->get_kind() );
 						for ( std::list< DeclarationWithType* >::iterator assert = (*i)->assertions.begin(); assert != (*i)->assertions.end(); ++assert ) {
-							PassVisitor<Mangler> sub_mangler( mangleOverridable, typeMode, mangleGenericParams );
-							sub_mangler.pass.nextVarNum = nextVarNum;
-							sub_mangler.pass.isTopLevel = false;
-							sub_mangler.pass.varNums = varNums;
+							PassVisitor<Mangler> sub_mangler( 
+								mangleOverridable, typeMode, mangleGenericParams, nextVarNum, env, 
+								varNums );
 							(*assert)->accept( sub_mangler );
-							assertionNames.push_back( sub_mangler.pass.mangleName.str() );
+							assertionNames.push_back( sub_mangler.pass.get_mangleName() );
 							acount++;
 						} // for
Index: src/SymTab/Mangler.h
===================================================================
--- src/SymTab/Mangler.h	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/SymTab/Mangler.h	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -31,4 +31,8 @@
 // * Currently name compression is not implemented.
 
+namespace ResolvExpr {
+	class TypeEnvironment;
+}
+
 namespace SymTab {
 	namespace Mangler {
@@ -40,4 +44,7 @@
 		/// Mangle ignoring generic type parameters
 		std::string mangleConcrete( Type* ty );
+		/// Mangle for assertion key
+		std::string mangleAssnKey( DeclarationWithType* decl, 
+			const ResolvExpr::TypeEnvironment& env );
 
 		namespace Encoding {
Index: src/main.cc
===================================================================
--- src/main.cc	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ src/main.cc	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -10,6 +10,6 @@
 // Created On       : Fri May 15 23:12:02 2015
 // Last Modified By : Peter A. Buhr
-// Last Modified On : Wed Jun  6 15:51:47 2018
-// Update Count     : 498
+// Last Modified On : Wed Dec 26 08:11:19 2018
+// Update Count     : 499
 //
 
@@ -371,5 +371,5 @@
 			}
 		} catch(const std::exception& e) {
-			std::cerr << "Unaught Exception \"" << e.what() << "\"\n";
+			std::cerr << "Uncaught Exception \"" << e.what() << "\"\n";
 		}
 		return 1;
Index: tests/abort.cfa
===================================================================
--- tests/abort.cfa	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
+++ tests/abort.cfa	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+int level3() {
+	abort();
+	return 0;
+}
+
+int level2() {
+	return level3();
+}
+
+int level1() {
+	return level2();
+}
+
+int main() {
+	return level1();
+}
Index: tests/pybin/print-core.gdb
===================================================================
--- tests/pybin/print-core.gdb	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
+++ tests/pybin/print-core.gdb	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -0,0 +1,4 @@
+echo -----\n
+where
+echo -----\n
+info threads
Index: tests/pybin/tools.py
===================================================================
--- tests/pybin/tools.py	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ tests/pybin/tools.py	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -3,11 +3,13 @@
 import __main__
 import argparse
+import fileinput
 import multiprocessing
 import os
 import re
+import resource
 import signal
 import stat
 import sys
-import fileinput
+import time
 
 from pybin import settings
@@ -131,7 +133,21 @@
 
     return None
+
+def run(exe, output, input):
+	ret, _ = sh("timeout %d %s > %s 2>&1" % (settings.timeout.single, exe, output), input = input)
+	return ret
+
 ################################################################################
 #               file handling
 ################################################################################
+# move a file
+def mv(source, dest):
+	ret, _ = sh("mv %s %s" % (source, dest))
+	return ret
+
+# cat one file into the other
+def cat(source, dest):
+	ret, _ = sh("cat %s > %s" % (source, dest))
+	return ret
 
 # helper function to replace patterns in a file
@@ -230,4 +246,8 @@
 		signal.signal(signal.SIGINT, signal.SIG_IGN)
 
+
+# enable core dumps for all the test children
+resource.setrlimit(resource.RLIMIT_CORE, (resource.RLIM_INFINITY, resource.RLIM_INFINITY))
+
 ################################################################################
 #               misc
@@ -251,2 +271,27 @@
 	else:
 		print(text)
+
+
+def coreInfo(path):
+	cmd   = os.path.join(settings.SRCDIR, "pybin/print-core.gdb")
+	if not os.path.isfile(cmd):
+		return 1, "ERR Printing format for core dumps not found"
+
+	dname = os.path.dirname(path)
+	core  = os.path.join(dname, "core" )
+	if not os.path.isfile(path):
+		return 1, "ERR Executable path is wrong"
+
+	if not os.path.isfile(core):
+		return 1, "ERR No core dump"
+
+	return sh("gdb -n %s %s -batch -x %s" % (path, core, cmd), print2stdout=False)
+
+class Timed:
+    def __enter__(self):
+        self.start = time.time()
+        return self
+
+    def __exit__(self, *args):
+        self.end = time.time()
+        self.duration = self.end - self.start
Index: tests/test.py
===================================================================
--- tests/test.py	(revision af433943323d50f0d9edd0b0afb33131386c326f)
+++ tests/test.py	(revision 1d832f4bfb43313e3f83a1b5e2db90f7b3c6cf30)
@@ -121,11 +121,12 @@
 #               running test functions
 ################################################################################
-# fix the absolute paths in the output
-def fixoutput( fname ):
-	if not is_ascii(fname):
-		return
-
-	file_replace(fname, "%s/" % settings.SRCDIR, "")
-
+def success(val):
+	return val == 0 or settings.dry_run
+
+def isExe(file):
+	return settings.dry_run or fileIsExecutable(file)
+
+def noRule(file, target):
+	return not settings.dry_run and fileContainsOnly(file, "make: *** No rule to make target `%s'.  Stop." % target)
 
 # logic to run a single test and return the result (No handling of printing or other test framework logic)
@@ -143,39 +144,27 @@
 
 	# build, skipping to next test on error
-	before = time.time()
-	make_ret, _ = make( test.target(),
-		redirects  = "2> %s 1> /dev/null" % out_file,
-		error_file = err_file
-	)
-	after = time.time()
-
-	comp_dur = after - before
-
+	with Timed() as comp_dur:
+		make_ret, _ = make( test.target(), 	redirects  = ("2> %s 1> /dev/null" % out_file), error_file = err_file )
+
+	# if the make command succeds continue otherwise skip to diff
 	run_dur = None
-
-	# if the make command succeds continue otherwise skip to diff
-	if make_ret == 0 or settings.dry_run:
-		before = time.time()
-		if settings.dry_run or fileIsExecutable(exe_file) :
-			# run test
-			retcode, _ = sh("timeout %d %s > %s 2>&1" % (settings.timeout.single, exe_file, out_file), input = in_file)
-		else :
-			# simply cat the result into the output
-			retcode, _ = sh("cat %s > %s" % (exe_file, out_file))
-
-		after = time.time()
-		run_dur = after - before
+	if success(make_ret):
+		with Timed() as run_dur:
+			if isExe(exe_file):
+				# run test
+				retcode = run(exe_file, out_file, in_file)
+			else :
+				# simply cat the result into the output
+				retcode = cat(exe_file, out_file)
 	else:
-		retcode, _ = sh("mv %s %s" % (err_file, out_file))
-
-
-	if retcode == 0:
-		# fixoutput(out_file)
+		retcode = mv(err_file, out_file)
+
+	if success(retcode):
 		if settings.generating :
 			# if we are ounly generating the output we still need to check that the test actually exists
-			if not settings.dry_run and fileContainsOnly(out_file, "make: *** No rule to make target `%s'.  Stop." % test.target()) :
-				retcode = 1;
+			if noRule(out_file, test.target()) :
+				retcode = 1
 				error = "\t\tNo make target for test %s!" % test.target()
-				sh("rm %s" % out_file, False)
+				rm(out_file)
 			else:
 				error = None
@@ -188,9 +177,13 @@
 			error = myfile.read()
 
+		ret, info = coreInfo(exe_file)
+		error = error + info
+
+
 
 	# clean the executable
-	sh("rm -f %s > /dev/null 2>&1" % test.target())
-
-	return retcode, error, [comp_dur, run_dur]
+	rm(exe_file)
+
+	return retcode, error, [comp_dur.duration, run_dur.duration if run_dur else None]
 
 # run a single test and handle the errors, outputs, printing, exception handling, etc.
@@ -199,5 +192,5 @@
 	with SignalHandling():
 		# print formated name
-		name_txt = "%20s  " % t.name
+		name_txt = "%24s  " % t.name
 
 		retcode, error, duration = run_single_test(t)
@@ -263,4 +256,5 @@
 	allTests = listTests( options.include, options.exclude )
 
+
 	# if user wants all tests than no other treatement of the test list is required
 	if options.all or options.list or options.list_comp or options.include :
