Merge pull request #3261 from ethereum/develop

Merge develop into release for 0.4.19

41 files changed, 1293 insertions, 234 deletions

diff --git a/libsolidity/analysis/ConstantEvaluator.cpp b/libsolidity/analysis/ConstantEvaluator.cpp
index 6636ad97..4d546e68 100644
--- a/libsolidity/analysis/ConstantEvaluator.cpp
+++ b/libsolidity/analysis/ConstantEvaluator.cpp
@@ -28,6 +28,7 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
+/// FIXME: this is pretty much a copy of TypeChecker::endVisit(BinaryOperation)
 void ConstantEvaluator::endVisit(UnaryOperation const& _operation)
 {
 	TypePointer const& subType = _operation.subExpression().annotation().type;
@@ -37,6 +38,7 @@ void ConstantEvaluator::endVisit(UnaryOperation const& _operation)
 	_operation.annotation().type = t;
 }
 
+/// FIXME: this is pretty much a copy of TypeChecker::endVisit(BinaryOperation)
 void ConstantEvaluator::endVisit(BinaryOperation const& _operation)
 {
 	TypePointer const& leftType = _operation.leftExpression().annotation().type;
@@ -46,9 +48,24 @@ void ConstantEvaluator::endVisit(BinaryOperation const& _operation)
 	if (!dynamic_cast<RationalNumberType const*>(rightType.get()))
 		m_errorReporter.fatalTypeError(_operation.rightExpression().location(), "Invalid constant expression.");
 	TypePointer commonType = leftType->binaryOperatorResult(_operation.getOperator(), rightType);
-	if (Token::isCompareOp(_operation.getOperator()))
-		commonType = make_shared<BoolType>();
-	_operation.annotation().type = commonType;
+	if (!commonType)
+	{
+		m_errorReporter.typeError(
+			_operation.location(),
+			"Operator " +
+			string(Token::toString(_operation.getOperator())) +
+			" not compatible with types " +
+			leftType->toString() +
+			" and " +
+			rightType->toString()
+		);
+		commonType = leftType;
+	}
+	_operation.annotation().commonType = commonType;
+	_operation.annotation().type =
+		Token::isCompareOp(_operation.getOperator()) ?
+		make_shared<BoolType>() :
+		commonType;
 }
 
 void ConstantEvaluator::endVisit(Literal const& _literal)
@@ -57,3 +74,25 @@ void ConstantEvaluator::endVisit(Literal const& _literal)
 	if (!_literal.annotation().type)
 		m_errorReporter.fatalTypeError(_literal.location(), "Invalid literal value.");
 }
+
+void ConstantEvaluator::endVisit(Identifier const& _identifier)
+{
+	VariableDeclaration const* variableDeclaration = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration);
+	if (!variableDeclaration)
+		return;
+	if (!variableDeclaration->isConstant())
+		m_errorReporter.fatalTypeError(_identifier.location(), "Identifier must be declared constant.");
+
+	ASTPointer<Expression> value = variableDeclaration->value();
+	if (!value)
+		m_errorReporter.fatalTypeError(_identifier.location(), "Constant identifier declaration must have a constant value.");
+
+	if (!value->annotation().type)
+	{
+		if (m_depth > 32)
+			m_errorReporter.fatalTypeError(_identifier.location(), "Cyclic constant definition (or maximum recursion depth exhausted).");
+		ConstantEvaluator e(*value, m_errorReporter, m_depth + 1);
+	}
+
+	_identifier.annotation().type = value->annotation().type;
+}
diff --git a/libsolidity/analysis/ConstantEvaluator.h b/libsolidity/analysis/ConstantEvaluator.h
index 90bceb5d..6725d610 100644
--- a/libsolidity/analysis/ConstantEvaluator.h
+++ b/libsolidity/analysis/ConstantEvaluator.h
@@ -38,8 +38,9 @@ class TypeChecker;
 class ConstantEvaluator: private ASTConstVisitor
 {
 public:
-	ConstantEvaluator(Expression const& _expr, ErrorReporter& _errorReporter):
-		m_errorReporter(_errorReporter)
+	ConstantEvaluator(Expression const& _expr, ErrorReporter& _errorReporter, size_t _newDepth = 0):
+		m_errorReporter(_errorReporter),
+		m_depth(_newDepth)
 	{
 		_expr.accept(*this);
 	}
@@ -48,8 +49,11 @@ private:
 	virtual void endVisit(BinaryOperation const& _operation);
 	virtual void endVisit(UnaryOperation const& _operation);
 	virtual void endVisit(Literal const& _literal);
+	virtual void endVisit(Identifier const& _identifier);
 
 	ErrorReporter& m_errorReporter;
+	/// Current recursion depth.
+	size_t m_depth;
 };
 
 }
diff --git a/libsolidity/analysis/PostTypeChecker.h b/libsolidity/analysis/PostTypeChecker.h
index 91d2b0b9..bafc1ae6 100644
--- a/libsolidity/analysis/PostTypeChecker.h
+++ b/libsolidity/analysis/PostTypeChecker.h
@@ -38,7 +38,7 @@ class ErrorReporter;
 class PostTypeChecker: private ASTConstVisitor
 {
 public:
-	/// @param _errors the reference to the list of errors and warnings to add them found during type checking.
+	/// @param _errorReporter provides the error logging functionality.
 	PostTypeChecker(ErrorReporter& _errorReporter): m_errorReporter(_errorReporter) {}
 
 	bool check(ASTNode const& _astRoot);
diff --git a/libsolidity/analysis/StaticAnalyzer.cpp b/libsolidity/analysis/StaticAnalyzer.cpp
index ffa538b6..bd8ee597 100644
--- a/libsolidity/analysis/StaticAnalyzer.cpp
+++ b/libsolidity/analysis/StaticAnalyzer.cpp
@@ -150,10 +150,18 @@ bool StaticAnalyzer::visit(MemberAccess const& _memberAccess)
 	if (_memberAccess.memberName() == "callcode")
 		if (auto const* type = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type.get()))
 			if (type->kind() == FunctionType::Kind::BareCallCode)
-				m_errorReporter.warning(
-					_memberAccess.location(),
-					"\"callcode\" has been deprecated in favour of \"delegatecall\"."
-				);
+			{
+				if (m_currentContract->sourceUnit().annotation().experimentalFeatures.count(ExperimentalFeature::V050))
+					m_errorReporter.typeError(
+						_memberAccess.location(),
+						"\"callcode\" has been deprecated in favour of \"delegatecall\"."
+					);
+				else
+					m_errorReporter.warning(
+						_memberAccess.location(),
+						"\"callcode\" has been deprecated in favour of \"delegatecall\"."
+					);
+			}
 
 	if (m_constructor && m_currentContract)
 		if (ContractType const* type = dynamic_cast<ContractType const*>(_memberAccess.expression().annotation().type.get()))
diff --git a/libsolidity/analysis/StaticAnalyzer.h b/libsolidity/analysis/StaticAnalyzer.h
index 24ed119f..124c4e7c 100644
--- a/libsolidity/analysis/StaticAnalyzer.h
+++ b/libsolidity/analysis/StaticAnalyzer.h
@@ -43,7 +43,7 @@ namespace solidity
 class StaticAnalyzer: private ASTConstVisitor
 {
 public:
-	/// @param _errors the reference to the list of errors and warnings to add them found during static analysis.
+	/// @param _errorReporter provides the error logging functionality.
 	explicit StaticAnalyzer(ErrorReporter& _errorReporter): m_errorReporter(_errorReporter) {}
 
 	/// Performs static analysis on the given source unit and all of its sub-nodes.
diff --git a/libsolidity/analysis/SyntaxChecker.cpp b/libsolidity/analysis/SyntaxChecker.cpp
index 0ca4b86c..b6cc04da 100644
--- a/libsolidity/analysis/SyntaxChecker.cpp
+++ b/libsolidity/analysis/SyntaxChecker.cpp
@@ -54,7 +54,7 @@ void SyntaxChecker::endVisit(SourceUnit const& _sourceUnit)
 				string(".") +
 				to_string(recommendedVersion.minor()) +
 				string(".") +
-				to_string(recommendedVersion.patch());
+				to_string(recommendedVersion.patch()) +
 				string(";\"");
 
 		m_errorReporter.warning(_sourceUnit.location(), errorString);
diff --git a/libsolidity/analysis/SyntaxChecker.h b/libsolidity/analysis/SyntaxChecker.h
index 7fffbec0..d5d72f14 100644
--- a/libsolidity/analysis/SyntaxChecker.h
+++ b/libsolidity/analysis/SyntaxChecker.h
@@ -38,7 +38,7 @@ namespace solidity
 class SyntaxChecker: private ASTConstVisitor
 {
 public:
-	/// @param _errors the reference to the list of errors and warnings to add them found during type checking.
+	/// @param _errorReporter provides the error logging functionality.
 	SyntaxChecker(ErrorReporter& _errorReporter): m_errorReporter(_errorReporter) {}
 
 	bool checkSyntax(ASTNode const& _astRoot);
diff --git a/libsolidity/analysis/TypeChecker.cpp b/libsolidity/analysis/TypeChecker.cpp
index 746e762e..73047e76 100644
--- a/libsolidity/analysis/TypeChecker.cpp
+++ b/libsolidity/analysis/TypeChecker.cpp
@@ -1122,7 +1122,7 @@ bool TypeChecker::visit(VariableDeclarationStatement const& _statement)
 						var.annotation().type->toString() +
 						". Try converting to type " +
 						valueComponentType->mobileType()->toString() +
-						" or use an explicit conversion." 
+						" or use an explicit conversion."
 					);
 				else
 					m_errorReporter.typeError(
@@ -1320,7 +1320,7 @@ bool TypeChecker::visit(TupleExpression const& _tuple)
 		_tuple.annotation().isPure = isPure;
 		if (_tuple.isInlineArray())
 		{
-			if (!inlineArrayType) 
+			if (!inlineArrayType)
 				m_errorReporter.fatalTypeError(_tuple.location(), "Unable to deduce common type for array elements.");
 			_tuple.annotation().type = make_shared<ArrayType>(DataLocation::Memory, inlineArrayType, types.size());
 		}
@@ -2000,7 +2000,9 @@ void TypeChecker::endVisit(Literal const& _literal)
 			m_errorReporter.warning(
 				_literal.location(),
 				"This looks like an address but has an invalid checksum. "
-				"If this is not used as an address, please prepend '00'."
+				"If this is not used as an address, please prepend '00'. " +
+				(!_literal.getChecksummedAddress().empty() ? "Correct checksummed address: '" + _literal.getChecksummedAddress() + "'. " : "") +
+				"For more information please see https://solidity.readthedocs.io/en/develop/types.html#address-literals"
 			);
 	}
 	if (!_literal.annotation().type)
diff --git a/libsolidity/analysis/TypeChecker.h b/libsolidity/analysis/TypeChecker.h
index abe6dac1..344b019d 100644
--- a/libsolidity/analysis/TypeChecker.h
+++ b/libsolidity/analysis/TypeChecker.h
@@ -42,7 +42,7 @@ class ErrorReporter;
 class TypeChecker: private ASTConstVisitor
 {
 public:
-	/// @param _errors the reference to the list of errors and warnings to add them found during type checking.
+	/// @param _errorReporter provides the error logging functionality.
 	TypeChecker(ErrorReporter& _errorReporter): m_errorReporter(_errorReporter) {}
 
 	/// Performs type checking on the given contract and all of its sub-nodes.
diff --git a/libsolidity/analysis/ViewPureChecker.cpp b/libsolidity/analysis/ViewPureChecker.cpp
index 7f28c7d2..7e41fc16 100644
--- a/libsolidity/analysis/ViewPureChecker.cpp
+++ b/libsolidity/analysis/ViewPureChecker.cpp
@@ -72,6 +72,11 @@ public:
 		for (auto const& arg: _funCall.arguments)
 			boost::apply_visitor(*this, arg);
 	}
+	void operator()(assembly::If const& _if)
+	{
+		boost::apply_visitor(*this, *_if.condition);
+		(*this)(_if.body);
+	}
 	void operator()(assembly::Switch const& _switch)
 	{
 		boost::apply_visitor(*this, *_switch.expression);
diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index 1048b610..8da6964e 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -583,3 +583,14 @@ bool Literal::passesAddressChecksum() const
 	solAssert(isHexNumber(), "Expected hex number");
 	return dev::passesAddressChecksum(value(), true);
 }
+
+std::string Literal::getChecksummedAddress() const
+{
+	solAssert(isHexNumber(), "Expected hex number");
+	/// Pad literal to be a proper hex address.
+	string address = value().substr(2);
+	if (address.length() > 40)
+		return string();
+	address.insert(address.begin(), 40 - address.size(), '0');
+	return dev::getChecksummedAddress(address);
+}
diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h
index 733e7c78..feffde64 100644
--- a/libsolidity/ast/AST.h
+++ b/libsolidity/ast/AST.h
@@ -1613,6 +1613,8 @@ public:
 	bool looksLikeAddress() const;
 	/// @returns true if it passes the address checksum test.
 	bool passesAddressChecksum() const;
+	/// @returns the checksummed version of an address (or empty string if not valid)
+	std::string getChecksummedAddress() const;
 
 private:
 	Token::Value m_token;
diff --git a/libsolidity/ast/ASTPrinter.cpp b/libsolidity/ast/ASTPrinter.cpp
index 81e6cc44..23c3cbe1 100644
--- a/libsolidity/ast/ASTPrinter.cpp
+++ b/libsolidity/ast/ASTPrinter.cpp
@@ -78,6 +78,13 @@ bool ASTPrinter::visit(InheritanceSpecifier const& _node)
 	return goDeeper();
 }
 
+bool ASTPrinter::visit(UsingForDirective const& _node)
+{
+	writeLine("UsingForDirective");
+	printSourcePart(_node);
+	return goDeeper();
+}
+
 bool ASTPrinter::visit(StructDefinition const& _node)
 {
 	writeLine("StructDefinition \"" + _node.name() + "\"");
@@ -385,6 +392,11 @@ void ASTPrinter::endVisit(InheritanceSpecifier const&)
 	m_indentation--;
 }
 
+void ASTPrinter::endVisit(UsingForDirective const&)
+{
+	m_indentation--;
+}
+
 void ASTPrinter::endVisit(StructDefinition const&)
 {
 	m_indentation--;
diff --git a/libsolidity/ast/ASTPrinter.h b/libsolidity/ast/ASTPrinter.h
index d6897dfd..01e4f7fc 100644
--- a/libsolidity/ast/ASTPrinter.h
+++ b/libsolidity/ast/ASTPrinter.h
@@ -51,6 +51,7 @@ public:
 	bool visit(ImportDirective const& _node) override;
 	bool visit(ContractDefinition const& _node) override;
 	bool visit(InheritanceSpecifier const& _node) override;
+	bool visit(UsingForDirective const& _node) override;
 	bool visit(StructDefinition const& _node) override;
 	bool visit(EnumDefinition const& _node) override;
 	bool visit(EnumValue const& _node) override;
@@ -94,6 +95,7 @@ public:
 	void endVisit(ImportDirective const&) override;
 	void endVisit(ContractDefinition const&) override;
 	void endVisit(InheritanceSpecifier const&) override;
+	void endVisit(UsingForDirective const&) override;
 	void endVisit(StructDefinition const&) override;
 	void endVisit(EnumDefinition const&) override;
 	void endVisit(EnumValue const&) override;
diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp
index ee5f462b..21daac2c 100644
--- a/libsolidity/ast/Types.cpp
+++ b/libsolidity/ast/Types.cpp
@@ -2574,7 +2574,7 @@ MemberList::MemberMap FunctionType::nativeMembers(ContractDefinition const*) con
 				"selector",
 				make_shared<FixedBytesType>(4)
 			));
-		if (m_kind != Kind::BareDelegateCall && m_kind != Kind::DelegateCall)
+		if (m_kind != Kind::BareDelegateCall)
 		{
 			if (isPayable())
 				members.push_back(MemberList::Member(
diff --git a/libsolidity/ast/Types.h b/libsolidity/ast/Types.h
index ce29975e..635279ab 100644
--- a/libsolidity/ast/Types.h
+++ b/libsolidity/ast/Types.h
@@ -707,10 +707,6 @@ public:
 	/// Returns the function type of the constructor modified to return an object of the contract's type.
 	FunctionTypePointer const& newExpressionType() const;
 
-	/// @returns the identifier of the function with the given name or Invalid256 if such a name does
-	/// not exist.
-	u256 functionIdentifier(std::string const& _functionName) const;
-
 	/// @returns a list of all state variables (including inherited) of the contract and their
 	/// offsets in storage.
 	std::vector<std::tuple<VariableDeclaration const*, u256, unsigned>> stateVariables() const;
diff --git a/libsolidity/codegen/ABIFunctions.cpp b/libsolidity/codegen/ABIFunctions.cpp
index 080be359..6648be06 100644
--- a/libsolidity/codegen/ABIFunctions.cpp
+++ b/libsolidity/codegen/ABIFunctions.cpp
@@ -22,9 +22,13 @@
 
 #include <libsolidity/codegen/ABIFunctions.h>
 
+#include <libsolidity/ast/AST.h>
+#include <libsolidity/codegen/CompilerUtils.h>
+
 #include <libdevcore/Whiskers.h>
 
-#include <libsolidity/ast/AST.h>
+#include <boost/algorithm/string/join.hpp>
+#include <boost/range/adaptor/reversed.hpp>
 
 using namespace std;
 using namespace dev;
@@ -99,6 +103,79 @@ string ABIFunctions::tupleEncoder(
 	});
 }
 
+string ABIFunctions::tupleDecoder(TypePointers const& _types, bool _fromMemory)
+{
+	string functionName = string("abi_decode_tuple_");
+	for (auto const& t: _types)
+		functionName += t->identifier();
+	if (_fromMemory)
+		functionName += "_fromMemory";
+
+	solAssert(!_types.empty(), "");
+
+	return createFunction(functionName, [&]() {
+		TypePointers decodingTypes;
+		for (auto const& t: _types)
+			decodingTypes.emplace_back(t->decodingType());
+
+		Whiskers templ(R"(
+			function <functionName>(headStart, dataEnd) -> <valueReturnParams> {
+				switch slt(sub(dataEnd, headStart), <minimumSize>) case 1 { revert(0, 0) }
+				<decodeElements>
+			}
+		)");
+		templ("functionName", functionName);
+		templ("minimumSize", to_string(headSize(decodingTypes)));
+
+		string decodeElements;
+		vector<string> valueReturnParams;
+		size_t headPos = 0;
+		size_t stackPos = 0;
+		for (size_t i = 0; i < _types.size(); ++i)
+		{
+			solAssert(_types[i], "");
+			solAssert(decodingTypes[i], "");
+			size_t sizeOnStack = _types[i]->sizeOnStack();
+			solAssert(sizeOnStack == decodingTypes[i]->sizeOnStack(), "");
+			solAssert(sizeOnStack > 0, "");
+			vector<string> valueNamesLocal;
+			for (size_t j = 0; j < sizeOnStack; j++)
+			{
+				valueNamesLocal.push_back("value" + to_string(stackPos));
+				valueReturnParams.push_back("value" + to_string(stackPos));
+				stackPos++;
+			}
+			bool dynamic = decodingTypes[i]->isDynamicallyEncoded();
+			Whiskers elementTempl(
+				dynamic ?
+				R"(
+				{
+					let offset := <load>(add(headStart, <pos>))
+					switch gt(offset, 0xffffffffffffffff) case 1 { revert(0, 0) }
+					<values> := <abiDecode>(add(headStart, offset), dataEnd)
+				}
+				)" :
+				R"(
+				{
+					let offset := <pos>
+					<values> := <abiDecode>(add(headStart, offset), dataEnd)
+				}
+				)"
+			);
+			elementTempl("load", _fromMemory ? "mload" : "calldataload");
+			elementTempl("values", boost::algorithm::join(valueNamesLocal, ", "));
+			elementTempl("pos", to_string(headPos));
+			elementTempl("abiDecode", abiDecodingFunction(*_types[i], _fromMemory, true));
+			decodeElements += elementTempl.render();
+			headPos += dynamic ? 0x20 : decodingTypes[i]->calldataEncodedSize();
+		}
+		templ("valueReturnParams", boost::algorithm::join(valueReturnParams, ", "));
+		templ("decodeElements", decodeElements);
+
+		return templ.render();
+	});
+}
+
 string ABIFunctions::requestedFunctions()
 {
 	string result;
@@ -141,10 +218,9 @@ string ABIFunctions::cleanupFunction(Type const& _type, bool _revertOnFailure)
 			solUnimplemented("Fixed point types not implemented.");
 			break;
 		case Type::Category::Array:
-			solAssert(false, "Array cleanup requested.");
-			break;
 		case Type::Category::Struct:
-			solAssert(false, "Struct cleanup requested.");
+			solAssert(_type.dataStoredIn(DataLocation::Storage), "Cleanup requested for non-storage reference type.");
+			templ("body", "cleaned := value");
 			break;
 		case Type::Category::FixedBytes:
 		{
@@ -168,7 +244,7 @@ string ABIFunctions::cleanupFunction(Type const& _type, bool _revertOnFailure)
 		{
 			size_t members = dynamic_cast<EnumType const&>(_type).numberOfMembers();
 			solAssert(members > 0, "empty enum should have caused a parser error.");
-			Whiskers w("switch lt(value, <members>) case 0 { <failure> } cleaned := value");
+			Whiskers w("if iszero(lt(value, <members>)) { <failure> } cleaned := value");
 			w("members", to_string(members));
 			if (_revertOnFailure)
 				w("failure", "revert(0, 0)");
@@ -367,6 +443,24 @@ string ABIFunctions::combineExternalFunctionIdFunction()
 	});
 }
 
+string ABIFunctions::splitExternalFunctionIdFunction()
+{
+	string functionName = "split_external_function_id";
+	return createFunction(functionName, [&]() {
+		return Whiskers(R"(
+			function <functionName>(combined) -> addr, selector {
+				combined := <shr64>(combined)
+				selector := and(combined, 0xffffffff)
+				addr := <shr32>(combined)
+			}
+		)")
+		("functionName", functionName)
+		("shr32", shiftRightFunction(32, false))
+		("shr64", shiftRightFunction(64, false))
+		.render();
+	});
+}
+
 string ABIFunctions::abiEncodingFunction(
 	Type const& _from,
 	Type const& _to,
@@ -483,7 +577,7 @@ string ABIFunctions::abiEncodingFunctionCalldataArray(
 		_to.identifier() +
 		(_encodeAsLibraryTypes ? "_library" : "");
 	return createFunction(functionName, [&]() {
-		solUnimplementedAssert(fromArrayType.isByteArray(), "");
+		solUnimplementedAssert(fromArrayType.isByteArray(), "Only byte arrays can be encoded from calldata currently.");
 		// TODO if this is not a byte array, we might just copy byte-by-byte anyway,
 		// because the encoding is position-independent, but we have to check that.
 		Whiskers templ(R"(
@@ -754,7 +848,7 @@ string ABIFunctions::abiEncodingFunctionStruct(
 		_to.identifier() +
 		(_encodeAsLibraryTypes ? "_library" : "");
 
-	solUnimplementedAssert(!_from.dataStoredIn(DataLocation::CallData), "");
+	solUnimplementedAssert(!_from.dataStoredIn(DataLocation::CallData), "Encoding struct from calldata is not yet supported.");
 	solAssert(&_from.structDefinition() == &_to.structDefinition(), "");
 
 	return createFunction(functionName, [&]() {
@@ -963,6 +1057,307 @@ string ABIFunctions::abiEncodingFunctionFunctionType(
 		});
 }
 
+string ABIFunctions::abiDecodingFunction(Type const& _type, bool _fromMemory, bool _forUseOnStack)
+{
+	// The decoding function has to perform bounds checks unless it decodes a value type.
+	// Conversely, bounds checks have to be performed before the decoding function
+	// of a value type is called.
+
+	TypePointer decodingType = _type.decodingType();
+	solAssert(decodingType, "");
+
+	if (auto arrayType = dynamic_cast<ArrayType const*>(decodingType.get()))
+	{
+		if (arrayType->dataStoredIn(DataLocation::CallData))
+		{
+			solAssert(!_fromMemory, "");
+			return abiDecodingFunctionCalldataArray(*arrayType);
+		}
+		else if (arrayType->isByteArray())
+			return abiDecodingFunctionByteArray(*arrayType, _fromMemory);
+		else
+			return abiDecodingFunctionArray(*arrayType, _fromMemory);
+	}
+	else if (auto const* structType = dynamic_cast<StructType const*>(decodingType.get()))
+		return abiDecodingFunctionStruct(*structType, _fromMemory);
+	else if (auto const* functionType = dynamic_cast<FunctionType const*>(decodingType.get()))
+		return abiDecodingFunctionFunctionType(*functionType, _fromMemory, _forUseOnStack);
+	else
+		return abiDecodingFunctionValueType(_type, _fromMemory);
+}
+
+string ABIFunctions::abiDecodingFunctionValueType(const Type& _type, bool _fromMemory)
+{
+	TypePointer decodingType = _type.decodingType();
+	solAssert(decodingType, "");
+	solAssert(decodingType->sizeOnStack() == 1, "");
+	solAssert(decodingType->isValueType(), "");
+	solAssert(decodingType->calldataEncodedSize() == 32, "");
+	solAssert(!decodingType->isDynamicallyEncoded(), "");
+
+	string functionName =
+		"abi_decode_" +
+		_type.identifier() +
+		(_fromMemory ? "_fromMemory" : "");
+	return createFunction(functionName, [&]() {
+		Whiskers templ(R"(
+			function <functionName>(offset, end) -> value {
+				value := <cleanup>(<load>(offset))
+			}
+		)");
+		templ("functionName", functionName);
+		templ("load", _fromMemory ? "mload" : "calldataload");
+		// Cleanup itself should use the type and not decodingType, because e.g.
+		// the decoding type of an enum is a plain int.
+		templ("cleanup", cleanupFunction(_type, true));
+		return templ.render();
+	});
+
+}
+
+string ABIFunctions::abiDecodingFunctionArray(ArrayType const& _type, bool _fromMemory)
+{
+	solAssert(_type.dataStoredIn(DataLocation::Memory), "");
+	solAssert(!_type.isByteArray(), "");
+
+	string functionName =
+		"abi_decode_" +
+		_type.identifier() +
+		(_fromMemory ? "_fromMemory" : "");
+
+	solAssert(!_type.dataStoredIn(DataLocation::Storage), "");
+
+	return createFunction(functionName, [&]() {
+		string load = _fromMemory ? "mload" : "calldataload";
+		bool dynamicBase = _type.baseType()->isDynamicallyEncoded();
+		Whiskers templ(
+			R"(
+				// <readableTypeName>
+				function <functionName>(offset, end) -> array {
+					switch slt(add(offset, 0x1f), end) case 0 { revert(0, 0) }
+					let length := <retrieveLength>
+					array := <allocate>(<allocationSize>(length))
+					let dst := array
+					<storeLength> // might update offset and dst
+					let src := offset
+					<staticBoundsCheck>
+					for { let i := 0 } lt(i, length) { i := add(i, 1) }
+					{
+						let elementPos := <retrieveElementPos>
+						mstore(dst, <decodingFun>(elementPos, end))
+						dst := add(dst, 0x20)
+						src := add(src, <baseEncodedSize>)
+					}
+				}
+			)"
+		);
+		templ("functionName", functionName);
+		templ("readableTypeName", _type.toString(true));
+		templ("retrieveLength", !_type.isDynamicallySized() ? toCompactHexWithPrefix(_type.length()) : load + "(offset)");
+		templ("allocate", allocationFunction());
+		templ("allocationSize", arrayAllocationSizeFunction(_type));
+		if (_type.isDynamicallySized())
+			templ("storeLength", "mstore(array, length) offset := add(offset, 0x20) dst := add(dst, 0x20)");
+		else
+			templ("storeLength", "");
+		if (dynamicBase)
+		{
+			templ("staticBoundsCheck", "");
+			templ("retrieveElementPos", "add(offset, " + load + "(src))");
+			templ("baseEncodedSize", "0x20");
+		}
+		else
+		{
+			string baseEncodedSize = toCompactHexWithPrefix(_type.baseType()->calldataEncodedSize());
+			templ("staticBoundsCheck", "switch gt(add(src, mul(length, " + baseEncodedSize + ")), end) case 1 { revert(0, 0) }");
+			templ("retrieveElementPos", "src");
+			templ("baseEncodedSize", baseEncodedSize);
+		}
+		templ("decodingFun", abiDecodingFunction(*_type.baseType(), _fromMemory, false));
+		return templ.render();
+	});
+}
+
+string ABIFunctions::abiDecodingFunctionCalldataArray(ArrayType const& _type)
+{
+	// This does not work with arrays of complex types - the array access
+	// is not yet implemented in Solidity.
+	solAssert(_type.dataStoredIn(DataLocation::CallData), "");
+	if (!_type.isDynamicallySized())
+		solAssert(_type.length() < u256("0xffffffffffffffff"), "");
+	solAssert(!_type.baseType()->isDynamicallyEncoded(), "");
+	solAssert(_type.baseType()->calldataEncodedSize() < u256("0xffffffffffffffff"), "");
+
+	string functionName =
+		"abi_decode_" +
+		_type.identifier();
+	return createFunction(functionName, [&]() {
+		string templ;
+		if (_type.isDynamicallySized())
+			templ = R"(
+				// <readableTypeName>
+				function <functionName>(offset, end) -> arrayPos, length {
+					switch slt(add(offset, 0x1f), end) case 0 { revert(0, 0) }
+					length := calldataload(offset)
+					switch gt(length, 0xffffffffffffffff) case 1 { revert(0, 0) }
+					arrayPos := add(offset, 0x20)
+					switch gt(add(arrayPos, mul(<length>, <baseEncodedSize>)), end) case 1 { revert(0, 0) }
+				}
+			)";
+		else
+			templ = R"(
+				// <readableTypeName>
+				function <functionName>(offset, end) -> arrayPos {
+					arrayPos := offset
+					switch gt(add(arrayPos, mul(<length>, <baseEncodedSize>)), end) case 1 { revert(0, 0) }
+				}
+			)";
+		Whiskers w{templ};
+		w("functionName", functionName);
+		w("readableTypeName", _type.toString(true));
+		w("baseEncodedSize", toCompactHexWithPrefix(_type.isByteArray() ? 1 : _type.baseType()->calldataEncodedSize()));
+		w("length", _type.isDynamicallyEncoded() ? "length" : toCompactHexWithPrefix(_type.length()));
+		return w.render();
+	});
+}
+
+string ABIFunctions::abiDecodingFunctionByteArray(ArrayType const& _type, bool _fromMemory)
+{
+	solAssert(_type.dataStoredIn(DataLocation::Memory), "");
+	solAssert(_type.isByteArray(), "");
+
+	string functionName =
+		"abi_decode_" +
+		_type.identifier() +
+		(_fromMemory ? "_fromMemory" : "");
+
+	return createFunction(functionName, [&]() {
+		Whiskers templ(
+			R"(
+				function <functionName>(offset, end) -> array {
+					switch slt(add(offset, 0x1f), end) case 0 { revert(0, 0) }
+					let length := <load>(offset)
+					array := <allocate>(<allocationSize>(length))
+					mstore(array, length)
+					let src := add(offset, 0x20)
+					let dst := add(array, 0x20)
+					switch gt(add(src, length), end) case 1 { revert(0, 0) }
+					<copyToMemFun>(src, dst, length)
+				}
+			)"
+		);
+		templ("functionName", functionName);
+		templ("load", _fromMemory ? "mload" : "calldataload");
+		templ("allocate", allocationFunction());
+		templ("allocationSize", arrayAllocationSizeFunction(_type));
+		templ("copyToMemFun", copyToMemoryFunction(!_fromMemory));
+		return templ.render();
+	});
+}
+
+string ABIFunctions::abiDecodingFunctionStruct(StructType const& _type, bool _fromMemory)
+{
+	string functionName =
+		"abi_decode_" +
+		_type.identifier() +
+		(_fromMemory ? "_fromMemory" : "");
+
+	solUnimplementedAssert(!_type.dataStoredIn(DataLocation::CallData), "");
+
+	return createFunction(functionName, [&]() {
+		Whiskers templ(R"(
+			// <readableTypeName>
+			function <functionName>(headStart, end) -> value {
+				switch slt(sub(end, headStart), <minimumSize>) case 1 { revert(0, 0) }
+				value := <allocate>(<memorySize>)
+				<#members>
+				{
+					// <memberName>
+					<decode>
+				}
+				</members>
+			}
+		)");
+		templ("functionName", functionName);
+		templ("readableTypeName", _type.toString(true));
+		templ("allocate", allocationFunction());
+		solAssert(_type.memorySize() < u256("0xffffffffffffffff"), "");
+		templ("memorySize", toCompactHexWithPrefix(_type.memorySize()));
+		size_t headPos = 0;
+		vector<map<string, string>> members;
+		for (auto const& member: _type.members(nullptr))
+		{
+			solAssert(member.type, "");
+			solAssert(member.type->canLiveOutsideStorage(), "");
+			auto decodingType = member.type->decodingType();
+			solAssert(decodingType, "");
+			bool dynamic = decodingType->isDynamicallyEncoded();
+			Whiskers memberTempl(
+				dynamic ?
+				R"(
+					let offset := <load>(add(headStart, <pos>))
+					switch gt(offset, 0xffffffffffffffff) case 1 { revert(0, 0) }
+					mstore(add(value, <memoryOffset>), <abiDecode>(add(headStart, offset), end))
+				)" :
+				R"(
+					let offset := <pos>
+					mstore(add(value, <memoryOffset>), <abiDecode>(add(headStart, offset), end))
+				)"
+			);
+			memberTempl("load", _fromMemory ? "mload" : "calldataload");
+			memberTempl("pos", to_string(headPos));
+			memberTempl("memoryOffset", toCompactHexWithPrefix(_type.memoryOffsetOfMember(member.name)));
+			memberTempl("abiDecode", abiDecodingFunction(*member.type, _fromMemory, false));
+
+			members.push_back({});
+			members.back()["decode"] = memberTempl.render();
+			members.back()["memberName"] = member.name;
+			headPos += dynamic ? 0x20 : decodingType->calldataEncodedSize();
+		}
+		templ("members", members);
+		templ("minimumSize", toCompactHexWithPrefix(headPos));
+		return templ.render();
+	});
+}
+
+string ABIFunctions::abiDecodingFunctionFunctionType(FunctionType const& _type, bool _fromMemory, bool _forUseOnStack)
+{
+	solAssert(_type.kind() == FunctionType::Kind::External, "");
+
+	string functionName =
+		"abi_decode_" +
+		_type.identifier() +
+		(_fromMemory ? "_fromMemory" : "") +
+		(_forUseOnStack ? "_onStack" : "");
+
+	return createFunction(functionName, [&]() {
+		if (_forUseOnStack)
+		{
+			return Whiskers(R"(
+				function <functionName>(offset, end) -> addr, function_selector {
+					addr, function_selector := <splitExtFun>(<load>(offset))
+				}
+			)")
+			("functionName", functionName)
+			("load", _fromMemory ? "mload" : "calldataload")
+			("splitExtFun", splitExternalFunctionIdFunction())
+			.render();
+		}
+		else
+		{
+			return Whiskers(R"(
+				function <functionName>(offset, end) -> fun {
+					fun := <cleanExtFun>(<load>(offset))
+				}
+			)")
+			("functionName", functionName)
+			("load", _fromMemory ? "mload" : "calldataload")
+			("cleanExtFun", cleanupCombinedExternalFunctionIdFunction())
+			.render();
+		}
+	});
+}
+
 string ABIFunctions::copyToMemoryFunction(bool _fromCalldata)
 {
 	string functionName = "copy_" + string(_fromCalldata ? "calldata" : "memory") + "_to_memory";
@@ -988,8 +1383,8 @@ string ABIFunctions::copyToMemoryFunction(bool _fromCalldata)
 					{
 						mstore(add(dst, i), mload(add(src, i)))
 					}
-					switch eq(i, length)
-					case 0 {
+					if gt(i, length)
+					{
 						// clear end
 						mstore(add(dst, length), 0)
 					}
@@ -1098,6 +1493,33 @@ string ABIFunctions::arrayLengthFunction(ArrayType const& _type)
 	});
 }
 
+string ABIFunctions::arrayAllocationSizeFunction(ArrayType const& _type)
+{
+	solAssert(_type.dataStoredIn(DataLocation::Memory), "");
+	string functionName = "array_allocation_size_" + _type.identifier();
+	return createFunction(functionName, [&]() {
+		Whiskers w(R"(
+			function <functionName>(length) -> size {
+				// Make sure we can allocate memory without overflow
+				switch gt(length, 0xffffffffffffffff) case 1 { revert(0, 0) }
+				size := <allocationSize>
+				<addLengthSlot>
+			}
+		)");
+		w("functionName", functionName);
+		if (_type.isByteArray())
+			// Round up
+			w("allocationSize", "and(add(length, 0x1f), not(0x1f))");
+		else
+			w("allocationSize", "mul(length, 0x20)");
+		if (_type.isDynamicallySized())
+			w("addLengthSlot", "size := add(size, 0x20)");
+		else
+			w("addLengthSlot", "");
+		return w.render();
+	});
+}
+
 string ABIFunctions::arrayDataAreaFunction(ArrayType const& _type)
 {
 	string functionName = "array_dataslot_" + _type.identifier();
@@ -1189,6 +1611,25 @@ string ABIFunctions::nextArrayElementFunction(ArrayType const& _type)
 	});
 }
 
+string ABIFunctions::allocationFunction()
+{
+	string functionName = "allocateMemory";
+	return createFunction(functionName, [&]() {
+		return Whiskers(R"(
+			function <functionName>(size) -> memPtr {
+				memPtr := mload(<freeMemoryPointer>)
+				let newFreePtr := add(memPtr, size)
+				// protect against overflow
+				switch or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, memPtr)) case 1 { revert(0, 0) }
+				mstore(<freeMemoryPointer>, newFreePtr)
+			}
+		)")
+		("freeMemoryPointer", to_string(CompilerUtils::freeMemoryPointer))
+		("functionName", functionName)
+		.render();
+	});
+}
+
 string ABIFunctions::createFunction(string const& _name, function<string ()> const& _creator)
 {
 	if (!m_requestedFunctions.count(_name))
diff --git a/libsolidity/codegen/ABIFunctions.h b/libsolidity/codegen/ABIFunctions.h
index e61f68bc..2b582e84 100644
--- a/libsolidity/codegen/ABIFunctions.h
+++ b/libsolidity/codegen/ABIFunctions.h
@@ -66,6 +66,16 @@ public:
 		bool _encodeAsLibraryTypes = false
 	);
 
+	/// @returns name of an assembly function to ABI-decode values of @a _types
+	/// into memory. If @a _fromMemory is true, decodes from memory instead of
+	/// from calldata.
+	/// Can allocate memory.
+	/// Inputs: <source_offset> <source_end> (layout reversed on stack)
+	/// Outputs: <value0> <value1> ... <valuen>
+	/// The values represent stack slots. If a type occupies more or less than one
+	/// stack slot, it takes exactly that number of values.
+	std::string tupleDecoder(TypePointers const& _types, bool _fromMemory = false);
+
 	/// @returns concatenation of all generated functions.
 	std::string requestedFunctions();
 
@@ -87,6 +97,10 @@ private:
 	/// for use in the ABI.
 	std::string combineExternalFunctionIdFunction();
 
+	/// @returns a function that splits the address and selector from a single value
+	/// for use in the ABI.
+	std::string splitExternalFunctionIdFunction();
+
 	/// @returns the name of the ABI encoding function with the given type
 	/// and queues the generation of the function to the requested functions.
 	/// @param _fromStack if false, the input value was just loaded from storage
@@ -146,6 +160,31 @@ private:
 		bool _fromStack
 	);
 
+	/// @returns the name of the ABI decoding function for the given type
+	/// and queues the generation of the function to the requested functions.
+	/// The caller has to ensure that no out of bounds access (at least to the static
+	/// part) can happen inside this function.
+	/// @param _fromMemory if decoding from memory instead of from calldata
+	/// @param _forUseOnStack if the decoded value is stored on stack or in memory.
+	std::string abiDecodingFunction(
+		Type const& _Type,
+		bool _fromMemory,
+		bool _forUseOnStack
+	);
+
+	/// Part of @a abiDecodingFunction for value types.
+	std::string abiDecodingFunctionValueType(Type const& _type, bool _fromMemory);
+	/// Part of @a abiDecodingFunction for "regular" array types.
+	std::string abiDecodingFunctionArray(ArrayType const& _type, bool _fromMemory);
+	/// Part of @a abiDecodingFunction for calldata array types.
+	std::string abiDecodingFunctionCalldataArray(ArrayType const& _type);
+	/// Part of @a abiDecodingFunction for byte array types.
+	std::string abiDecodingFunctionByteArray(ArrayType const& _type, bool _fromMemory);
+	/// Part of @a abiDecodingFunction for struct types.
+	std::string abiDecodingFunctionStruct(StructType const& _type, bool _fromMemory);
+	/// Part of @a abiDecodingFunction for array types.
+	std::string abiDecodingFunctionFunctionType(FunctionType const& _type, bool _fromMemory, bool _forUseOnStack);
+
 	/// @returns a function that copies raw bytes of dynamic length from calldata
 	/// or memory to memory.
 	/// Pads with zeros and might write more than exactly length.
@@ -158,6 +197,10 @@ private:
 	std::string roundUpFunction();
 
 	std::string arrayLengthFunction(ArrayType const& _type);
+	/// @returns the name of a function that computes the number of bytes required
+	/// to store an array in memory given its length (internally encoded, not ABI encoded).
+	/// The function reverts for too large lengthes.
+	std::string arrayAllocationSizeFunction(ArrayType const& _type);
 	/// @returns the name of a function that converts a storage slot number
 	/// or a memory pointer to the slot number / memory pointer for the data position of an array
 	/// which is stored in that slot / memory area.
@@ -166,6 +209,12 @@ private:
 	/// Only works for memory arrays and storage arrays that store one item per slot.
 	std::string nextArrayElementFunction(ArrayType const& _type);
 
+	/// @returns the name of a function that allocates memory.
+	/// Modifies the "free memory pointer"
+	/// Arguments: size
+	/// Return value: pointer
+	std::string allocationFunction();
+
 	/// Helper function that uses @a _creator to create a function and add it to
 	/// @a m_requestedFunctions if it has not been created yet and returns @a _name in both
 	/// cases.
diff --git a/libsolidity/codegen/CompilerUtils.cpp b/libsolidity/codegen/CompilerUtils.cpp
index f9b181ae..533aca5c 100644
--- a/libsolidity/codegen/CompilerUtils.cpp
+++ b/libsolidity/codegen/CompilerUtils.cpp
@@ -121,7 +121,7 @@ void CompilerUtils::storeInMemoryDynamic(Type const& _type, bool _padToWordBound
 {
 	if (auto ref = dynamic_cast<ReferenceType const*>(&_type))
 	{
-		solUnimplementedAssert(ref->location() == DataLocation::Memory, "");
+		solUnimplementedAssert(ref->location() == DataLocation::Memory, "Only in-memory reference type can be stored.");
 		storeInMemoryDynamic(IntegerType(256), _padToWordBoundaries);
 	}
 	else if (auto str = dynamic_cast<StringLiteralType const*>(&_type))
@@ -319,6 +319,23 @@ void CompilerUtils::abiEncodeV2(
 	m_context << ret.tag();
 }
 
+void CompilerUtils::abiDecodeV2(TypePointers const& _parameterTypes, bool _fromMemory)
+{
+	// stack: <source_offset>
+	auto ret = m_context.pushNewTag();
+	m_context << Instruction::SWAP1;
+	if (_fromMemory)
+		// TODO pass correct size for the memory case
+		m_context << (u256(1) << 63);
+	else
+		m_context << Instruction::CALLDATASIZE;
+	m_context << Instruction::SWAP1;
+	string decoderName = m_context.abiFunctions().tupleDecoder(_parameterTypes, _fromMemory);
+	m_context.appendJumpTo(m_context.namedTag(decoderName));
+	m_context.adjustStackOffset(int(sizeOnStack(_parameterTypes)) - 3);
+	m_context << ret.tag();
+}
+
 void CompilerUtils::zeroInitialiseMemoryArray(ArrayType const& _type)
 {
 	auto repeat = m_context.newTag();
diff --git a/libsolidity/codegen/CompilerUtils.h b/libsolidity/codegen/CompilerUtils.h
index ad3989ad..3cde281b 100644
--- a/libsolidity/codegen/CompilerUtils.h
+++ b/libsolidity/codegen/CompilerUtils.h
@@ -146,6 +146,13 @@ public:
 		bool _encodeAsLibraryTypes = false
 	);
 
+	/// Decodes data from ABI encoding into internal encoding. If @a _fromMemory is set to true,
+	/// the data is taken from memory instead of from calldata.
+	/// Can allocate memory.
+	/// Stack pre: <source_offset>
+	/// Stack post: <value0> <value1> ... <valuen>
+	void abiDecodeV2(TypePointers const& _parameterTypes, bool _fromMemory = false);
+
 	/// Zero-initialises (the data part of) an already allocated memory array.
 	/// Length has to be nonzero!
 	/// Stack pre: <length> <memptr>
diff --git a/libsolidity/codegen/ContractCompiler.cpp b/libsolidity/codegen/ContractCompiler.cpp
index 74565ae4..a81ba518 100644
--- a/libsolidity/codegen/ContractCompiler.cpp
+++ b/libsolidity/codegen/ContractCompiler.cpp
@@ -322,6 +322,15 @@ void ContractCompiler::appendCalldataUnpacker(TypePointers const& _typeParameter
 {
 	// We do not check the calldata size, everything is zero-padded
 
+	if (m_context.experimentalFeatureActive(ExperimentalFeature::ABIEncoderV2))
+	{
+		// Use the new JULIA-based decoding function
+		auto stackHeightBefore = m_context.stackHeight();
+		CompilerUtils(m_context).abiDecodeV2(_typeParameters, _fromMemory);
+		solAssert(m_context.stackHeight() - stackHeightBefore == CompilerUtils(m_context).sizeOnStack(_typeParameters) - 1, "");
+		return;
+	}
+
 	//@todo this does not yet support nested dynamic arrays
 
 	// Retain the offset pointer as base_offset, the point from which the data offsets are computed.
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 2d2f05ec..1050621e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -23,9 +23,12 @@
 #include <libsolidity/formal/SMTLib2Interface.h>
 #endif
 
+#include <libsolidity/formal/VariableUsage.h>
+
 #include <libsolidity/interface/ErrorReporter.h>
 
 #include <boost/range/adaptor/map.hpp>
+#include <boost/algorithm/string/replace.hpp>
 
 using namespace std;
 using namespace dev;
@@ -44,28 +47,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
 
 void SMTChecker::analyze(SourceUnit const& _source)
 {
+	m_variableUsage = make_shared<VariableUsage>(_source);
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
-	{
-		m_interface->reset();
-		m_currentSequenceCounter.clear();
-		m_nextFreeSequenceCounter.clear();
 		_source.accept(*this);
-	}
 }
 
 void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
 {
-	if (_varDecl.value())
-	{
-		m_errorReporter.warning(
-			_varDecl.location(),
-			"Assertion checker does not yet support this."
-		);
-	}
-	else if (_varDecl.isLocalOrReturn())
-		createVariable(_varDecl, true);
-	else if (_varDecl.isCallableParameter())
-		createVariable(_varDecl, false);
+	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
+		assignment(_varDecl, *_varDecl.value());
 }
 
 bool SMTChecker::visit(FunctionDefinition const& _function)
@@ -75,20 +65,22 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 			_function.location(),
 			"Assertion checker does not yet support constructors and functions with modifiers."
 		);
-	// TODO actually we probably also have to reset all local variables and similar things.
 	m_currentFunction = &_function;
-	m_interface->push();
+	// We only handle local variables, so we clear at the beginning of the function.
+	// If we add storage variables, those should be cleared differently.
+	m_interface->reset();
+	m_currentSequenceCounter.clear();
+	m_nextFreeSequenceCounter.clear();
+	m_conditionalExecutionHappened = false;
+	initializeLocalVariables(_function);
 	return true;
 }
 
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
 	// TOOD we could check for "reachability", i.e. satisfiability here.
-	// We only handle local variables, so we clear everything.
+	// We only handle local variables, so we clear at the beginning of the function.
 	// If we add storage variables, those should be cleared differently.
-	m_currentSequenceCounter.clear();
-	m_nextFreeSequenceCounter.clear();
-	m_interface->pop();
 	m_currentFunction = nullptr;
 }
 
@@ -96,57 +88,84 @@ bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
 
-	// TODO Check if condition is always true
-
-	auto countersAtStart = m_currentSequenceCounter;
-	m_interface->push();
-	m_interface->addAssertion(expr(_node.condition()));
-	_node.trueStatement().accept(*this);
-	auto countersAtEndOfTrue = m_currentSequenceCounter;
-	m_interface->pop();
+	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	decltype(m_currentSequenceCounter) countersAtEndOfFalse;
+	visitBranch(_node.trueStatement(), expr(_node.condition()));
+	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
 	if (_node.falseStatement())
 	{
-		m_currentSequenceCounter = countersAtStart;
-		m_interface->push();
-		m_interface->addAssertion(!expr(_node.condition()));
-		_node.falseStatement()->accept(*this);
-		countersAtEndOfFalse = m_currentSequenceCounter;
-		m_interface->pop();
+		visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
-	else
-		countersAtEndOfFalse = countersAtStart;
 
-	// Reset all values that have been touched.
+	resetVariables(touchedVariables);
 
-	// TODO this should use a previously generated side-effect structure
+	return false;
+}
 
-	solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
-	for (auto const& declCounter: countersAtEndOfTrue)
+bool SMTChecker::visit(WhileStatement const& _node)
+{
+	auto touchedVariables = m_variableUsage->touchedVariables(_node);
+	resetVariables(touchedVariables);
+	if (_node.isDoWhile())
 	{
-		solAssert(countersAtEndOfFalse.count(declCounter.first), "");
-		auto decl = declCounter.first;
-		int trueCounter = countersAtEndOfTrue.at(decl);
-		int falseCounter = countersAtEndOfFalse.at(decl);
-		if (trueCounter == falseCounter)
-			continue; // Was not modified
-		newValue(*decl);
-		setValue(*decl, 0);
+		visitBranch(_node.body());
+		// TODO the assertions generated in the body should still be active in the condition
+		_node.condition().accept(*this);
+		checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
 	}
+	else
+	{
+		_node.condition().accept(*this);
+		checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+
+		visitBranch(_node.body(), expr(_node.condition()));
+	}
+	resetVariables(touchedVariables);
+
 	return false;
 }
 
-bool SMTChecker::visit(WhileStatement const& _node)
+bool SMTChecker::visit(ForStatement const& _node)
 {
-	_node.condition().accept(*this);
+	if (_node.initializationExpression())
+		_node.initializationExpression()->accept(*this);
+
+	// Do not reset the init expression part.
+	auto touchedVariables =
+		m_variableUsage->touchedVariables(_node.body());
+	if (_node.condition())
+		touchedVariables += m_variableUsage->touchedVariables(*_node.condition());
+	if (_node.loopExpression())
+		touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression());
+	// Remove duplicates
+	std::sort(touchedVariables.begin(), touchedVariables.end());
+	touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
+
+	resetVariables(touchedVariables);
+
+	if (_node.condition())
+	{
+		_node.condition()->accept(*this);
+		checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+	}
 
-	//m_interface->push();
-	//m_interface->addAssertion(expr(_node.condition()));
-	// TDOO clear knowledge (increment sequence numbers and add bounds assertions	) apart from assertions
+	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+	m_interface->push();
+	if (_node.condition())
+		m_interface->addAssertion(expr(*_node.condition()));
+	_node.body().accept(*this);
+	if (_node.loopExpression())
+		_node.loopExpression()->accept(*this);
 
-	// TODO combine similar to if
-	return true;
+	m_interface->pop();
+
+	m_conditionalExecutionHappened = true;
+	m_currentSequenceCounter = sequenceCountersStart;
+
+	resetVariables(touchedVariables);
+
+	return false;
 }
 
 void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
@@ -160,8 +179,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 	{
 		if (_varDecl.initialValue())
 			// TODO more checks?
-			// TODO add restrictions about type (might be assignment from smaller type)
-			m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
+			assignment(*_varDecl.declarations()[0], *_varDecl.initialValue());
 	}
 	else
 		m_errorReporter.warning(
@@ -190,9 +208,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 	{
 		Declaration const* decl = identifier->annotation().referencedDeclaration;
 		if (knownVariable(*decl))
-			// TODO more checks?
-			// TODO add restrictions about type (might be assignment from smaller type)
-			m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
+			assignment(*decl, _assignment.rightHandSide());
 		else
 			m_errorReporter.warning(
 				_assignment.location(),
@@ -269,23 +285,17 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 {
 	Declaration const* decl = _identifier.annotation().referencedDeclaration;
 	solAssert(decl, "");
-	if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+	if (_identifier.annotation().lValueRequested)
 	{
-		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
-		return;
+		// Will be translated as part of the node that requested the lvalue.
 	}
+	else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
 		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
 			return;
-		// TODO for others, clear our knowledge about storage and memory
 	}
-	m_errorReporter.warning(
-		_identifier.location(),
-		"Assertion checker does not yet support the type of this expression (" +
-		_identifier.annotation().type->toString() +
-		")."
-	);
 }
 
 void SMTChecker::endVisit(Literal const& _literal)
@@ -298,10 +308,12 @@ void SMTChecker::endVisit(Literal const& _literal)
 
 		m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
 	}
+	else if (type.category() == Type::Category::Bool)
+		m_interface->addAssertion(expr(_literal) == smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else
 		m_errorReporter.warning(
 			_literal.location(),
-			"Assertion checker does not yet support the type of this expression (" +
+			"Assertion checker does not yet support the type of this literal (" +
 			_literal.annotation().type->toString() +
 			")."
 		);
@@ -386,6 +398,7 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 	solAssert(_op.annotation().commonType, "");
 	if (_op.annotation().commonType->category() == Type::Category::Bool)
 	{
+		// @TODO check that both of them are not constant
 		if (_op.getOperator() == Token::And)
 			m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		else
@@ -395,7 +408,33 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 		m_errorReporter.warning(
 			_op.location(),
 			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
-		);
+					);
+}
+
+void SMTChecker::assignment(Declaration const& _variable, Expression const& _value)
+{
+	// TODO more checks?
+	// TODO add restrictions about type (might be assignment from smaller type)
+	m_interface->addAssertion(newValue(_variable) == expr(_value));
+}
+
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+{
+	visitBranch(_statement, &_condition);
+}
+
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+{
+	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+
+	m_interface->push();
+	if (_condition)
+		m_interface->addAssertion(*_condition);
+	_statement.accept(*this);
+	m_interface->pop();
+
+	m_conditionalExecutionHappened = true;
+	m_currentSequenceCounter = sequenceCountersStart;
 }
 
 void SMTChecker::checkCondition(
@@ -433,19 +472,13 @@ void SMTChecker::checkCondition(
 	}
 	smt::CheckResult result;
 	vector<string> values;
-	try
-	{
-		tie(result, values) = m_interface->check(expressionsToEvaluate);
-	}
-	catch (smt::SolverError const& _e)
-	{
-		string description("Error querying SMT solver");
-		if (_e.comment())
-			description += ": " + *_e.comment();
-		m_errorReporter.warning(_location, description);
-		return;
-	}
+	tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate);
 
+	string conditionalComment;
+	if (m_conditionalExecutionHappened)
+		conditionalComment =
+			"\nNote that some information is erased after conditional execution of parts of the code.\n"
+			"You can re-introduce information using require().";
 	switch (result)
 	{
 	case smt::CheckResult::SATISFIABLE:
@@ -457,27 +490,17 @@ void SMTChecker::checkCondition(
 			message << " for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			for (size_t i = 0; i < values.size(); ++i)
-			{
-				string formattedValue = values.at(i);
-				try
-				{
-					// Parse and re-format nicely
-					formattedValue = formatNumber(bigint(formattedValue));
-				}
-				catch (...) { }
-
-				message << "  " << expressionNames.at(i) << " = " << formattedValue << "\n";
-			}
+				message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
 		}
 		else
 			message << ".";
-		m_errorReporter.warning(_location, message.str());
+		m_errorReporter.warning(_location, message.str() + conditionalComment);
 		break;
 	}
 	case smt::CheckResult::UNSATISFIABLE:
 		break;
 	case smt::CheckResult::UNKNOWN:
-		m_errorReporter.warning(_location, _description + " might happen here.");
+		m_errorReporter.warning(_location, _description + " might happen here." + conditionalComment);
 		break;
 	case smt::CheckResult::ERROR:
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
@@ -488,7 +511,110 @@ void SMTChecker::checkCondition(
 	m_interface->pop();
 }
 
-void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
+{
+	// Do not check for const-ness if this is a constant.
+	if (dynamic_cast<Literal const*>(&_condition))
+		return;
+
+	m_interface->push();
+	m_interface->addAssertion(expr(_condition));
+	auto positiveResult = checkSatisifable();
+	m_interface->pop();
+
+	m_interface->push();
+	m_interface->addAssertion(!expr(_condition));
+	auto negatedResult = checkSatisifable();
+	m_interface->pop();
+
+	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
+		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
+	else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
+	{
+		// everything fine.
+	}
+	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
+		m_errorReporter.warning(_condition.location(), "Condition unreachable.");
+	else
+	{
+		string value;
+		if (positiveResult == smt::CheckResult::SATISFIABLE)
+		{
+			solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
+			value = "true";
+		}
+		else
+		{
+			solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
+			solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
+			value = "false";
+		}
+		m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value));
+	}
+}
+
+pair<smt::CheckResult, vector<string>>
+SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
+{
+	smt::CheckResult result;
+	vector<string> values;
+	try
+	{
+		tie(result, values) = m_interface->check(_expressionsToEvaluate);
+	}
+	catch (smt::SolverError const& _e)
+	{
+		string description("Error querying SMT solver");
+		if (_e.comment())
+			description += ": " + *_e.comment();
+		m_errorReporter.warning(description);
+		result = smt::CheckResult::ERROR;
+	}
+
+	for (string& value: values)
+	{
+		try
+		{
+			// Parse and re-format nicely
+			value = formatNumber(bigint(value));
+		}
+		catch (...) { }
+	}
+
+	return make_pair(result, values);
+}
+
+smt::CheckResult SMTChecker::checkSatisifable()
+{
+	return checkSatisifableAndGenerateModel({}).first;
+}
+
+void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
+{
+	for (auto const& variable: _function.localVariables())
+		if (createVariable(*variable))
+			setZeroValue(*variable);
+
+	for (auto const& param: _function.parameters())
+		if (createVariable(*param))
+			setUnknownValue(*param);
+
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+			if (createVariable(*retParam))
+				setZeroValue(*retParam);
+}
+
+void SMTChecker::resetVariables(vector<Declaration const*> _variables)
+{
+	for (auto const* decl: _variables)
+	{
+		newValue(*decl);
+		setUnknownValue(*decl);
+	}
+}
+
+bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
 	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
 	{
@@ -498,13 +624,16 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
 		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
-		setValue(_varDecl, _setToZero);
+		return true;
 	}
 	else
+	{
 		m_errorReporter.warning(
 			_varDecl.location(),
 			"Assertion checker does not yet support the type of this variable."
 		);
+		return false;
+	}
 }
 
 string SMTChecker::uniqueSymbol(Declaration const& _decl)
@@ -535,23 +664,22 @@ smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _seque
 
 smt::Expression SMTChecker::newValue(Declaration const& _decl)
 {
-	solAssert(m_currentSequenceCounter.count(&_decl), "");
 	solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
 	m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
 	return currentValue(_decl);
 }
 
-void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
+void SMTChecker::setZeroValue(Declaration const& _decl)
 {
-	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+	solAssert(_decl.type()->category() == Type::Category::Integer, "");
+	m_interface->addAssertion(currentValue(_decl) == 0);
+}
 
-	if (_setToZero)
-		m_interface->addAssertion(currentValue(_decl) == 0);
-	else
-	{
-		m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
-		m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
-	}
+void SMTChecker::setUnknownValue(Declaration const& _decl)
+{
+	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+	m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
+	m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
 }
 
 smt::Expression SMTChecker::minValue(IntegerType const& _t)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index faaac639..8e07d74d 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -17,8 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/ast/ASTVisitor.h>
+
 #include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
@@ -29,6 +32,7 @@ namespace dev
 namespace solidity
 {
 
+class VariableUsage;
 class ErrorReporter;
 
 class SMTChecker: private ASTConstVisitor
@@ -48,6 +52,7 @@ private:
 	virtual void endVisit(FunctionDefinition const& _node) override;
 	virtual bool visit(IfStatement const& _node) override;
 	virtual bool visit(WhileStatement const& _node) override;
+	virtual bool visit(ForStatement const& _node) override;
 	virtual void endVisit(VariableDeclarationStatement const& _node) override;
 	virtual void endVisit(ExpressionStatement const& _node) override;
 	virtual void endVisit(Assignment const& _node) override;
@@ -61,6 +66,14 @@ private:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void assignment(Declaration const& _variable, Expression const& _value);
+
+	// Visits the branch given by the statement, pushes and pops the SMT checker.
+	// @param _condition if present, asserts that this condition is true within the branch.
+	void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	void visitBranch(Statement const& _statement, smt::Expression _condition);
+
+	/// Check that a condition can be satisfied.
 	void checkCondition(
 		smt::Expression _condition,
 		SourceLocation const& _location,
@@ -68,8 +81,24 @@ private:
 		std::string const& _additionalValueName = "",
 		smt::Expression* _additionalValue = nullptr
 	);
+	/// Checks that a boolean condition is not constant. Do not warn if the expression
+	/// is a literal constant.
+	/// @param _description the warning string, $VALUE will be replaced by the constant value.
+	void checkBooleanNotConstant(
+		Expression const& _condition,
+		std::string const& _description
+	);
+
+	std::pair<smt::CheckResult, std::vector<std::string>>
+	checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
 
-	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+	smt::CheckResult checkSatisifable();
+
+	void initializeLocalVariables(FunctionDefinition const& _function);
+	void resetVariables(std::vector<Declaration const*> _variables);
+	/// Tries to create an uninitialized variable and returns true on success.
+	/// This fails if the type is not supported.
+	bool createVariable(VariableDeclaration const& _varDecl);
 
 	static std::string uniqueSymbol(Declaration const& _decl);
 	static std::string uniqueSymbol(Expression const& _expr);
@@ -87,12 +116,16 @@ private:
 	/// sequence number to this value and returns the expression.
 	smt::Expression newValue(Declaration const& _decl);
 
-	/// Sets the value of the declaration either to zero or to its intrinsic range.
-	void setValue(Declaration const& _decl, bool _setToZero);
+	/// Sets the value of the declaration to zero.
+	void setZeroValue(Declaration const& _decl);
+	/// Resets the variable to an unknown value (in its range).
+	void setUnknownValue(Declaration const& decl);
 
 	static smt::Expression minValue(IntegerType const& _t);
 	static smt::Expression maxValue(IntegerType const& _t);
 
+	using VariableSequenceCounters = std::map<Declaration const*, int>;
+
 	/// Returns the expression corresponding to the AST node. Creates a new expression
 	/// if it does not exist yet.
 	smt::Expression expr(Expression const& _e);
@@ -101,6 +134,8 @@ private:
 	smt::Expression var(Declaration const& _decl);
 
 	std::shared_ptr<smt::SolverInterface> m_interface;
+	std::shared_ptr<VariableUsage> m_variableUsage;
+	bool m_conditionalExecutionHappened = false;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_expressions;
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index cbd766fb..0e00665a 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -145,8 +145,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
-			// TODO they don't have to be ints...
-			command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
+			solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
 		command += "(check-sat)\n";
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 70dc1585..c9adf863 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -44,7 +44,9 @@ enum class CheckResult
 
 enum class Sort
 {
-	Int, Bool
+	Int,
+	Bool,
+	IntIntFun // Function of one Int returning a single Int
 };
 
 /// C++ representation of an SMTLIB2 expression.
@@ -52,9 +54,10 @@ class Expression
 {
 	friend class SolverInterface;
 public:
-	Expression(size_t _number): name(std::to_string(_number)) {}
-	Expression(u256 const& _number): name(_number.str()) {}
-	Expression(bigint const& _number): name(_number.str()) {}
+	explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {}
+	Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {}
+	Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {}
+	Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {}
 
 	Expression(Expression const&) = default;
 	Expression(Expression&&) = default;
@@ -63,26 +66,27 @@ public:
 
 	static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
 	{
+		solAssert(_trueValue.sort == _falseValue.sort, "");
 		return Expression("ite", std::vector<Expression>{
 			std::move(_condition), std::move(_trueValue), std::move(_falseValue)
-		});
+		}, _trueValue.sort);
 	}
 
 	friend Expression operator!(Expression _a)
 	{
-		return Expression("not", std::move(_a));
+		return Expression("not", std::move(_a), Sort::Bool);
 	}
 	friend Expression operator&&(Expression _a, Expression _b)
 	{
-		return Expression("and", std::move(_a), std::move(_b));
+		return Expression("and", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator||(Expression _a, Expression _b)
 	{
-		return Expression("or", std::move(_a), std::move(_b));
+		return Expression("or", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator==(Expression _a, Expression _b)
 	{
-		return Expression("=", std::move(_a), std::move(_b));
+		return Expression("=", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator!=(Expression _a, Expression _b)
 	{
@@ -90,52 +94,56 @@ public:
 	}
 	friend Expression operator<(Expression _a, Expression _b)
 	{
-		return Expression("<", std::move(_a), std::move(_b));
+		return Expression("<", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator<=(Expression _a, Expression _b)
 	{
-		return Expression("<=", std::move(_a), std::move(_b));
+		return Expression("<=", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator>(Expression _a, Expression _b)
 	{
-		return Expression(">", std::move(_a), std::move(_b));
+		return Expression(">", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator>=(Expression _a, Expression _b)
 	{
-		return Expression(">=", std::move(_a), std::move(_b));
+		return Expression(">=", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator+(Expression _a, Expression _b)
 	{
-		return Expression("+", std::move(_a), std::move(_b));
+		return Expression("+", std::move(_a), std::move(_b), Sort::Int);
 	}
 	friend Expression operator-(Expression _a, Expression _b)
 	{
-		return Expression("-", std::move(_a), std::move(_b));
+		return Expression("-", std::move(_a), std::move(_b), Sort::Int);
 	}
 	friend Expression operator*(Expression _a, Expression _b)
 	{
-		return Expression("*", std::move(_a), std::move(_b));
+		return Expression("*", std::move(_a), std::move(_b), Sort::Int);
 	}
 	Expression operator()(Expression _a) const
 	{
-		solAssert(arguments.empty(), "Attempted function application to non-function.");
-		return Expression(name, _a);
+		solAssert(
+			sort == Sort::IntIntFun && arguments.empty(),
+			"Attempted function application to non-function."
+		);
+		return Expression(name, _a, Sort::Int);
 	}
 
 	std::string const name;
 	std::vector<Expression> const arguments;
+	Sort sort;
 
 private:
 	/// Manual constructor, should only be used by SolverInterface and this class itself.
-	Expression(std::string _name, std::vector<Expression> _arguments):
-		name(std::move(_name)), arguments(std::move(_arguments)) {}
-
-	explicit Expression(std::string _name):
-		Expression(std::move(_name), std::vector<Expression>{}) {}
-	Expression(std::string _name, Expression _arg):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
-	Expression(std::string _name, Expression _arg1, Expression _arg2):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
+	Expression(std::string _name, std::vector<Expression> _arguments, Sort _sort):
+		name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {}
+
+	explicit Expression(std::string _name, Sort _sort):
+		Expression(std::move(_name), std::vector<Expression>{}, _sort) {}
+	Expression(std::string _name, Expression _arg, Sort _sort):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _sort) {}
+	Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _sort) {}
 };
 
 DEV_SIMPLE_EXCEPTION(SolverError);
@@ -148,20 +156,21 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
+	virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
 	{
+		solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported.");
 		// Subclasses should do something here
-		return Expression(std::move(_name), {});
+		return Expression(std::move(_name), {}, Sort::IntIntFun);
 	}
 	virtual Expression newInteger(std::string _name)
 	{
 		// Subclasses should do something here
-		return Expression(std::move(_name), {});
+		return Expression(std::move(_name), {}, Sort::Int);
 	}
 	virtual Expression newBool(std::string _name)
 	{
 		// Subclasses should do something here
-		return Expression(std::move(_name), {});
+		return Expression(std::move(_name), {}, Sort::Bool);
 	}
 
 	virtual void addAssertion(Expression const& _expr) = 0;
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
new file mode 100644
index 00000000..4e96059d
--- /dev/null
+++ b/libsolidity/formal/VariableUsage.cpp
@@ -0,0 +1,80 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/VariableUsage.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+VariableUsage::VariableUsage(ASTNode const& _node)
+{
+	auto nodeFun = [&](ASTNode const& n) -> bool
+	{
+		if (Identifier const* identifier = dynamic_cast<decltype(identifier)>(&n))
+		{
+			Declaration const* declaration = identifier->annotation().referencedDeclaration;
+			solAssert(declaration, "");
+			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
+				if (
+					varDecl->isLocalVariable() &&
+					identifier->annotation().lValueRequested &&
+					varDecl->annotation().type->isValueType()
+				)
+					m_touchedVariable[&n] = varDecl;
+		}
+		return true;
+	};
+	auto edgeFun = [&](ASTNode const& _parent, ASTNode const& _child)
+	{
+		if (m_touchedVariable.count(&_child) || m_children.count(&_child))
+			m_children[&_parent].push_back(&_child);
+	};
+
+	ASTReduce reducer(nodeFun, edgeFun);
+	_node.accept(reducer);
+}
+
+vector<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+{
+	if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
+		return {};
+
+	set<Declaration const*> touched;
+	vector<ASTNode const*> toVisit;
+	toVisit.push_back(&_node);
+
+	while (!toVisit.empty())
+	{
+		ASTNode const* n = toVisit.back();
+		toVisit.pop_back();
+		if (m_children.count(n))
+		{
+			solAssert(!m_touchedVariable.count(n), "");
+			toVisit += m_children.at(n);
+		}
+		else
+		{
+			solAssert(m_touchedVariable.count(n), "");
+			touched.insert(m_touchedVariable.at(n));
+		}
+	}
+
+	return {touched.begin(), touched.end()};
+}
diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h
new file mode 100644
index 00000000..62561cce
--- /dev/null
+++ b/libsolidity/formal/VariableUsage.h
@@ -0,0 +1,50 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <map>
+#include <set>
+#include <vector>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ASTNode;
+class Declaration;
+
+/**
+ * This class collects information about which local variables of value type
+ * are modified in which parts of the AST.
+ */
+class VariableUsage
+{
+public:
+	explicit VariableUsage(ASTNode const& _node);
+
+	std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const;
+
+private:
+	// Variable touched by a specific AST node.
+	std::map<ASTNode const*, Declaration const*> m_touchedVariable;
+	std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
+};
+
+}
+}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index ab28baa3..e5c1aef4 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -91,14 +91,14 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 			solAssert(false, "");
 		}
 
-		if (result != CheckResult::UNSATISFIABLE)
+		if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
 		{
 			z3::model m = m_solver.get_model();
 			for (Expression const& e: _expressionsToEvaluate)
 				values.push_back(toString(m.eval(toZ3Expr(e))));
 		}
 	}
-	catch (z3::exception const& _e)
+	catch (z3::exception const&)
 	{
 		result = CheckResult::ERROR;
 		values.clear();
@@ -139,8 +139,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 	}
 	else if (arguments.empty())
 	{
-		// We assume it is an integer...
-		return m_context.int_val(n.c_str());
+		if (n == "true")
+			return m_context.bool_val(true);
+		else if (n == "false")
+			return m_context.bool_val(false);
+		else
+			// We assume it is an integer...
+			return m_context.int_val(n.c_str());
 	}
 
 	solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
diff --git a/libsolidity/inlineasm/AsmAnalysis.cpp b/libsolidity/inlineasm/AsmAnalysis.cpp
index e5bdc90f..2804ddfc 100644
--- a/libsolidity/inlineasm/AsmAnalysis.cpp
+++ b/libsolidity/inlineasm/AsmAnalysis.cpp
@@ -286,6 +286,22 @@ bool AsmAnalyzer::operator()(assembly::FunctionCall const& _funCall)
 	return success;
 }
 
+bool AsmAnalyzer::operator()(If const& _if)
+{
+	bool success = true;
+
+	if (!expectExpression(*_if.condition))
+		success = false;
+	m_stackHeight--;
+
+	if (!(*this)(_if.body))
+		success = false;
+
+	m_info.stackHeightInfo[&_if] = m_stackHeight;
+
+	return success;
+}
+
 bool AsmAnalyzer::operator()(Switch const& _switch)
 {
 	bool success = true;
diff --git a/libsolidity/inlineasm/AsmAnalysis.h b/libsolidity/inlineasm/AsmAnalysis.h
index 9b2a8f9c..e484b876 100644
--- a/libsolidity/inlineasm/AsmAnalysis.h
+++ b/libsolidity/inlineasm/AsmAnalysis.h
@@ -70,6 +70,7 @@ public:
 	bool operator()(assembly::VariableDeclaration const& _variableDeclaration);
 	bool operator()(assembly::FunctionDefinition const& _functionDefinition);
 	bool operator()(assembly::FunctionCall const& _functionCall);
+	bool operator()(assembly::If const& _if);
 	bool operator()(assembly::Switch const& _switch);
 	bool operator()(assembly::ForLoop const& _forLoop);
 	bool operator()(assembly::Block const& _block);
diff --git a/libsolidity/inlineasm/AsmData.h b/libsolidity/inlineasm/AsmData.h
index b0dd85ca..a792a1b8 100644
--- a/libsolidity/inlineasm/AsmData.h
+++ b/libsolidity/inlineasm/AsmData.h
@@ -68,6 +68,8 @@ struct VariableDeclaration { SourceLocation location; TypedNameList variables; s
 struct Block { SourceLocation location; std::vector<Statement> statements; };
 /// Function definition ("function f(a, b) -> (d, e) { ... }")
 struct FunctionDefinition { SourceLocation location; std::string name; TypedNameList arguments; TypedNameList returns; Block body; };
+/// Conditional execution without "else" part.
+struct If { SourceLocation location; std::shared_ptr<Statement> condition; Block body; };
 /// Switch case or default case
 struct Case { SourceLocation location; std::shared_ptr<Literal> value; Block body; };
 /// Switch statement
diff --git a/libsolidity/inlineasm/AsmDataForward.h b/libsolidity/inlineasm/AsmDataForward.h
index 4ead7ff5..d627b41a 100644
--- a/libsolidity/inlineasm/AsmDataForward.h
+++ b/libsolidity/inlineasm/AsmDataForward.h
@@ -41,11 +41,12 @@ struct VariableDeclaration;
 struct FunctionalInstruction;
 struct FunctionDefinition;
 struct FunctionCall;
+struct If;
 struct Switch;
 struct ForLoop;
 struct Block;
 
-using Statement = boost::variant<Instruction, Literal, Label, StackAssignment, Identifier, Assignment, FunctionCall, FunctionalInstruction, VariableDeclaration, FunctionDefinition, Switch, ForLoop, Block>;
+using Statement = boost::variant<Instruction, Literal, Label, StackAssignment, Identifier, Assignment, FunctionCall, FunctionalInstruction, VariableDeclaration, FunctionDefinition, If, Switch, ForLoop, Block>;
 
 }
 }
diff --git a/libsolidity/inlineasm/AsmParser.cpp b/libsolidity/inlineasm/AsmParser.cpp
index 1f4df75b..8f171005 100644
--- a/libsolidity/inlineasm/AsmParser.cpp
+++ b/libsolidity/inlineasm/AsmParser.cpp
@@ -73,13 +73,23 @@ assembly::Statement Parser::parseStatement()
 		return parseFunctionDefinition();
 	case Token::LBrace:
 		return parseBlock();
+	case Token::If:
+	{
+		assembly::If _if = createWithLocation<assembly::If>();
+		m_scanner->next();
+		_if.condition = make_shared<Statement>(parseExpression());
+		if (_if.condition->type() == typeid(assembly::Instruction))
+			fatalParserError("Instructions are not supported as conditions for if - try to append \"()\".");
+		_if.body = parseBlock();
+		return _if;
+	}
 	case Token::Switch:
 	{
 		assembly::Switch _switch = createWithLocation<assembly::Switch>();
 		m_scanner->next();
 		_switch.expression = make_shared<Statement>(parseExpression());
 		if (_switch.expression->type() == typeid(assembly::Instruction))
-			fatalParserError("Instructions are not supported as expressions for switch.");
+			fatalParserError("Instructions are not supported as expressions for switch - try to append \"()\".");
 		while (m_scanner->currentToken() == Token::Case)
 			_switch.cases.emplace_back(parseCase());
 		if (m_scanner->currentToken() == Token::Default)
diff --git a/libsolidity/inlineasm/AsmPrinter.cpp b/libsolidity/inlineasm/AsmPrinter.cpp
index a5272808..0f183244 100644
--- a/libsolidity/inlineasm/AsmPrinter.cpp
+++ b/libsolidity/inlineasm/AsmPrinter.cpp
@@ -174,6 +174,11 @@ string AsmPrinter::operator()(assembly::FunctionCall const& _functionCall)
 		")";
 }
 
+string AsmPrinter::operator()(If const& _if)
+{
+	return "if " + boost::apply_visitor(*this, *_if.condition) + "\n" + (*this)(_if.body);
+}
+
 string AsmPrinter::operator()(Switch const& _switch)
 {
 	string out = "switch " + boost::apply_visitor(*this, *_switch.expression);
diff --git a/libsolidity/inlineasm/AsmPrinter.h b/libsolidity/inlineasm/AsmPrinter.h
index 66520632..eadf81d9 100644
--- a/libsolidity/inlineasm/AsmPrinter.h
+++ b/libsolidity/inlineasm/AsmPrinter.h
@@ -48,6 +48,7 @@ public:
 	std::string operator()(assembly::VariableDeclaration const& _variableDeclaration);
 	std::string operator()(assembly::FunctionDefinition const& _functionDefinition);
 	std::string operator()(assembly::FunctionCall const& _functionCall);
+	std::string operator()(assembly::If const& _if);
 	std::string operator()(assembly::Switch const& _switch);
 	std::string operator()(assembly::ForLoop const& _forLoop);
 	std::string operator()(assembly::Block const& _block);
diff --git a/libsolidity/inlineasm/AsmScopeFiller.cpp b/libsolidity/inlineasm/AsmScopeFiller.cpp
index b70ae9ac..77ae9102 100644
--- a/libsolidity/inlineasm/AsmScopeFiller.cpp
+++ b/libsolidity/inlineasm/AsmScopeFiller.cpp
@@ -104,6 +104,11 @@ bool ScopeFiller::operator()(assembly::FunctionDefinition const& _funDef)
 	return success;
 }
 
+bool ScopeFiller::operator()(If const& _if)
+{
+	return (*this)(_if.body);
+}
+
 bool ScopeFiller::operator()(Switch const& _switch)
 {
 	bool success = true;
diff --git a/libsolidity/inlineasm/AsmScopeFiller.h b/libsolidity/inlineasm/AsmScopeFiller.h
index 80c03d2c..ed28abbf 100644
--- a/libsolidity/inlineasm/AsmScopeFiller.h
+++ b/libsolidity/inlineasm/AsmScopeFiller.h
@@ -59,6 +59,7 @@ public:
 	bool operator()(assembly::VariableDeclaration const& _variableDeclaration);
 	bool operator()(assembly::FunctionDefinition const& _functionDefinition);
 	bool operator()(assembly::FunctionCall const&) { return true; }
+	bool operator()(assembly::If const& _if);
 	bool operator()(assembly::Switch const& _switch);
 	bool operator()(assembly::ForLoop const& _forLoop);
 	bool operator()(assembly::Block const& _block);
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index b99fe4ee..5713256a 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -747,22 +747,32 @@ void CompilerStack::compileContract(
 	}
 }
 
+string const CompilerStack::lastContractName() const
+{
+	if (m_contracts.empty())
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("No compiled contracts found."));
+	// try to find some user-supplied contract
+	string contractName;
+	for (auto const& it: m_sources)
+		for (ASTPointer<ASTNode> const& node: it.second.ast->nodes())
+			if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
+				contractName = contract->fullyQualifiedName();
+	return contractName;
+}
+
 CompilerStack::Contract const& CompilerStack::contract(string const& _contractName) const
 {
 	if (m_contracts.empty())
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("No compiled contracts found."));
-	string contractName = _contractName;
-	if (_contractName.empty())
-		// try to find some user-supplied contract
-		for (auto const& it: m_sources)
-			for (ASTPointer<ASTNode> const& node: it.second.ast->nodes())
-				if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
-					contractName = contract->fullyQualifiedName();
-	auto it = m_contracts.find(contractName);
+
+	auto it = m_contracts.find(_contractName);
+	if (it != m_contracts.end())
+		return it->second;
+
 	// To provide a measure of backward-compatibility, if a contract is not located by its
 	// fully-qualified name, a lookup will be attempted purely on the contract's name to see
 	// if anything will satisfy.
-	if (it == m_contracts.end() && contractName.find(":") == string::npos)
+	if (_contractName.find(":") == string::npos)
 	{
 		for (auto const& contractEntry: m_contracts)
 		{
@@ -773,12 +783,13 @@ CompilerStack::Contract const& CompilerStack::contract(string const& _contractNa
 			string foundName;
 			getline(ss, source, ':');
 			getline(ss, foundName, ':');
-			if (foundName == contractName) return contractEntry.second;
+			if (foundName == _contractName)
+				return contractEntry.second;
 		}
-		// If we get here, both lookup methods failed.
-		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Contract " + _contractName + " not found."));
 	}
-	return it->second;
+
+	// If we get here, both lookup methods failed.
+	BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Contract \"" + _contractName + "\" not found."));
 }
 
 CompilerStack::Source const& CompilerStack::source(string const& _sourceName) const
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index c567ac2c..b377b3aa 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -155,10 +155,10 @@ public:
 	std::map<std::string, unsigned> sourceIndices() const;
 
 	/// @returns the previously used scanner, useful for counting lines during error reporting.
-	Scanner const& scanner(std::string const& _sourceName = "") const;
+	Scanner const& scanner(std::string const& _sourceName) const;
 
 	/// @returns the parsed source unit with the supplied name.
-	SourceUnit const& ast(std::string const& _sourceName = "") const;
+	SourceUnit const& ast(std::string const& _sourceName) const;
 
 	/// Helper function for logs printing. Do only use in error cases, it's quite expensive.
 	/// line and columns are numbered starting from 1 with following order:
@@ -168,48 +168,51 @@ public:
 	/// @returns a list of the contract names in the sources.
 	std::vector<std::string> contractNames() const;
 
+	/// @returns the name of the last contract.
+	std::string const lastContractName() const;
+
 	/// @returns either the contract's name or a mixture of its name and source file, sanitized for filesystem use
 	std::string const filesystemFriendlyName(std::string const& _contractName) const;
 
 	/// @returns the assembled object for a contract.
-	eth::LinkerObject const& object(std::string const& _contractName = "") const;
+	eth::LinkerObject const& object(std::string const& _contractName) const;
 
 	/// @returns the runtime object for the contract.
-	eth::LinkerObject const& runtimeObject(std::string const& _contractName = "") const;
+	eth::LinkerObject const& runtimeObject(std::string const& _contractName) const;
 
 	/// @returns the bytecode of a contract that uses an already deployed contract via DELEGATECALL.
 	/// The returned bytes will contain a sequence of 20 bytes of the format "XXX...XXX" which have to
 	/// substituted by the actual address. Note that this sequence starts end ends in three X
 	/// characters but can contain anything in between.
-	eth::LinkerObject const& cloneObject(std::string const& _contractName = "") const;
+	eth::LinkerObject const& cloneObject(std::string const& _contractName) const;
 
 	/// @returns normal contract assembly items
-	eth::AssemblyItems const* assemblyItems(std::string const& _contractName = "") const;
+	eth::AssemblyItems const* assemblyItems(std::string const& _contractName) const;
 
 	/// @returns runtime contract assembly items
-	eth::AssemblyItems const* runtimeAssemblyItems(std::string const& _contractName = "") const;
+	eth::AssemblyItems const* runtimeAssemblyItems(std::string const& _contractName) const;
 
 	/// @returns the string that provides a mapping between bytecode and sourcecode or a nullptr
 	/// if the contract does not (yet) have bytecode.
-	std::string const* sourceMapping(std::string const& _contractName = "") const;
+	std::string const* sourceMapping(std::string const& _contractName) const;
 
 	/// @returns the string that provides a mapping between runtime bytecode and sourcecode.
 	/// if the contract does not (yet) have bytecode.
-	std::string const* runtimeSourceMapping(std::string const& _contractName = "") const;
+	std::string const* runtimeSourceMapping(std::string const& _contractName) const;
 
 	/// @return a verbose text representation of the assembly.
 	/// @arg _sourceCodes is the map of input files to source code strings
 	/// Prerequisite: Successful compilation.
-	std::string assemblyString(std::string const& _contractName = "", StringMap _sourceCodes = StringMap()) const;
+	std::string assemblyString(std::string const& _contractName, StringMap _sourceCodes = StringMap()) const;
 
 	/// @returns a JSON representation of the assembly.
 	/// @arg _sourceCodes is the map of input files to source code strings
 	/// Prerequisite: Successful compilation.
-	Json::Value assemblyJSON(std::string const& _contractName = "", StringMap _sourceCodes = StringMap()) const;
+	Json::Value assemblyJSON(std::string const& _contractName, StringMap _sourceCodes = StringMap()) const;
 
 	/// @returns a JSON representing the contract ABI.
 	/// Prerequisite: Successful call to parse or compile.
-	Json::Value const& contractABI(std::string const& _contractName = "") const;
+	Json::Value const& contractABI(std::string const& _contractName) const;
 
 	/// @returns a JSON representing the contract's user documentation.
 	/// Prerequisite: Successful call to parse or compile.
@@ -276,8 +279,8 @@ private:
 	);
 	void link();
 
-	Contract const& contract(std::string const& _contractName = "") const;
-	Source const& source(std::string const& _sourceName = "") const;
+	Contract const& contract(std::string const& _contractName) const;
+	Source const& source(std::string const& _sourceName) const;
 
 	/// @returns the parsed contract with the supplied name. Throws an exception if the contract
 	/// does not exist.
diff --git a/libsolidity/interface/SourceReferenceFormatter.cpp b/libsolidity/interface/SourceReferenceFormatter.cpp
index 62d22999..aeafaf2d 100644
--- a/libsolidity/interface/SourceReferenceFormatter.cpp
+++ b/libsolidity/interface/SourceReferenceFormatter.cpp
@@ -49,6 +49,21 @@ void SourceReferenceFormatter::printSourceLocation(
 	if (startLine == endLine)
 	{
 		string line = scanner.lineAtPosition(_location->start);
+
+		int locationLength = endColumn - startColumn;
+		if (locationLength > 150)
+		{
+			line = line.substr(0, startColumn + 35) + " ... " + line.substr(endColumn - 35);
+			endColumn = startColumn + 75;
+			locationLength = 75;
+		}
+		if (line.length() > 150)
+		{
+			line = " ... " + line.substr(startColumn, locationLength) + " ... ";
+			startColumn = 5;
+			endColumn = startColumn + locationLength;
+		}
+
 		_stream << line << endl;
 		for_each(
 			line.cbegin(),
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 430739ac..ad01821e 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -131,6 +131,61 @@ StringMap createSourceList(Json::Value const& _input)
 	return sources;
 }
 
+bool isArtifactRequested(Json::Value const& _outputSelection, string const& _artifact)
+{
+	for (auto const& artifact: _outputSelection)
+		/// @TODO support sub-matching, e.g "evm" matches "evm.assembly"
+		if (artifact == "*" || artifact == _artifact)
+			return true;
+	return false;
+}
+
+///
+/// @a _outputSelection is a JSON object containining a two-level hashmap, where the first level is the filename,
+/// the second level is the contract name and the value is an array of artifact names to be requested for that contract.
+/// @a _file is the current file
+/// @a _contract is the current contract
+/// @a _artifact is the current artifact name
+///
+/// @returns true if the @a _outputSelection has a match for the requested target in the specific file / contract.
+///
+/// In @a _outputSelection the use of '*' as a wildcard is permitted.
+///
+/// @TODO optimise this. Perhaps flatten the structure upfront.
+///
+bool isArtifactRequested(Json::Value const& _outputSelection, string const& _file, string const& _contract, string const& _artifact)
+{
+	if (!_outputSelection.isObject())
+		return false;
+
+	for (auto const& file: { _file, string("*") })
+		if (_outputSelection.isMember(file) && _outputSelection[file].isObject())
+		{
+			/// For SourceUnit-level targets (such as AST) only allow empty name, otherwise
+			/// for Contract-level targets try both contract name and wildcard
+			vector<string> contracts{ _contract };
+			if (!_contract.empty())
+				contracts.push_back("*");
+			for (auto const& contract: contracts)
+				if (
+					_outputSelection[file].isMember(contract) &&
+					_outputSelection[file][contract].isArray() &&
+					isArtifactRequested(_outputSelection[file][contract], _artifact)
+				)
+					return true;
+		}
+
+	return false;
+}
+
+bool isArtifactRequested(Json::Value const& _outputSelection, string const& _file, string const& _contract, vector<string> const& _artifacts)
+{
+	for (auto const& artifact: _artifacts)
+		if (isArtifactRequested(_outputSelection, _file, _contract, artifact))
+			return true;
+	return false;
+}
+
 Json::Value formatLinkReferences(std::map<size_t, std::string> const& linkReferences)
 {
 	Json::Value ret(Json::objectValue);
@@ -396,8 +451,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 	{
 		Json::Value sourceResult = Json::objectValue;
 		sourceResult["id"] = sourceIndex++;
-		sourceResult["ast"] = ASTJsonConverter(false, m_compilerStack.sourceIndices()).toJson(m_compilerStack.ast(sourceName));
-		sourceResult["legacyAST"] = ASTJsonConverter(true, m_compilerStack.sourceIndices()).toJson(m_compilerStack.ast(sourceName));
+		if (isArtifactRequested(outputSelection, sourceName, "", "ast"))
+			sourceResult["ast"] = ASTJsonConverter(false, m_compilerStack.sourceIndices()).toJson(m_compilerStack.ast(sourceName));
+		if (isArtifactRequested(outputSelection, sourceName, "", "legacyAST"))
+			sourceResult["legacyAST"] = ASTJsonConverter(true, m_compilerStack.sourceIndices()).toJson(m_compilerStack.ast(sourceName));
 		output["sources"][sourceName] = sourceResult;
 	}
 
@@ -411,28 +468,48 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 
 		// ABI, documentation and metadata
 		Json::Value contractData(Json::objectValue);
-		contractData["abi"] = m_compilerStack.contractABI(contractName);
-		contractData["metadata"] = m_compilerStack.metadata(contractName);
-		contractData["userdoc"] = m_compilerStack.natspecUser(contractName);
-		contractData["devdoc"] = m_compilerStack.natspecDev(contractName);
+		if (isArtifactRequested(outputSelection, file, name, "abi"))
+			contractData["abi"] = m_compilerStack.contractABI(contractName);
+		if (isArtifactRequested(outputSelection, file, name, "metadata"))
+			contractData["metadata"] = m_compilerStack.metadata(contractName);
+		if (isArtifactRequested(outputSelection, file, name, "userdoc"))
+			contractData["userdoc"] = m_compilerStack.natspecUser(contractName);
+		if (isArtifactRequested(outputSelection, file, name, "devdoc"))
+			contractData["devdoc"] = m_compilerStack.natspecDev(contractName);
 
 		// EVM
 		Json::Value evmData(Json::objectValue);
 		// @TODO: add ir
-		evmData["assembly"] = m_compilerStack.assemblyString(contractName, createSourceList(_input));
-		evmData["legacyAssembly"] = m_compilerStack.assemblyJSON(contractName, createSourceList(_input));
-		evmData["methodIdentifiers"] = m_compilerStack.methodIdentifiers(contractName);
-		evmData["gasEstimates"] = m_compilerStack.gasEstimates(contractName);
-
-		evmData["bytecode"] = collectEVMObject(
-			m_compilerStack.object(contractName),
-			m_compilerStack.sourceMapping(contractName)
-		);
-
-		evmData["deployedBytecode"] = collectEVMObject(
-			m_compilerStack.runtimeObject(contractName),
-			m_compilerStack.runtimeSourceMapping(contractName)
-		);
+		if (isArtifactRequested(outputSelection, file, name, "evm.assembly"))
+			evmData["assembly"] = m_compilerStack.assemblyString(contractName, createSourceList(_input));
+		if (isArtifactRequested(outputSelection, file, name, "evm.legacyAssembly"))
+			evmData["legacyAssembly"] = m_compilerStack.assemblyJSON(contractName, createSourceList(_input));
+		if (isArtifactRequested(outputSelection, file, name, "evm.methodIdentifiers"))
+			evmData["methodIdentifiers"] = m_compilerStack.methodIdentifiers(contractName);
+		if (isArtifactRequested(outputSelection, file, name, "evm.gasEstimates"))
+			evmData["gasEstimates"] = m_compilerStack.gasEstimates(contractName);
+
+		if (isArtifactRequested(
+			outputSelection,
+			file,
+			name,
+			{ "evm.bytecode", "evm.bytecode.object", "evm.bytecode.opcodes", "evm.bytecode.sourceMap", "evm.bytecode.linkReferences" }
+		))
+			evmData["bytecode"] = collectEVMObject(
+				m_compilerStack.object(contractName),
+				m_compilerStack.sourceMapping(contractName)
+			);
+
+		if (isArtifactRequested(
+			outputSelection,
+			file,
+			name,
+			{ "evm.deployedBytecode", "evm.deployedBytecode.object", "evm.deployedBytecode.opcodes", "evm.deployedBytecode.sourceMap", "evm.deployedBytecode.linkReferences" }
+		))
+			evmData["deployedBytecode"] = collectEVMObject(
+				m_compilerStack.runtimeObject(contractName),
+				m_compilerStack.runtimeSourceMapping(contractName)
+			);
 
 		contractData["evm"] = evmData;