diff --git a/Changelog.md b/Changelog.md
index 02d67924f..70cde92e9 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -9,6 +9,7 @@ Language Features:
 
 Compiler Features:
  * Export compiler-generated utility sources via standard-json or combined-json.
+ * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
@@ -16,13 +17,16 @@ Compiler Features:
  * Yul Optimizer: Prune unused parameters in functions.
  * Yul Optimizer: Inline into functions further down in the call graph first.
  * Yul Optimizer: Try to simplify function names.
+ * Yul IR Generator: Report source locations related to unimplemented features.
 
 
 Bugfixes:
+ * Code generator: Fix internal error on stripping dynamic types from return parameters on EVM versions without ``RETURNDATACOPY``.
  * Type Checker: Disallow ``virtual`` for modifiers in libraries.
  * Type Checker: Correct the warning for homonymous, but not shadowing declarations.
  * ViewPureChecker: Prevent visibility check on constructors.
  * Type system: Fix internal error on implicit conversion of contract instance to the type of its ``super``.
+ * Type system: Fix internal error on implicit conversion of string literal to a calldata string.
  * Type system: Fix named parameters in overloaded function and event calls being matched incorrectly if the order differs from the declaration.
 
 ### 0.7.1 (2020-09-02)
diff --git a/docs/installing-solidity.rst b/docs/installing-solidity.rst
index 7a5c52d71..d975c2611 100644
--- a/docs/installing-solidity.rst
+++ b/docs/installing-solidity.rst
@@ -163,8 +163,13 @@ Homebrew formula directly from Github.
 View
 `solidity.rb commits on Github <https://github.com/ethereum/homebrew-ethereum/commits/master/solidity.rb>`_.
 
-Follow the history links until you have a raw file link of a
-specific commit of ``solidity.rb``.
+Copy the commit hash of the version you want and check it out on your machine.
+
+.. code-block:: bash
+
+    git clone https://github.com/ethereum/homebrew-ethereum.git
+    cd homebrew-ethereum
+    git checkout <your-hash-goes-here>
 
 Install it using ``brew``:
 
@@ -172,7 +177,7 @@ Install it using ``brew``:
 
     brew unlink solidity
     # eg. Install 0.4.8
-    brew install https://raw.githubusercontent.com/ethereum/homebrew-ethereum/77cce03da9f289e5a3ffe579840d3c5dc0a62717/solidity.rb
+    brew install solidity.rb
 
 Gentoo Linux has an `Ethereum overlay <https://overlays.gentoo.org/#ethereum>`_ that contains a solidity package.
 After the overlay is setup, ``solc`` can be installed in x86_64 architectures by:
diff --git a/docs/yul.rst b/docs/yul.rst
index c7c7fdb33..281cb8d63 100644
--- a/docs/yul.rst
+++ b/docs/yul.rst
@@ -1110,6 +1110,7 @@ Abbreviation Full name
 ``L``        ``LoadResolver``
 ``M``        ``LoopInvariantCodeMotion``
 ``r``        ``RedundantAssignEliminator``
+``R``        ``ReasoningBasedSimplifier`` - highly experimental
 ``m``        ``Rematerialiser``
 ``V``        ``SSAReverser``
 ``a``        ``SSATransform``
@@ -1121,6 +1122,10 @@ Abbreviation Full name
 Some steps depend on properties ensured by ``BlockFlattener``, ``FunctionGrouper``, ``ForLoopInitRewriter``.
 For this reason the Yul optimizer always applies them before applying any steps supplied by the user.
 
+The ReasoningBasedSimplifier is an optimizer step that is currently not enabled
+in the default set of steps. It uses an SMT solver to simplify arithmetic expressions
+and boolean conditions. It has not received thorough testing or validation yet and can produce
+non-reproducible results, so please use with care!
 
 .. _erc20yul:
 
diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt
index 62b52f5c6..8c8b3677d 100644
--- a/libsmtutil/CMakeLists.txt
+++ b/libsmtutil/CMakeLists.txt
@@ -9,6 +9,7 @@ set(sources
 	SolverInterface.h
 	Sorts.cpp
 	Sorts.h
+	Helpers.h
 )
 
 if (${Z3_FOUND})
diff --git a/libsmtutil/Helpers.h b/libsmtutil/Helpers.h
new file mode 100644
index 000000000..fa6081b16
--- /dev/null
+++ b/libsmtutil/Helpers.h
@@ -0,0 +1,58 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsmtutil/SolverInterface.h>
+
+namespace solidity::smtutil
+{
+
+/// Signed division in SMTLIB2 rounds differently than EVM.
+/// This does not check for division by zero!
+inline Expression signedDivision(Expression _left, Expression _right)
+{
+	return Expression::ite(
+		_left >= 0,
+		Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
+		Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
+	);
+}
+
+inline Expression abs(Expression _value)
+{
+	return Expression::ite(_value >= 0, _value, 0 - _value);
+}
+
+/// Signed modulo in SMTLIB2 behaves differently with regards
+/// to the sign than EVM.
+/// This does not check for modulo by zero!
+inline Expression signedModulo(Expression _left, Expression _right)
+{
+	return Expression::ite(
+		_left >= 0,
+		_left % _right,
+		Expression::ite(
+			(_left % _right) == 0,
+			0,
+			(_left % _right) - abs(_right)
+		)
+	);
+}
+
+}
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt
index 8feb665e0..091c87cd4 100644
--- a/libsolidity/CMakeLists.txt
+++ b/libsolidity/CMakeLists.txt
@@ -104,6 +104,8 @@ set(sources
 	formal/ModelChecker.h
 	formal/Predicate.cpp
 	formal/Predicate.h
+	formal/PredicateSort.cpp
+	formal/PredicateSort.h
 	formal/SMTEncoder.cpp
 	formal/SMTEncoder.h
 	formal/SSAVariable.cpp
diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp
index 6191faf4f..b0418dee5 100644
--- a/libsolidity/ast/Types.cpp
+++ b/libsolidity/ast/Types.cpp
@@ -1408,6 +1408,7 @@ BoolResult StringLiteralType::isImplicitlyConvertibleTo(Type const& _convertTo)
 		return static_cast<size_t>(fixedBytes->numBytes()) >= m_value.size();
 	else if (auto arrayType = dynamic_cast<ArrayType const*>(&_convertTo))
 		return
+			arrayType->location() != DataLocation::CallData &&
 			arrayType->isByteArray() &&
 			!(arrayType->dataStoredIn(DataLocation::Storage) && arrayType->isPointer()) &&
 			!(arrayType->isString() && !util::validateUTF8(value()));
@@ -3010,7 +3011,7 @@ TypePointers FunctionType::returnParameterTypesWithoutDynamicTypes() const
 		m_kind == Kind::BareStaticCall
 	)
 		for (auto& param: returnParameterTypes)
-			if (param->isDynamicallySized() && !param->dataStoredIn(DataLocation::Storage))
+			if (param->isDynamicallyEncoded() && !param->dataStoredIn(DataLocation::Storage))
 				param = TypeProvider::inaccessibleDynamic();
 
 	return returnParameterTypes;
diff --git a/libsolidity/codegen/ir/IRGenerator.cpp b/libsolidity/codegen/ir/IRGenerator.cpp
index 8fb932d01..151b8c9fd 100644
--- a/libsolidity/codegen/ir/IRGenerator.cpp
+++ b/libsolidity/codegen/ir/IRGenerator.cpp
@@ -164,7 +164,7 @@ string IRGenerator::generate(
 string IRGenerator::generate(Block const& _block)
 {
 	IRGeneratorForStatements generator(m_context, m_utils);
-	_block.accept(generator);
+	generator.generate(_block);
 	return generator.code();
 }
 
diff --git a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
index 34b677c9c..176f876bd 100644
--- a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
+++ b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
@@ -38,6 +38,8 @@
 #include <libyul/Dialect.h>
 #include <libyul/optimiser/ASTCopier.h>
 
+#include <liblangutil/Exceptions.h>
+
 #include <libsolutil/Whiskers.h>
 #include <libsolutil/StringUtils.h>
 #include <libsolutil/Keccak256.h>
@@ -152,70 +154,130 @@ string IRGeneratorForStatements::code() const
 	return m_code.str();
 }
 
+void IRGeneratorForStatements::generate(Block const& _block)
+{
+	try
+	{
+		_block.accept(*this);
+	}
+	catch (langutil::UnimplementedFeatureError const& _error)
+	{
+		if (!boost::get_error_info<langutil::errinfo_sourceLocation>(_error))
+			_error << langutil::errinfo_sourceLocation(m_currentLocation);
+		throw _error;
+	}
+}
+
 void IRGeneratorForStatements::initializeStateVar(VariableDeclaration const& _varDecl)
 {
-	solAssert(_varDecl.immutable() || m_context.isStateVariable(_varDecl), "Must be immutable or a state variable.");
-	solAssert(!_varDecl.isConstant(), "");
-	if (!_varDecl.value())
-		return;
+	try
+	{
+		setLocation(_varDecl);
 
-	_varDecl.value()->accept(*this);
-	writeToLValue(
-		_varDecl.immutable() ?
-		IRLValue{*_varDecl.annotation().type, IRLValue::Immutable{&_varDecl}} :
-		IRLValue{*_varDecl.annotation().type, IRLValue::Storage{
-			util::toCompactHexWithPrefix(m_context.storageLocationOfStateVariable(_varDecl).first),
-			m_context.storageLocationOfStateVariable(_varDecl).second
-		}},
-		*_varDecl.value()
-	);
+		solAssert(_varDecl.immutable() || m_context.isStateVariable(_varDecl), "Must be immutable or a state variable.");
+		solAssert(!_varDecl.isConstant(), "");
+		if (!_varDecl.value())
+			return;
+
+		_varDecl.value()->accept(*this);
+		writeToLValue(
+			_varDecl.immutable() ?
+			IRLValue{*_varDecl.annotation().type, IRLValue::Immutable{&_varDecl}} :
+			IRLValue{*_varDecl.annotation().type, IRLValue::Storage{
+				util::toCompactHexWithPrefix(m_context.storageLocationOfStateVariable(_varDecl).first),
+				m_context.storageLocationOfStateVariable(_varDecl).second
+			}},
+			*_varDecl.value()
+		);
+	}
+	catch (langutil::UnimplementedFeatureError const& _error)
+	{
+		if (!boost::get_error_info<langutil::errinfo_sourceLocation>(_error))
+			_error << langutil::errinfo_sourceLocation(m_currentLocation);
+		throw _error;
+	}
 }
 
 void IRGeneratorForStatements::initializeLocalVar(VariableDeclaration const& _varDecl)
 {
-	solAssert(m_context.isLocalVariable(_varDecl), "Must be a local variable.");
+	try
+	{
+		setLocation(_varDecl);
 
-	auto const* type = _varDecl.type();
-	if (auto const* refType = dynamic_cast<ReferenceType const*>(type))
-		if (refType->dataStoredIn(DataLocation::Storage) && refType->isPointer())
-			return;
+		solAssert(m_context.isLocalVariable(_varDecl), "Must be a local variable.");
 
-	IRVariable zero = zeroValue(*type);
-	assign(m_context.localVariable(_varDecl), zero);
+		auto const* type = _varDecl.type();
+		if (auto const* refType = dynamic_cast<ReferenceType const*>(type))
+			if (refType->dataStoredIn(DataLocation::Storage) && refType->isPointer())
+				return;
+
+		IRVariable zero = zeroValue(*type);
+		assign(m_context.localVariable(_varDecl), zero);
+	}
+	catch (langutil::UnimplementedFeatureError const& _error)
+	{
+		if (!boost::get_error_info<langutil::errinfo_sourceLocation>(_error))
+			_error << langutil::errinfo_sourceLocation(m_currentLocation);
+		throw _error;
+	}
 }
 
 IRVariable IRGeneratorForStatements::evaluateExpression(Expression const& _expression, Type const& _targetType)
 {
-	_expression.accept(*this);
-	IRVariable variable{m_context.newYulVariable(), _targetType};
-	define(variable, _expression);
-	return variable;
+	try
+	{
+		setLocation(_expression);
+
+		_expression.accept(*this);
+		IRVariable variable{m_context.newYulVariable(), _targetType};
+		define(variable, _expression);
+		return variable;
+	}
+	catch (langutil::UnimplementedFeatureError const& _error)
+	{
+		if (!boost::get_error_info<langutil::errinfo_sourceLocation>(_error))
+			_error << langutil::errinfo_sourceLocation(m_currentLocation);
+		throw _error;
+	}
 }
 
 string IRGeneratorForStatements::constantValueFunction(VariableDeclaration const& _constant)
 {
-	string functionName = IRNames::constantValueFunction(_constant);
-	return m_context.functionCollector().createFunction(functionName, [&] {
-		Whiskers templ(R"(
-			function <functionName>() -> <ret> {
-				<code>
-				<ret> := <value>
-			}
-		)");
-		templ("functionName", functionName);
-		IRGeneratorForStatements generator(m_context, m_utils);
-		solAssert(_constant.value(), "");
-		Type const& constantType = *_constant.type();
-		templ("value", generator.evaluateExpression(*_constant.value(), constantType).commaSeparatedList());
-		templ("code", generator.code());
-		templ("ret", IRVariable("ret", constantType).commaSeparatedList());
+	try
+	{
+		setLocation(_constant);
 
-		return templ.render();
-	});
+		string functionName = IRNames::constantValueFunction(_constant);
+		return m_context.functionCollector().createFunction(functionName, [&] {
+			Whiskers templ(R"(
+				function <functionName>() -> <ret> {
+					<code>
+					<ret> := <value>
+				}
+			)");
+			templ("functionName", functionName);
+			IRGeneratorForStatements generator(m_context, m_utils);
+			solAssert(_constant.value(), "");
+			Type const& constantType = *_constant.type();
+			templ("value", generator.evaluateExpression(*_constant.value(), constantType).commaSeparatedList());
+			templ("code", generator.code());
+			templ("ret", IRVariable("ret", constantType).commaSeparatedList());
+
+			return templ.render();
+		});
+	}
+	catch (langutil::UnimplementedFeatureError const& _error)
+	{
+		if (!boost::get_error_info<langutil::errinfo_sourceLocation>(_error))
+			_error << langutil::errinfo_sourceLocation(m_currentLocation);
+		throw _error;
+	}
 }
 
 void IRGeneratorForStatements::endVisit(VariableDeclarationStatement const& _varDeclStatement)
 {
+	setLocation(_varDeclStatement);
+
 	if (Expression const* expression = _varDeclStatement.initialValue())
 	{
 		if (_varDeclStatement.declarations().size() > 1)
@@ -249,14 +311,22 @@ bool IRGeneratorForStatements::visit(Conditional const& _conditional)
 {
 	_conditional.condition().accept(*this);
 
+	setLocation(_conditional);
+
 	string condition = expressionAsType(_conditional.condition(), *TypeProvider::boolean());
 	declare(_conditional);
 
 	m_code << "switch " << condition << "\n" "case 0 {\n";
+
 	_conditional.falseExpression().accept(*this);
+	setLocation(_conditional);
+
 	assign(_conditional, _conditional.falseExpression());
 	m_code << "}\n" "default {\n";
+
 	_conditional.trueExpression().accept(*this);
+	setLocation(_conditional);
+
 	assign(_conditional, _conditional.trueExpression());
 	m_code << "}\n";
 
@@ -266,6 +336,7 @@ bool IRGeneratorForStatements::visit(Conditional const& _conditional)
 bool IRGeneratorForStatements::visit(Assignment const& _assignment)
 {
 	_assignment.rightHandSide().accept(*this);
+	setLocation(_assignment);
 
 	Token assignmentOperator = _assignment.assignmentOperator();
 	Token binaryOperator =
@@ -283,6 +354,7 @@ bool IRGeneratorForStatements::visit(Assignment const& _assignment)
 	IRVariable value = convert(_assignment.rightHandSide(), *rightIntermediateType);
 	_assignment.leftHandSide().accept(*this);
 	solAssert(!!m_currentLValue, "LValue not retrieved.");
+	setLocation(_assignment);
 
 	if (assignmentOperator != Token::Assign)
 	{
@@ -323,6 +395,8 @@ bool IRGeneratorForStatements::visit(Assignment const& _assignment)
 
 bool IRGeneratorForStatements::visit(TupleExpression const& _tuple)
 {
+	setLocation(_tuple);
+
 	if (_tuple.isInlineArray())
 	{
 		auto const& arrayType = dynamic_cast<ArrayType const&>(*_tuple.annotation().type);
@@ -339,6 +413,7 @@ bool IRGeneratorForStatements::visit(TupleExpression const& _tuple)
 		{
 			Expression const& component = *_tuple.components()[i];
 			component.accept(*this);
+			setLocation(_tuple);
 			IRVariable converted = convert(component, baseType);
 			m_code <<
 				m_utils.writeToMemoryFunction(baseType) <<
@@ -358,6 +433,7 @@ bool IRGeneratorForStatements::visit(TupleExpression const& _tuple)
 		{
 			solAssert(_tuple.components().front(), "");
 			_tuple.components().front()->accept(*this);
+			setLocation(_tuple);
 			if (willBeWrittenTo)
 				solAssert(!!m_currentLValue, "");
 			else
@@ -370,6 +446,7 @@ bool IRGeneratorForStatements::visit(TupleExpression const& _tuple)
 				if (auto const& component = _tuple.components()[i])
 				{
 					component->accept(*this);
+					setLocation(_tuple);
 					if (willBeWrittenTo)
 					{
 						solAssert(!!m_currentLValue, "");
@@ -395,17 +472,20 @@ bool IRGeneratorForStatements::visit(TupleExpression const& _tuple)
 bool IRGeneratorForStatements::visit(IfStatement const& _ifStatement)
 {
 	_ifStatement.condition().accept(*this);
+	setLocation(_ifStatement);
 	string condition = expressionAsType(_ifStatement.condition(), *TypeProvider::boolean());
 
 	if (_ifStatement.falseStatement())
 	{
 		m_code << "switch " << condition << "\n" "case 0 {\n";
 		_ifStatement.falseStatement()->accept(*this);
+		setLocation(_ifStatement);
 		m_code << "}\n" "default {\n";
 	}
 	else
 		m_code << "if " << condition << " {\n";
 	_ifStatement.trueStatement().accept(*this);
+	setLocation(_ifStatement);
 	m_code << "}\n";
 
 	return false;
@@ -413,6 +493,7 @@ bool IRGeneratorForStatements::visit(IfStatement const& _ifStatement)
 
 bool IRGeneratorForStatements::visit(ForStatement const& _forStatement)
 {
+	setLocation(_forStatement);
 	generateLoop(
 		_forStatement.body(),
 		_forStatement.condition(),
@@ -425,6 +506,7 @@ bool IRGeneratorForStatements::visit(ForStatement const& _forStatement)
 
 bool IRGeneratorForStatements::visit(WhileStatement const& _whileStatement)
 {
+	setLocation(_whileStatement);
 	generateLoop(
 		_whileStatement.body(),
 		&_whileStatement.condition(),
@@ -436,20 +518,23 @@ bool IRGeneratorForStatements::visit(WhileStatement const& _whileStatement)
 	return false;
 }
 
-bool IRGeneratorForStatements::visit(Continue const&)
+bool IRGeneratorForStatements::visit(Continue const& _continue)
 {
+	setLocation(_continue);
 	m_code << "continue\n";
 	return false;
 }
 
-bool IRGeneratorForStatements::visit(Break const&)
+bool IRGeneratorForStatements::visit(Break const& _break)
 {
+	setLocation(_break);
 	m_code << "break\n";
 	return false;
 }
 
 void IRGeneratorForStatements::endVisit(Return const& _return)
 {
+	setLocation(_return);
 	if (Expression const* value = _return.expression())
 	{
 		solAssert(_return.annotation().functionReturnParameters, "Invalid return parameters pointer.");
@@ -466,6 +551,7 @@ void IRGeneratorForStatements::endVisit(Return const& _return)
 
 void IRGeneratorForStatements::endVisit(UnaryOperation const& _unaryOperation)
 {
+	setLocation(_unaryOperation);
 	Type const& resultType = type(_unaryOperation);
 	Token const op = _unaryOperation.getOperator();
 
@@ -551,6 +637,8 @@ void IRGeneratorForStatements::endVisit(UnaryOperation const& _unaryOperation)
 
 bool IRGeneratorForStatements::visit(BinaryOperation const& _binOp)
 {
+	setLocation(_binOp);
+
 	solAssert(!!_binOp.annotation().commonType, "");
 	TypePointer commonType = _binOp.annotation().commonType;
 	langutil::Token op = _binOp.getOperator();
@@ -570,6 +658,7 @@ bool IRGeneratorForStatements::visit(BinaryOperation const& _binOp)
 
 	_binOp.leftExpression().accept(*this);
 	_binOp.rightExpression().accept(*this);
+	setLocation(_binOp);
 
 	if (TokenTraits::isCompareOp(op))
 	{
@@ -629,6 +718,7 @@ bool IRGeneratorForStatements::visit(BinaryOperation const& _binOp)
 
 bool IRGeneratorForStatements::visit(FunctionCall const& _functionCall)
 {
+	setLocation(_functionCall);
 	FunctionTypePointer functionType = dynamic_cast<FunctionType const*>(&type(_functionCall.expression()));
 	if (
 		functionType &&
@@ -643,6 +733,7 @@ bool IRGeneratorForStatements::visit(FunctionCall const& _functionCall)
 
 void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 {
+	setLocation(_functionCall);
 	auto functionCallKind = *_functionCall.annotation().kind;
 
 	if (functionCallKind == FunctionCallKind::TypeConversion)
@@ -1360,6 +1451,7 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 
 void IRGeneratorForStatements::endVisit(FunctionCallOptions const& _options)
 {
+	setLocation(_options);
 	FunctionType const& previousType = dynamic_cast<FunctionType const&>(*_options.expression().annotation().type);
 
 	solUnimplementedAssert(!previousType.bound(), "");
@@ -1379,6 +1471,7 @@ void IRGeneratorForStatements::endVisit(FunctionCallOptions const& _options)
 
 void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 {
+	setLocation(_memberAccess);
 	ASTString const& member = _memberAccess.memberName();
 	auto memberFunctionType = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type);
 	Type::Category objectCategory = _memberAccess.expression().annotation().type->category();
@@ -1764,6 +1857,7 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 
 bool IRGeneratorForStatements::visit(InlineAssembly const& _inlineAsm)
 {
+	setLocation(_inlineAsm);
 	CopyTranslate bodyCopier{_inlineAsm.dialect(), m_context, _inlineAsm.annotation().externalReferences};
 
 	yul::Statement modified = bodyCopier(_inlineAsm.operations());
@@ -1778,6 +1872,7 @@ bool IRGeneratorForStatements::visit(InlineAssembly const& _inlineAsm)
 
 void IRGeneratorForStatements::endVisit(IndexAccess const& _indexAccess)
 {
+	setLocation(_indexAccess);
 	Type const& baseType = *_indexAccess.baseExpression().annotation().type;
 
 	if (baseType.category() == Type::Category::Mapping)
@@ -1913,6 +2008,7 @@ void IRGeneratorForStatements::endVisit(IndexAccess const& _indexAccess)
 
 void IRGeneratorForStatements::endVisit(IndexRangeAccess const& _indexRangeAccess)
 {
+	setLocation(_indexRangeAccess);
 	Type const& baseType = *_indexRangeAccess.baseExpression().annotation().type;
 	solAssert(
 		baseType.category() == Type::Category::Array || baseType.category() == Type::Category::ArraySlice,
@@ -1959,6 +2055,7 @@ void IRGeneratorForStatements::endVisit(IndexRangeAccess const& _indexRangeAcces
 
 void IRGeneratorForStatements::endVisit(Identifier const& _identifier)
 {
+	setLocation(_identifier);
 	Declaration const* declaration = _identifier.annotation().referencedDeclaration;
 	if (MagicVariableDeclaration const* magicVar = dynamic_cast<MagicVariableDeclaration const*>(declaration))
 	{
@@ -2017,6 +2114,7 @@ void IRGeneratorForStatements::endVisit(Identifier const& _identifier)
 
 bool IRGeneratorForStatements::visit(Literal const& _literal)
 {
+	setLocation(_literal);
 	Type const& literalType = type(_literal);
 
 	switch (literalType.category())
@@ -2039,6 +2137,7 @@ void IRGeneratorForStatements::handleVariableReference(
 	Expression const& _referencingExpression
 )
 {
+	setLocation(_referencingExpression);
 	if (_variable.isStateVariable() && _variable.isConstant())
 		define(_referencingExpression) << constantValueFunction(_variable) << "()\n";
 	else if (_variable.isStateVariable() && _variable.immutable())
@@ -2480,6 +2579,7 @@ void IRGeneratorForStatements::appendAndOrOperatorCode(BinaryOperation const& _b
 	solAssert(op == Token::Or || op == Token::And, "");
 
 	_binOp.leftExpression().accept(*this);
+	setLocation(_binOp);
 
 	IRVariable value(_binOp);
 	define(value, _binOp.leftExpression());
@@ -2488,6 +2588,7 @@ void IRGeneratorForStatements::appendAndOrOperatorCode(BinaryOperation const& _b
 	else
 		m_code << "if " << value.name() << " {\n";
 	_binOp.rightExpression().accept(*this);
+	setLocation(_binOp);
 	assign(value, _binOp.rightExpression());
 	m_code << "}\n";
 }
@@ -2687,6 +2788,7 @@ bool IRGeneratorForStatements::visit(TryStatement const& _tryStatement)
 {
 	Expression const& externalCall = _tryStatement.externalCall();
 	externalCall.accept(*this);
+	setLocation(_tryStatement);
 
 	m_code << "switch iszero(" << IRNames::trySuccessConditionVariable(externalCall) << ")\n";
 
@@ -2707,6 +2809,7 @@ bool IRGeneratorForStatements::visit(TryStatement const& _tryStatement)
 	}
 
 	successClause.block().accept(*this);
+	setLocation(_tryStatement);
 	m_code << "}\n";
 
 	m_code << "default { // failure case\n";
@@ -2797,3 +2900,8 @@ bool IRGeneratorForStatements::visit(TryCatchClause const& _clause)
 	_clause.block().accept(*this);
 	return false;
 }
+
+void IRGeneratorForStatements::setLocation(ASTNode const& _node)
+{
+	m_currentLocation = _node.location();
+}
diff --git a/libsolidity/codegen/ir/IRGeneratorForStatements.h b/libsolidity/codegen/ir/IRGeneratorForStatements.h
index 09c9c7d27..3d87eae57 100644
--- a/libsolidity/codegen/ir/IRGeneratorForStatements.h
+++ b/libsolidity/codegen/ir/IRGeneratorForStatements.h
@@ -47,6 +47,9 @@ public:
 
 	std::string code() const;
 
+	/// Generate the code for the statements in the block;
+	void generate(Block const& _block);
+
 	/// Generates code to initialize the given state variable.
 	void initializeStateVar(VariableDeclaration const& _varDecl);
 	/// Generates code to initialize the given local variable.
@@ -179,10 +182,13 @@ private:
 
 	static Type const& type(Expression const& _expression);
 
+	void setLocation(ASTNode const& _node);
+
 	std::ostringstream m_code;
 	IRGenerationContext& m_context;
 	YulUtilFunctions& m_utils;
 	std::optional<IRLValue> m_currentLValue;
+	langutil::SourceLocation m_currentLocation;
 };
 
 }
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 39b7ae593..b26e34942 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -22,6 +22,7 @@
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
 
+#include <libsolidity/formal/PredicateSort.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsolidity/ast/TypeProvider.h>
@@ -39,13 +40,14 @@ using namespace solidity::util;
 using namespace solidity::langutil;
 using namespace solidity::smtutil;
 using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 CHC::CHC(
-	smt::EncodingContext& _context,
+	EncodingContext& _context,
 	ErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers
+	SMTSolverChoice _enabledSolvers
 ):
 	SMTEncoder(_context),
 	m_outerErrorReporter(_errorReporter),
@@ -56,7 +58,7 @@ CHC::CHC(
 	usesZ3 = false;
 #endif
 	if (!usesZ3)
-		m_interface = make_unique<smtutil::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
+		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -79,7 +81,7 @@ void CHC::analyze(SourceUnit const& _source)
 
 vector<string> CHC::unhandledQueries() const
 {
-	if (auto smtlib2 = dynamic_cast<smtutil::CHCSmtLib2Interface const*>(m_interface.get()))
+	if (auto smtlib2 = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		return smtlib2->unhandledQueries();
 
 	return {};
@@ -92,13 +94,15 @@ bool CHC::visit(ContractDefinition const& _contract)
 	initContract(_contract);
 
 	m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
-	m_stateSorts = stateSorts(_contract);
 
 	clearIndices(&_contract);
 
-	string suffix = _contract.name() + "_" + to_string(_contract.id());
-	m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix, &_contract);
-	m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix, &_contract);
+	solAssert(m_currentContract, "");
+	m_constructorSummaryPredicate = createSymbolicBlock(
+		constructorSort(*m_currentContract),
+		"summary_constructor_" + contractSuffix(_contract),
+		&_contract
+	);
 	auto stateExprs = currentStateVariables();
 	setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
@@ -108,7 +112,12 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 void CHC::endVisit(ContractDefinition const& _contract)
 {
-	auto implicitConstructor = (*m_implicitConstructorPredicate)({});
+	auto implicitConstructorPredicate = createSymbolicBlock(
+		implicitConstructorSort(),
+		"implicit_constructor_" + contractSuffix(_contract),
+		&_contract
+	);
+	auto implicitConstructor = (*implicitConstructorPredicate)({});
 	addRule(implicitConstructor, implicitConstructor.name);
 	m_currentBlock = implicitConstructor;
 	m_context.addAssertion(m_error.currentValue() == 0);
@@ -204,7 +213,12 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		if (_function.isConstructor())
 		{
 			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
-			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix, m_currentContract);
+			solAssert(m_currentContract, "");
+			auto constructorExit = createSymbolicBlock(
+				constructorSort(*m_currentContract),
+				"constructor_exit_" + suffix,
+				m_currentContract
+			);
 			connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
 
 			clearIndices(m_currentContract, m_currentFunction);
@@ -566,7 +580,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 
 	auto memberAccess = dynamic_cast<MemberAccess const*>(&_arrayPop.expression());
 	solAssert(memberAccess, "");
-	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
 	auto previousError = m_error.currentValue();
@@ -662,15 +676,15 @@ void CHC::resetSourceAnalysis()
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
-		m_interface.reset(new smtutil::Z3CHCInterface());
-		auto z3Interface = dynamic_cast<smtutil::Z3CHCInterface const*>(m_interface.get());
+		m_interface.reset(new Z3CHCInterface());
+		auto z3Interface = dynamic_cast<Z3CHCInterface const*>(m_interface.get());
 		solAssert(z3Interface, "");
 		m_context.setSolver(z3Interface->z3Interface());
 	}
 #endif
 	if (!usesZ3)
 	{
-		auto smtlib2Interface = dynamic_cast<smtutil::CHCSmtLib2Interface*>(m_interface.get());
+		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
 		smtlib2Interface->reset();
 		solAssert(smtlib2Interface, "");
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
@@ -682,7 +696,6 @@ void CHC::resetSourceAnalysis()
 
 void CHC::resetContractAnalysis()
 {
-	m_stateSorts.clear();
 	m_stateVariables.clear();
 	m_unknownFunctionCallSeen = false;
 	m_breakDest = nullptr;
@@ -739,117 +752,18 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
 	return assertions;
 }
 
-vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
+SortPointer CHC::sort(FunctionDefinition const& _function)
 {
-	return applyMap(
-		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
-		[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
-	);
+	return functionSort(_function, m_currentContract);
 }
 
-smtutil::SortPointer CHC::constructorSort()
-{
-	solAssert(m_currentContract, "");
-	if (auto const* constructor = m_currentContract->constructor())
-		return sort(*constructor);
-
-	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + m_stateSorts,
-		smtutil::SortProvider::boolSort
-	);
-}
-
-smtutil::SortPointer CHC::interfaceSort()
-{
-	solAssert(m_currentContract, "");
-	return interfaceSort(*m_currentContract);
-}
-
-smtutil::SortPointer CHC::nondetInterfaceSort()
-{
-	solAssert(m_currentContract, "");
-	return nondetInterfaceSort(*m_currentContract);
-}
-
-smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
-{
-	return make_shared<smtutil::FunctionSort>(
-		stateSorts(_contract),
-		smtutil::SortProvider::boolSort
-	);
-}
-
-smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contract)
-{
-	auto sorts = stateSorts(_contract);
-	return make_shared<smtutil::FunctionSort>(
-		sorts + sorts,
-		smtutil::SortProvider::boolSort
-	);
-}
-
-smtutil::SortPointer CHC::arity0FunctionSort() const
-{
-	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>(),
-		smtutil::SortProvider::boolSort
-	);
-}
-
-/// A function in the symbolic CFG requires:
-/// - Index of failed assertion. 0 means no assertion failed.
-/// - 2 sets of state variables:
-///   - State variables at the beginning of the current function, immutable
-///   - Current state variables
-///    At the beginning of the function these must equal set 1
-/// - 2 sets of input variables:
-///   - Input variables at the beginning of the current function, immutable
-///   - Current input variables
-///    At the beginning of the function these must equal set 1
-/// - 1 set of output variables
-smtutil::SortPointer CHC::sort(FunctionDefinition const& _function)
-{
-	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
-	auto inputSorts = applyMap(_function.parameters(), smtSort);
-	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
-	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
-		smtutil::SortProvider::boolSort
-	);
-}
-
-smtutil::SortPointer CHC::sort(ASTNode const* _node)
+SortPointer CHC::sort(ASTNode const* _node)
 {
 	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
 		return sort(*funDef);
 
-	auto fSort = dynamic_pointer_cast<smtutil::FunctionSort>(sort(*m_currentFunction));
-	solAssert(fSort, "");
-
-	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
-	return make_shared<smtutil::FunctionSort>(
-		fSort->domain + applyMap(m_currentFunction->localVariables(), smtSort),
-		smtutil::SortProvider::boolSort
-	);
-}
-
-smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
-{
-	auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
-	auto sorts = stateSorts(_contract);
-
-	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
-	auto inputSorts = applyMap(_function.parameters(), smtSort);
-	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
-	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} +
-			sorts +
-			inputSorts +
-			sorts +
-			inputSorts +
-			outputSorts,
-		smtutil::SortProvider::boolSort
-	);
+	solAssert(m_currentFunction, "");
+	return functionBodySort(*m_currentFunction, m_currentContract);
 }
 
 Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node)
@@ -987,7 +901,7 @@ Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix)
 Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
 	auto block = createSymbolicBlock(
-		summarySort(_function, _contract),
+		functionSort(_function, &_contract),
 		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
 		&_function
 	);
@@ -1157,14 +1071,14 @@ void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
 	m_interface->addRule(_rule, _ruleName);
 }
 
-pair<smtutil::CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
+pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
 {
-	smtutil::CheckResult result;
+	CheckResult result;
 	CHCSolverInterface::CexGraph cex;
 	tie(result, cex) = m_interface->query(_query);
 	switch (result)
 	{
-	case smtutil::CheckResult::SATISFIABLE:
+	case CheckResult::SATISFIABLE:
 	{
 #ifdef HAVE_Z3
 		// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
@@ -1173,25 +1087,25 @@ pair<smtutil::CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Exp
 		solAssert(spacer, "");
 		spacer->setSpacerOptions(false);
 
-		smtutil::CheckResult resultNoOpt;
+		CheckResult resultNoOpt;
 		CHCSolverInterface::CexGraph cexNoOpt;
 		tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
 
-		if (resultNoOpt == smtutil::CheckResult::SATISFIABLE)
+		if (resultNoOpt == CheckResult::SATISFIABLE)
 			cex = move(cexNoOpt);
 
 		spacer->setSpacerOptions(true);
 #endif
 		break;
 	}
-	case smtutil::CheckResult::UNSATISFIABLE:
+	case CheckResult::UNSATISFIABLE:
 		break;
-	case smtutil::CheckResult::UNKNOWN:
+	case CheckResult::UNKNOWN:
 		break;
-	case smtutil::CheckResult::CONFLICTING:
+	case CheckResult::CONFLICTING:
 		m_outerErrorReporter.warning(1988_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
 		break;
-	case smtutil::CheckResult::ERROR:
+	case CheckResult::ERROR:
 		m_outerErrorReporter.warning(1218_error, _location, "Error trying to invoke SMT solver.");
 		break;
 	}
@@ -1339,9 +1253,9 @@ void CHC::checkAndReportTarget(
 	createErrorBlock();
 	connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId));
 	auto const& [result, model] = query(error(), _scope->location());
-	if (result == smtutil::CheckResult::UNSATISFIABLE)
+	if (result == CheckResult::UNSATISFIABLE)
 		m_safeTargets[_scope].insert(_target.type);
-	else if (result == smtutil::CheckResult::SATISFIABLE)
+	else if (result == CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
 		m_unsafeTargets[_scope].insert(_target.type);
@@ -1477,7 +1391,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 	return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
 }
 
-string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
+string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
 {
 	string dot = "digraph {\n";
 
@@ -1498,6 +1412,11 @@ string CHC::uniquePrefix()
 	return to_string(m_blockCounter++);
 }
 
+string CHC::contractSuffix(ContractDefinition const& _contract)
+{
+	return _contract.name() + "_" + to_string(_contract.id());
+}
+
 unsigned CHC::newErrorId(frontend::Expression const& _expr)
 {
 	unsigned errorId = m_context.newUniqueId();
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 769c91aa4..7eee92eb7 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -117,19 +117,8 @@ private:
 
 	/// Sort helpers.
 	//@{
-	static std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract);
-	smtutil::SortPointer constructorSort();
-	smtutil::SortPointer interfaceSort();
-	smtutil::SortPointer nondetInterfaceSort();
-	static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
-	static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const);
-	smtutil::SortPointer arity0FunctionSort() const;
 	smtutil::SortPointer sort(FunctionDefinition const& _function);
 	smtutil::SortPointer sort(ASTNode const* _block);
-	/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
-	/// The _contract is also needed because the same function might be in many contracts due to inheritance,
-	/// where the sort changes because the set of state variables might change.
-	static smtutil::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
 	//@}
 
 	/// Predicate helpers.
@@ -246,10 +235,13 @@ private:
 
 	/// Misc.
 	//@{
-	/// Returns a prefix to be used in a new unique block name
+	/// @returns a prefix to be used in a new unique block name
 	/// and increases the block counter.
 	std::string uniquePrefix();
 
+	/// @returns a suffix to be used by contract related predicates.
+	std::string contractSuffix(ContractDefinition const& _contract);
+
 	/// @returns a new unique error id associated with _expr and stores
 	/// it into m_errorIds.
 	unsigned newErrorId(Expression const& _expr);
@@ -257,10 +249,6 @@ private:
 
 	/// Predicates.
 	//@{
-	/// Implicit constructor predicate.
-	/// Explicit constructors are handled as functions.
-	Predicate const* m_implicitConstructorPredicate = nullptr;
-
 	/// Constructor summary predicate, exists after the constructor
 	/// (implicit or explicit) and before the interface.
 	Predicate const* m_constructorSummaryPredicate = nullptr;
@@ -292,9 +280,6 @@ private:
 
 	/// Variables.
 	//@{
-	/// State variables sorts.
-	/// Used by all predicates.
-	std::vector<smtutil::SortPointer> m_stateSorts;
 	/// State variables.
 	/// Used to create all predicates.
 	std::vector<VariableDeclaration const*> m_stateVariables;
diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp
new file mode 100644
index 000000000..ffef00f0c
--- /dev/null
+++ b/libsolidity/formal/PredicateSort.cpp
@@ -0,0 +1,111 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/PredicateSort.h>
+
+#include <libsolidity/formal/SMTEncoder.h>
+#include <libsolidity/formal/SymbolicTypes.h>
+
+using namespace std;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+namespace solidity::frontend::smt
+{
+
+SortPointer interfaceSort(ContractDefinition const& _contract)
+{
+	return make_shared<FunctionSort>(
+		stateSorts(_contract),
+		SortProvider::boolSort
+	);
+}
+
+SortPointer nondetInterfaceSort(ContractDefinition const& _contract)
+{
+	auto varSorts = stateSorts(_contract);
+	return make_shared<FunctionSort>(
+		varSorts + varSorts,
+		SortProvider::boolSort
+	);
+}
+
+SortPointer implicitConstructorSort()
+{
+	return arity0FunctionSort();
+}
+
+SortPointer constructorSort(ContractDefinition const& _contract)
+{
+	if (auto const* constructor = _contract.constructor())
+		return functionSort(*constructor, &_contract);
+
+	return make_shared<FunctionSort>(
+		vector<SortPointer>{SortProvider::uintSort} + stateSorts(_contract),
+		SortProvider::boolSort
+	);
+}
+
+SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract)
+{
+	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
+	auto varSorts = _contract ? stateSorts(*_contract) : vector<SortPointer>{};
+	auto inputSorts = applyMap(_function.parameters(), smtSort);
+	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
+	return make_shared<FunctionSort>(
+		vector<SortPointer>{SortProvider::uintSort} +
+			varSorts +
+			inputSorts +
+			varSorts +
+			inputSorts +
+			outputSorts,
+		SortProvider::boolSort
+	);
+}
+
+SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract)
+{
+	auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract));
+	solAssert(fSort, "");
+
+	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
+	return make_shared<FunctionSort>(
+		fSort->domain + applyMap(_function.localVariables(), smtSort),
+		SortProvider::boolSort
+	);
+}
+
+SortPointer arity0FunctionSort()
+{
+	return make_shared<FunctionSort>(
+		vector<SortPointer>(),
+		SortProvider::boolSort
+	);
+}
+
+/// Helpers
+
+vector<SortPointer> stateSorts(ContractDefinition const& _contract)
+{
+	return applyMap(
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
+		[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
+	);
+}
+
+}
diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h
new file mode 100644
index 000000000..04d5226c6
--- /dev/null
+++ b/libsolidity/formal/PredicateSort.h
@@ -0,0 +1,82 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsolidity/formal/Predicate.h>
+
+#include <libsmtutil/Sorts.h>
+
+namespace solidity::frontend::smt
+{
+
+/**
+ * This file represents the specification for CHC predicate sorts.
+ * Types of predicates:
+ *
+ * 1. Interface
+ * The idle state of a contract. Signature:
+ * interface(stateVariables).
+ *
+ * 2. Nondet interface
+ * The nondeterminism behavior of a contract. Signature:
+ * nondet_interface(stateVariables, stateVariables').
+ *
+ * 3. Implicit constructor
+ * The implicit constructor of a contract, that is, without input parameters. Signature:
+ * implicit_constructor().
+ *
+ * 4. Constructor entry/summary
+ * The summary of an implicit constructor. Signature:
+ * constructor_summary(error, stateVariables').
+ *
+ * 5. Function entry/summary
+ * The entry point of a function definition. Signature:
+ * function_entry(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables').
+ *
+ * 6. Function body
+ * Use for any predicate within a function. Signature:
+ * function_body(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables', localVariables).
+ */
+
+/// @returns the interface predicate sort for _contract.
+smtutil::SortPointer interfaceSort(ContractDefinition const& _contract);
+
+/// @returns the nondeterminisc interface predicate sort for _contract.
+smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract);
+
+/// @returns the implicit constructor predicate sort.
+smtutil::SortPointer implicitConstructorSort();
+
+/// @returns the constructor entry/summary predicate sort for _contract.
+smtutil::SortPointer constructorSort(ContractDefinition const& _contract);
+
+/// @returns the function entry/summary predicate sort for _function contained in _contract.
+smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract);
+
+/// @returns the function body predicate sort for _function contained in _contract.
+smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract);
+
+/// @returns the sort of a predicate without parameters.
+smtutil::SortPointer arity0FunctionSort();
+
+/// Helpers
+
+std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract) ;
+
+}
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index e2a35a0d8..cb7322d62 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -23,6 +23,7 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/Helpers.h>
 
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
@@ -675,6 +676,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ArrayPop:
 		arrayPop(_funCall);
 		break;
+	case FunctionType::Kind::Log0:
+	case FunctionType::Kind::Log1:
+	case FunctionType::Kind::Log2:
+	case FunctionType::Kind::Log3:
+	case FunctionType::Kind::Log4:
+	case FunctionType::Kind::Event:
+		// These can be safely ignored.
+		break;
 	default:
 		m_errorReporter.warning(
 			4588_error,
@@ -1497,11 +1506,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.
 	if (_type.isSigned())
-		return (smtutil::Expression::ite(
-			_left >= 0,
-			smtutil::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
-			smtutil::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
-		));
+		return signedDivision(_left, _right);
 	else
 		return _left / _right;
 }
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 79380a703..32469e566 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -524,6 +524,10 @@ bool CompilerStack::compile()
 					{
 						if (m_generateEvmBytecode)
 							compileContract(*contract, otherCompilers);
+						if (m_generateIR || m_generateEwasm)
+							generateIR(*contract);
+						if (m_generateEwasm)
+							generateEwasm(*contract);
 					}
 					catch (Error const& _error)
 					{
@@ -532,10 +536,28 @@ bool CompilerStack::compile()
 						m_errorReporter.error(_error.errorId(), _error.type(), SourceLocation(), _error.what());
 						return false;
 					}
-					if (m_generateIR || m_generateEwasm)
-						generateIR(*contract);
-					if (m_generateEwasm)
-						generateEwasm(*contract);
+					catch (UnimplementedFeatureError const& _unimplementedError)
+					{
+						if (
+							SourceLocation const* sourceLocation =
+							boost::get_error_info<langutil::errinfo_sourceLocation>(_unimplementedError)
+						)
+						{
+							string const* comment = _unimplementedError.comment();
+							m_errorReporter.error(
+								1834_error,
+								Error::Type::CodeGenerationError,
+								*sourceLocation,
+								"Unimplemented feature error" +
+								((comment && !comment->empty()) ? ": " + *comment : string{}) +
+								" in " +
+								_unimplementedError.lineInfo()
+							);
+							return false;
+						}
+						else
+							throw;
+					}
 				}
 	m_stackState = CompilationSuccessful;
 	this->link();
diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt
index bb385c755..bbc52d8f2 100644
--- a/libyul/CMakeLists.txt
+++ b/libyul/CMakeLists.txt
@@ -132,6 +132,8 @@ add_library(yul
 	optimiser/OptimiserStep.h
 	optimiser/OptimizerUtilities.cpp
 	optimiser/OptimizerUtilities.h
+	optimiser/ReasoningBasedSimplifier.cpp
+	optimiser/ReasoningBasedSimplifier.h
 	optimiser/RedundantAssignEliminator.cpp
 	optimiser/RedundantAssignEliminator.h
 	optimiser/Rematerialiser.cpp
@@ -168,4 +170,5 @@ add_library(yul
 	optimiser/VarNameCleaner.cpp
 	optimiser/VarNameCleaner.h
 )
-target_link_libraries(yul PUBLIC evmasm solutil langutil)
+
+target_link_libraries(yul PUBLIC evmasm solutil langutil smtutil)
\ No newline at end of file
diff --git a/libyul/Dialect.cpp b/libyul/Dialect.cpp
index 1003c8e44..6c498ce4c 100644
--- a/libyul/Dialect.cpp
+++ b/libyul/Dialect.cpp
@@ -33,6 +33,15 @@ Literal Dialect::zeroLiteralForType(solidity::yul::YulString _type) const
 	return {SourceLocation{}, LiteralKind::Number, "0"_yulstring, _type};
 }
 
+
+Literal Dialect::trueLiteral() const
+{
+	if (boolType != defaultType)
+		return {SourceLocation{}, LiteralKind::Boolean, "true"_yulstring, boolType};
+	else
+		return {SourceLocation{}, LiteralKind::Number, "1"_yulstring, defaultType};
+}
+
 bool Dialect::validTypeForLiteral(LiteralKind _kind, YulString, YulString _type) const
 {
 	if (_kind == LiteralKind::Boolean)
diff --git a/libyul/Dialect.h b/libyul/Dialect.h
index 6634d6cfd..d47c09659 100644
--- a/libyul/Dialect.h
+++ b/libyul/Dialect.h
@@ -77,6 +77,7 @@ struct Dialect: boost::noncopyable
 	virtual bool validTypeForLiteral(LiteralKind _kind, YulString _value, YulString _type) const;
 
 	virtual Literal zeroLiteralForType(YulString _type) const;
+	virtual Literal trueLiteral() const;
 
 	virtual std::set<YulString> fixedFunctionNames() const { return {}; }
 
diff --git a/libyul/optimiser/OptimiserStep.h b/libyul/optimiser/OptimiserStep.h
index 3da161957..70ed098a8 100644
--- a/libyul/optimiser/OptimiserStep.h
+++ b/libyul/optimiser/OptimiserStep.h
@@ -20,6 +20,7 @@
 
 #include <libyul/Exceptions.h>
 
+#include <optional>
 #include <string>
 #include <set>
 
@@ -49,17 +50,41 @@ struct OptimiserStep
 	virtual ~OptimiserStep() = default;
 
 	virtual void run(OptimiserStepContext&, Block&) const = 0;
+	/// @returns non-nullopt if the step cannot be run, for example because it requires
+	/// an SMT solver to be loaded, but none is available. In that case, the string
+	/// contains a human-readable reason.
+	virtual std::optional<std::string> invalidInCurrentEnvironment() const = 0;
 	std::string name;
 };
 
 template <class Step>
 struct OptimiserStepInstance: public OptimiserStep
 {
+private:
+	template<typename T>
+	struct HasInvalidInCurrentEnvironmentMethod
+	{
+	private:
+		template<typename U> static auto test(int) -> decltype(U::invalidInCurrentEnvironment(), std::true_type());
+		template<typename> static std::false_type test(...);
+
+	public:
+		static constexpr bool value = decltype(test<T>(0))::value;
+	};
+
+public:
 	OptimiserStepInstance(): OptimiserStep{Step::name} {}
 	void run(OptimiserStepContext& _context, Block& _ast) const override
 	{
 		Step::run(_context, _ast);
 	}
+	std::optional<std::string> invalidInCurrentEnvironment() const override
+	{
+		if constexpr (HasInvalidInCurrentEnvironmentMethod<Step>::value)
+			return Step::invalidInCurrentEnvironment();
+		else
+			return std::nullopt;
+	};
 };
 
 
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
new file mode 100644
index 000000000..90c3916c2
--- /dev/null
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -0,0 +1,339 @@
+/*
+	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 <libyul/optimiser/ReasoningBasedSimplifier.h>
+
+#include <libyul/optimiser/SSAValueTracker.h>
+#include <libyul/optimiser/Semantics.h>
+#include <libyul/AsmData.h>
+#include <libyul/Utilities.h>
+#include <libyul/Dialect.h>
+
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/Helpers.h>
+
+#include <libsolutil/Visitor.h>
+#include <libsolutil/CommonData.h>
+
+#include <utility>
+#include <memory>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::yul;
+using namespace solidity::smtutil;
+
+void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
+{
+	set<YulString> ssaVars = SSAValueTracker::ssaVariables(_ast);
+	ReasoningBasedSimplifier{_context.dialect, ssaVars}(_ast);
+}
+
+std::optional<string> ReasoningBasedSimplifier::invalidInCurrentEnvironment()
+{
+	// SMTLib2 interface is always available, but we would like to have synchronous answers.
+	if (smtutil::SMTPortfolio{}.solvers() <= 1)
+		return string{"No SMT solvers available."};
+	else
+		return nullopt;
+}
+
+void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl)
+{
+	if (_varDecl.variables.size() != 1 || !_varDecl.value)
+		return;
+	YulString varName = _varDecl.variables.front().name;
+	if (!m_ssaVariables.count(varName))
+		return;
+	bool const inserted = m_variables.insert({varName, m_solver->newVariable("yul_" + varName.str(), defaultSort())}).second;
+	yulAssert(inserted, "");
+	m_solver->addAssertion(m_variables.at(varName) == encodeExpression(*_varDecl.value));
+}
+
+void ReasoningBasedSimplifier::operator()(If& _if)
+{
+	if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
+		return;
+
+	smtutil::Expression condition = encodeExpression(*_if.condition);
+	m_solver->push();
+	m_solver->addAssertion(condition == constantValue(0));
+	CheckResult result = m_solver->check({}).first;
+	m_solver->pop();
+	if (result == CheckResult::UNSATISFIABLE)
+	{
+		Literal trueCondition = m_dialect.trueLiteral();
+		trueCondition.location = locationOf(*_if.condition);
+		_if.condition = make_unique<yul::Expression>(move(trueCondition));
+	}
+	else
+	{
+		m_solver->push();
+		m_solver->addAssertion(condition != constantValue(0));
+		CheckResult result2 = m_solver->check({}).first;
+		m_solver->pop();
+		if (result2 == CheckResult::UNSATISFIABLE)
+		{
+			Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
+			falseCondition.location = locationOf(*_if.condition);
+			_if.condition = make_unique<yul::Expression>(move(falseCondition));
+			_if.body = yul::Block{};
+			// Nothing left to be done.
+			return;
+		}
+	}
+
+	m_solver->push();
+	m_solver->addAssertion(condition != constantValue(0));
+
+	ASTModifier::operator()(_if.body);
+
+	m_solver->pop();
+}
+
+ReasoningBasedSimplifier::ReasoningBasedSimplifier(
+	Dialect const& _dialect,
+	set<YulString> const& _ssaVariables
+):
+	m_dialect(_dialect),
+	m_ssaVariables(_ssaVariables),
+	m_solver(make_unique<smtutil::SMTPortfolio>())
+{
+}
+
+smtutil::Expression ReasoningBasedSimplifier::encodeExpression(yul::Expression const& _expression)
+{
+	return std::visit(GenericVisitor{
+		[&](FunctionCall const& _functionCall)
+		{
+			if (auto const* dialect = dynamic_cast<EVMDialect const*>(&m_dialect))
+				if (auto const* builtin = dialect->builtin(_functionCall.functionName.name))
+					if (builtin->instruction)
+						return encodeEVMBuiltin(*builtin->instruction, _functionCall.arguments);
+			return newRestrictedVariable();
+		},
+		[&](Identifier const& _identifier)
+		{
+			if (
+				m_ssaVariables.count(_identifier.name) &&
+				m_variables.count(_identifier.name)
+			)
+				return m_variables.at(_identifier.name);
+			else
+				return newRestrictedVariable();
+		},
+		[&](Literal const& _literal)
+		{
+			return literalValue(_literal);
+		}
+	}, _expression);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
+	evmasm::Instruction _instruction,
+	vector<yul::Expression> const& _arguments
+)
+{
+	vector<smtutil::Expression> arguments = applyMap(
+		_arguments,
+		[this](yul::Expression const& _expr) { return encodeExpression(_expr); }
+	);
+	switch (_instruction)
+	{
+	case evmasm::Instruction::ADD:
+		return wrap(arguments.at(0) + arguments.at(1));
+	case evmasm::Instruction::MUL:
+		return wrap(arguments.at(0) * arguments.at(1));
+	case evmasm::Instruction::SUB:
+		return wrap(arguments.at(0) - arguments.at(1));
+	case evmasm::Instruction::DIV:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			arguments.at(0) / arguments.at(1)
+		);
+	case evmasm::Instruction::SDIV:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			// No `wrap()` needed here, because -2**255 / -1 results
+			// in 2**255 which is "converted" to its two's complement
+			// representation 2**255 in `signedToUnsigned`
+			signedToUnsigned(smtutil::signedDivision(
+				unsignedToSigned(arguments.at(0)),
+				unsignedToSigned(arguments.at(1))
+			))
+		);
+		break;
+	case evmasm::Instruction::MOD:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			arguments.at(0) % arguments.at(1)
+		);
+	case evmasm::Instruction::SMOD:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			signedToUnsigned(signedModulo(
+				unsignedToSigned(arguments.at(0)),
+				unsignedToSigned(arguments.at(1))
+			))
+		);
+		break;
+	case evmasm::Instruction::LT:
+		return booleanValue(arguments.at(0) < arguments.at(1));
+	case evmasm::Instruction::SLT:
+		return booleanValue(unsignedToSigned(arguments.at(0)) < unsignedToSigned(arguments.at(1)));
+	case evmasm::Instruction::GT:
+		return booleanValue(arguments.at(0) > arguments.at(1));
+	case evmasm::Instruction::SGT:
+		return booleanValue(unsignedToSigned(arguments.at(0)) > unsignedToSigned(arguments.at(1)));
+	case evmasm::Instruction::EQ:
+		return booleanValue(arguments.at(0) == arguments.at(1));
+	case evmasm::Instruction::ISZERO:
+		return booleanValue(arguments.at(0) == constantValue(0));
+	case evmasm::Instruction::AND:
+		return smtutil::Expression::ite(
+			(arguments.at(0) == 0 || arguments.at(0) == 1) &&
+			(arguments.at(1) == 0 || arguments.at(1) == 1),
+			booleanValue(arguments.at(0) == 1 && arguments.at(1) == 1),
+			bv2int(int2bv(arguments.at(0)) & int2bv(arguments.at(1)))
+		);
+	case evmasm::Instruction::OR:
+		return smtutil::Expression::ite(
+			(arguments.at(0) == 0 || arguments.at(0) == 1) &&
+			(arguments.at(1) == 0 || arguments.at(1) == 1),
+			booleanValue(arguments.at(0) == 1 || arguments.at(1) == 1),
+			bv2int(int2bv(arguments.at(0)) | int2bv(arguments.at(1)))
+		);
+	case evmasm::Instruction::XOR:
+		return bv2int(int2bv(arguments.at(0)) ^ int2bv(arguments.at(1)));
+	case evmasm::Instruction::NOT:
+		return smtutil::Expression(u256(-1)) - arguments.at(0);
+	case evmasm::Instruction::SHL:
+		return smtutil::Expression::ite(
+			arguments.at(0) > 255,
+			constantValue(0),
+			bv2int(int2bv(arguments.at(1)) << int2bv(arguments.at(0)))
+		);
+	case evmasm::Instruction::SHR:
+		return smtutil::Expression::ite(
+			arguments.at(0) > 255,
+			constantValue(0),
+			bv2int(int2bv(arguments.at(1)) >> int2bv(arguments.at(0)))
+		);
+	case evmasm::Instruction::SAR:
+		return smtutil::Expression::ite(
+			arguments.at(0) > 255,
+			constantValue(0),
+			bv2int(smtutil::Expression::ashr(int2bv(arguments.at(1)), int2bv(arguments.at(0))))
+		);
+	case evmasm::Instruction::ADDMOD:
+		return smtutil::Expression::ite(
+			arguments.at(2) == constantValue(0),
+			constantValue(0),
+			(arguments.at(0) + arguments.at(1)) % arguments.at(2)
+		);
+	case evmasm::Instruction::MULMOD:
+		return smtutil::Expression::ite(
+			arguments.at(2) == constantValue(0),
+			constantValue(0),
+			(arguments.at(0) * arguments.at(1)) % arguments.at(2)
+		);
+	// TODO SIGNEXTEND
+	default:
+		break;
+	}
+	return newRestrictedVariable();
+}
+
+smtutil::Expression ReasoningBasedSimplifier::int2bv(smtutil::Expression _arg) const
+{
+	return smtutil::Expression::int2bv(std::move(_arg), 256);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::bv2int(smtutil::Expression _arg) const
+{
+	return smtutil::Expression::bv2int(std::move(_arg));
+}
+
+smtutil::Expression ReasoningBasedSimplifier::newVariable()
+{
+	return m_solver->newVariable(uniqueName(), defaultSort());
+}
+
+smtutil::Expression ReasoningBasedSimplifier::newRestrictedVariable()
+{
+	smtutil::Expression var = newVariable();
+	m_solver->addAssertion(0 <= var && var < smtutil::Expression(bigint(1) << 256));
+	return var;
+}
+
+string ReasoningBasedSimplifier::uniqueName()
+{
+	return "expr_" + to_string(m_varCounter++);
+}
+
+shared_ptr<Sort> ReasoningBasedSimplifier::defaultSort() const
+{
+	return SortProvider::intSort();
+}
+
+smtutil::Expression ReasoningBasedSimplifier::booleanValue(smtutil::Expression _value) const
+{
+	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
+}
+
+smtutil::Expression ReasoningBasedSimplifier::constantValue(size_t _value) const
+{
+	return _value;
+}
+
+smtutil::Expression ReasoningBasedSimplifier::literalValue(Literal const& _literal) const
+{
+	return smtutil::Expression(valueOfLiteral(_literal));
+}
+
+smtutil::Expression ReasoningBasedSimplifier::unsignedToSigned(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(
+		_value < smtutil::Expression(bigint(1) << 255),
+		_value,
+		_value - smtutil::Expression(bigint(1) << 256)
+	);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::signedToUnsigned(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(
+		_value >= 0,
+		_value,
+		_value + smtutil::Expression(bigint(1) << 256)
+	);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::wrap(smtutil::Expression _value)
+{
+	smtutil::Expression rest = newRestrictedVariable();
+	smtutil::Expression multiplier = newVariable();
+	m_solver->addAssertion(_value == multiplier * smtutil::Expression(bigint(1) << 256) + rest);
+	return rest;
+}
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h
new file mode 100644
index 000000000..18fcf3583
--- /dev/null
+++ b/libyul/optimiser/ReasoningBasedSimplifier.h
@@ -0,0 +1,98 @@
+/*
+	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 <libyul/optimiser/ASTWalker.h>
+#include <libyul/optimiser/OptimiserStep.h>
+#include <libyul/Dialect.h>
+
+// because of instruction
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <map>
+
+namespace solidity::smtutil
+{
+class SolverInterface;
+class Expression;
+struct Sort;
+}
+
+namespace solidity::yul
+{
+
+/**
+ * Reasoning-based simplifier.
+ * This optimizer uses SMT solvers to check whether `if` conditions are constant.
+ * - If `constraints AND condition` is UNSAT, the condition is never true and the whole body can be removed.
+ * - If `constraints AND NOT condition` is UNSAT, the condition is always true and can be replaced by `1`.
+ * The simplifications above can only be applied if the condition is movable.
+ *
+ * It is only effective on the EVM dialect, but safe to use on other dialects.
+ *
+ * Prerequisite: Disambiguator, SSATransform.
+ */
+class ReasoningBasedSimplifier: public ASTModifier
+{
+public:
+	static constexpr char const* name{"ReasoningBasedSimplifier"};
+	static void run(OptimiserStepContext& _context, Block& _ast);
+	static std::optional<std::string> invalidInCurrentEnvironment();
+
+	using ASTModifier::operator();
+	void operator()(VariableDeclaration& _varDecl) override;
+	void operator()(If& _if) override;
+
+private:
+	explicit ReasoningBasedSimplifier(
+		Dialect const& _dialect,
+		std::set<YulString> const& _ssaVariables
+	);
+
+	smtutil::Expression encodeExpression(
+		Expression const& _expression
+	);
+
+	virtual smtutil::Expression encodeEVMBuiltin(
+		evmasm::Instruction _instruction,
+		std::vector<Expression> const& _arguments
+	);
+
+	smtutil::Expression int2bv(smtutil::Expression _arg) const;
+	smtutil::Expression bv2int(smtutil::Expression _arg) const;
+
+	smtutil::Expression newVariable();
+	virtual smtutil::Expression newRestrictedVariable();
+	std::string uniqueName();
+
+	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
+	virtual smtutil::Expression booleanValue(smtutil::Expression _value) const;
+	virtual smtutil::Expression constantValue(size_t _value) const;
+	virtual smtutil::Expression literalValue(Literal const& _literal) const;
+	virtual smtutil::Expression unsignedToSigned(smtutil::Expression _value);
+	virtual smtutil::Expression signedToUnsigned(smtutil::Expression _value);
+	virtual smtutil::Expression wrap(smtutil::Expression _value);
+
+	Dialect const& m_dialect;
+	std::set<YulString> const& m_ssaVariables;
+	std::unique_ptr<smtutil::SolverInterface> m_solver;
+	std::map<YulString, smtutil::Expression> m_variables;
+
+	size_t m_varCounter = 0;
+};
+
+}
diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp
index 1625e60c5..98683b453 100644
--- a/libyul/optimiser/Suite.cpp
+++ b/libyul/optimiser/Suite.cpp
@@ -41,6 +41,7 @@
 #include <libyul/optimiser/ForLoopConditionOutOfBody.h>
 #include <libyul/optimiser/ForLoopInitRewriter.h>
 #include <libyul/optimiser/ForLoopConditionIntoBody.h>
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/UnusedFunctionParameterPruner.h>
 #include <libyul/optimiser/UnusedPruner.h>
@@ -184,6 +185,7 @@ map<string, unique_ptr<OptimiserStep>> const& OptimiserSuite::allSteps()
 			LoopInvariantCodeMotion,
 			NameSimplifier,
 			RedundantAssignEliminator,
+			ReasoningBasedSimplifier,
 			Rematerialiser,
 			SSAReverser,
 			SSATransform,
@@ -221,6 +223,7 @@ map<string, char> const& OptimiserSuite::stepNameToAbbreviationMap()
 		{LoadResolver::name,                  'L'},
 		{LoopInvariantCodeMotion::name,       'M'},
 		{NameSimplifier::name,                'N'},
+		{ReasoningBasedSimplifier::name,      'R'},
 		{RedundantAssignEliminator::name,     'r'},
 		{Rematerialiser::name,                'm'},
 		{SSAReverser::name,                   'V'},
@@ -266,6 +269,7 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations)
 			insideLoop = false;
 			break;
 		default:
+		{
 			yulAssert(
 				string(NonStepAbbreviations).find(abbreviation) == string::npos,
 				"Unhandled syntactic element in the abbreviation sequence"
@@ -275,6 +279,14 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations)
 				OptimizerException,
 				"'"s + abbreviation + "' is not a valid step abbreviation"
 			);
+			optional<string> invalid = allSteps().at(stepAbbreviationToNameMap().at(abbreviation))->invalidInCurrentEnvironment();
+			assertThrow(
+				!invalid.has_value(),
+				OptimizerException,
+				"'"s + abbreviation + "' is invalid in the current environment: " + *invalid
+			);
+
+		}
 		}
 	assertThrow(!insideLoop, OptimizerException, "Unbalanced brackets");
 }
diff --git a/scripts/error_codes.py b/scripts/error_codes.py
index 69e452b2a..d77fcacaa 100755
--- a/scripts/error_codes.py
+++ b/scripts/error_codes.py
@@ -188,6 +188,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
     # Warning (1878): SPDX license identifier not provided in source file. ....
     # Warning (3420): Source file does not specify required compiler version!
     test_ids |= find_ids_in_cmdline_test_err(path.join(top_dir, "test", "cmdlineTests", "error_codes", "err"))
+    test_ids |= find_ids_in_cmdline_test_err(path.join(top_dir, "test", "cmdlineTests", "yul_unimplemented", "err"))
 
     # white list of ids which are not covered by tests
     white_ids = {
diff --git a/test/cmdlineTests.sh b/test/cmdlineTests.sh
index a22fb7339..abb7ab5ba 100755
--- a/test/cmdlineTests.sh
+++ b/test/cmdlineTests.sh
@@ -124,6 +124,7 @@ function test_solc_behaviour()
         sed -i.bak -e '/^Warning (3805): This is a pre-release compiler version, please do not use it in production./d' "$stderr_path"
         sed -i.bak -e 's/\(^[ ]*auxdata: \)0x[0-9a-f]*$/\1AUXDATA REMOVED/' "$stdout_path"
         sed -i.bak -e 's/ Consider adding "pragma .*$//' "$stderr_path"
+        sed -i.bak -e 's/\(Unimplemented feature error: .* in \).*$/\1FILENAME REMOVED/' "$stderr_path"
         sed -i.bak -e 's/"version": "[^"]*"/"version": "VERSION REMOVED"/' "$stdout_path"
         # Remove trailing empty lines. Needs a line break to make OSX sed happy.
         sed -i.bak -e '1{/^$/d
diff --git a/test/cmdlineTests/yul_unimplemented/args b/test/cmdlineTests/yul_unimplemented/args
new file mode 100644
index 000000000..e869749f2
--- /dev/null
+++ b/test/cmdlineTests/yul_unimplemented/args
@@ -0,0 +1 @@
+--ir --error-codes
diff --git a/test/cmdlineTests/yul_unimplemented/err b/test/cmdlineTests/yul_unimplemented/err
new file mode 100644
index 000000000..d6159a1f1
--- /dev/null
+++ b/test/cmdlineTests/yul_unimplemented/err
@@ -0,0 +1,5 @@
+Error (1834): Unimplemented feature error: setToZero for type t_struct$_S_$4_storage not yet implemented! in FILENAME REMOVED
+ --> yul_unimplemented/input.sol:9:9:
+  |
+9 |         delete str;
+  |         ^^^^^^^^^^
diff --git a/test/cmdlineTests/yul_unimplemented/exit b/test/cmdlineTests/yul_unimplemented/exit
new file mode 100644
index 000000000..d00491fd7
--- /dev/null
+++ b/test/cmdlineTests/yul_unimplemented/exit
@@ -0,0 +1 @@
+1
diff --git a/test/cmdlineTests/yul_unimplemented/input.sol b/test/cmdlineTests/yul_unimplemented/input.sol
new file mode 100644
index 000000000..d024eeba0
--- /dev/null
+++ b/test/cmdlineTests/yul_unimplemented/input.sol
@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract test {
+    struct S {
+        uint x;
+    }
+    S str;
+    constructor() {
+        delete str;
+    }
+}
\ No newline at end of file
diff --git a/test/libsolidity/SolidityExecutionFramework.cpp b/test/libsolidity/SolidityExecutionFramework.cpp
index 84333269e..4a0745431 100644
--- a/test/libsolidity/SolidityExecutionFramework.cpp
+++ b/test/libsolidity/SolidityExecutionFramework.cpp
@@ -54,6 +54,12 @@ bytes SolidityExecutionFramework::multiSourceCompileContract(
 	m_compiler.setRevertStringBehaviour(m_revertStrings);
 	if (!m_compiler.compile())
 	{
+		// The testing framework expects an exception for
+		// "unimplemented" yul IR generation.
+		if (m_compileViaYul)
+			for (auto const& error: m_compiler.errors())
+				if (error->type() == langutil::Error::Type::CodeGenerationError)
+					BOOST_THROW_EXCEPTION(*error);
 		langutil::SourceReferenceFormatter formatter(std::cerr);
 
 		for (auto const& error: m_compiler.errors())
diff --git a/test/libsolidity/semanticTests/arithmetics/signed_mod.sol b/test/libsolidity/semanticTests/arithmetics/signed_mod.sol
new file mode 100644
index 000000000..a992bd0be
--- /dev/null
+++ b/test/libsolidity/semanticTests/arithmetics/signed_mod.sol
@@ -0,0 +1,14 @@
+contract C {
+    function f(int a, int b) public pure returns (int) {
+        return a % b;
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// f(int256,int256): 7, 5 -> 2
+// f(int256,int256): 7, -5 -> 2
+// f(int256,int256): -7, 5 -> -2
+// f(int256,int256): -7, 5 -> -2
+// f(int256,int256): -5, -5 -> 0
diff --git a/test/libsolidity/semanticTests/various/skip_dynamic_types_for_static_arrays_with_dynamic_elements.sol b/test/libsolidity/semanticTests/various/skip_dynamic_types_for_static_arrays_with_dynamic_elements.sol
new file mode 100644
index 000000000..86509cfe4
--- /dev/null
+++ b/test/libsolidity/semanticTests/various/skip_dynamic_types_for_static_arrays_with_dynamic_elements.sol
@@ -0,0 +1,23 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        bool[] b;
+    }
+
+    function f() public returns (uint256, bool[][2] memory, S[2] memory, uint256) {
+        return (
+            5,
+            [new bool[](1), new bool[](2)],
+            [S(new bool[](2)), S(new bool[](5))],
+            6
+        );
+    }
+
+    function g() public returns (uint256, uint256) {
+        (uint256 a, , , uint256 b) = this.f();
+        return (a, b);
+    }
+}
+// ----
+// g() -> 5, 6
diff --git a/test/libsolidity/smtCheckerTests/special/event.sol b/test/libsolidity/smtCheckerTests/special/event.sol
new file mode 100644
index 000000000..c3e45c30e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/event.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+	event Nudge();
+	event SomeArgs(uint, uint);
+	event Caller(address, uint);
+	function f() payable external {
+		emit Nudge();
+		emit SomeArgs(134, 567);
+		emit Caller(msg.sender, msg.value);
+	}
+	function g_data() pure internal returns (uint) {
+		assert(true);
+	}
+	function g() external {
+		emit SomeArgs(g_data(), g_data());
+	}
+	bool x = true;
+	function h_data() view internal returns (uint) {
+		assert(x);
+	}
+	function h() external {
+		x = false;
+		emit SomeArgs(h_data(), h_data());
+	}
+}
+// ----
+// Warning 6328: (440-449): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/special/log.sol b/test/libsolidity/smtCheckerTests/special/log.sol
new file mode 100644
index 000000000..a9d6fcc08
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/log.sol
@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() external {
+		bytes32 t1 = bytes32(uint256(0x1234));
+		log0(t1);
+		log1(t1, t1);
+		log2(t1, t1, t1);
+		log3(t1, t1, t1, t1);
+		log4(t1, t1, t1, t1, t1);
+	}
+	function g_data() pure internal returns (bytes32) {
+		assert(true);
+		return bytes32(uint256(0x5678));
+	}
+	function g() external {
+		// To test that the function call is actually visited.
+		log0(g_data());
+		log1(g_data(), g_data());
+		log2(g_data(), g_data(), g_data());
+		log3(g_data(), g_data(), g_data(), g_data());
+		log4(g_data(), g_data(), g_data(), g_data(), g_data());
+	}
+	bool x = true;
+	function h_data() view internal returns (bytes32) {
+		assert(x);
+	}
+	function h() external {
+		// To test that the function call is actually visited.
+		x = false;
+		log0(h_data());
+		log1(h_data(), h_data());
+		log2(h_data(), h_data(), h_data());
+		log3(h_data(), h_data(), h_data(), h_data());
+		log4(h_data(), h_data(), h_data(), h_data(), h_data());
+	}
+}
+// ----
+// Warning 6328: (668-677): Assertion violation happens here.
diff --git a/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_array_of_string_literals_to_calldata_string.sol b/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_array_of_string_literals_to_calldata_string.sol
new file mode 100644
index 000000000..328a86f79
--- /dev/null
+++ b/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_array_of_string_literals_to_calldata_string.sol
@@ -0,0 +1,9 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    function f() public pure returns(string[5] calldata) {
+        return ["h", "e", "l", "l", "o"];
+    }
+}
+// ----
+// TypeError 6359: (122-147): Return argument type string memory[5] memory is not implicitly convertible to expected type (type of first return variable) string calldata[5] calldata.
diff --git a/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_string_literal_to_calldata_string.sol b/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_string_literal_to_calldata_string.sol
new file mode 100644
index 000000000..166ebffb0
--- /dev/null
+++ b/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_string_literal_to_calldata_string.sol
@@ -0,0 +1,17 @@
+contract C {
+    function f1() public pure returns(string calldata) {
+        return "hello";
+    }
+
+    function f2() public pure returns(string calldata) {
+        return unicode"hello";
+    }
+
+    function f3() public pure returns(bytes calldata) {
+        return hex"68656c6c6f";
+    }
+}
+// ----
+// TypeError 6359: (85-92): Return argument type literal_string "hello" is not implicitly convertible to expected type (type of first return variable) string calldata.
+// TypeError 6359: (173-187): Return argument type literal_string "hello" is not implicitly convertible to expected type (type of first return variable) string calldata.
+// TypeError 6359: (267-282): Return argument type literal_string "hello" is not implicitly convertible to expected type (type of first return variable) bytes calldata.
diff --git a/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_string_literal_to_calldata_string_in_function_parameter.sol b/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_string_literal_to_calldata_string_in_function_parameter.sol
new file mode 100644
index 000000000..bf58cba42
--- /dev/null
+++ b/test/libsolidity/syntaxTests/conversion/implicit_conversion_from_string_literal_to_calldata_string_in_function_parameter.sol
@@ -0,0 +1,14 @@
+contract C {
+    function g(string calldata _s) public {}
+    function h(bytes calldata _b) public {}
+
+    function f() public {
+        g("hello");
+        g(unicode"hello");
+        h(hex"68656c6c6f");
+    }
+}
+// ----
+// TypeError 9553: (139-146): Invalid type for argument in function call. Invalid implicit conversion from literal_string "hello" to string calldata requested.
+// TypeError 9553: (159-173): Invalid type for argument in function call. Invalid implicit conversion from literal_string "hello" to string calldata requested.
+// TypeError 9553: (186-201): Invalid type for argument in function call. Invalid implicit conversion from literal_string "hello" to bytes calldata requested.
diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp
index 18576384d..cdcfd4fc2 100644
--- a/test/libyul/YulOptimizerTest.cpp
+++ b/test/libyul/YulOptimizerTest.cpp
@@ -53,6 +53,7 @@
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionJoiner.h>
 #include <libyul/optimiser/OptimiserStep.h>
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/SSAReverser.h>
 #include <libyul/optimiser/SSATransform.h>
 #include <libyul/optimiser/Semantics.h>
@@ -102,6 +103,9 @@ YulOptimizerTest::YulOptimizerTest(string const& _filename):
 		BOOST_THROW_EXCEPTION(runtime_error("Filename path has to contain a directory: \"" + _filename + "\"."));
 	m_optimizerStep = std::prev(std::prev(path.end()))->string();
 
+	if (m_optimizerStep == "reasoningBasedSimplifier" && solidity::test::CommonOptions::get().disableSMT)
+		m_shouldRun = false;
+
 	m_source = m_reader.source();
 
 	auto dialectName = m_reader.stringSetting("dialect", "evm");
@@ -320,6 +324,11 @@ TestCase::TestResult YulOptimizerTest::run(ostream& _stream, string const& _line
 		LiteralRematerialiser::run(*m_context, *m_object->code);
 		StructuralSimplifier::run(*m_context, *m_object->code);
 	}
+	else if (m_optimizerStep == "reasoningBasedSimplifier")
+	{
+		disambiguate();
+		ReasoningBasedSimplifier::run(*m_context, *m_object->code);
+	}
 	else if (m_optimizerStep == "equivalentFunctionCombiner")
 	{
 		disambiguate();
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul
new file mode 100644
index 000000000..88c60a0ee
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul
@@ -0,0 +1,31 @@
+{
+    let x := calldataload(0)
+    let y := calldataload(32)
+    let z := calldataload(64)
+    let result := addmod(x, y, z)
+
+    // should be zero
+    if gt(result, z) { sstore(0, 1) }
+
+    // addmod is equal to mod of sum for small numbers
+    if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) {
+        if eq(result, mod(add(x, y), z)) { sstore(0, 9) }
+    }
+
+    // but not in general
+    if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) {
+        if eq(result, mod(add(x, y), z)) { sstore(0, 5) }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(32)
+//     let z := calldataload(64)
+//     let result := addmod(x, y, z)
+//     if 0 { }
+//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } }
+//     if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) { if 0 { } }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul
new file mode 100644
index 000000000..7ff930766
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul
@@ -0,0 +1,13 @@
+{
+    let x := 7
+    let y := 8
+    if eq(add(x, y), 15) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := 7
+//     let y := 8
+//     if 1 { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul
new file mode 100644
index 000000000..2080a678c
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul
@@ -0,0 +1,19 @@
+{
+	function f() -> z
+	{
+		z := 15
+	}
+	let x := 7
+	let y := 8
+	if eq(add(x, y), f()) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     function f() -> z
+//     { z := 15 }
+//     let x := 7
+//     let y := 8
+//     if eq(add(x, y), f()) { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul
new file mode 100644
index 000000000..ed50224d0
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul
@@ -0,0 +1,23 @@
+{
+	function f() -> z
+	{
+		sstore(1, 15)
+		z := 15
+	}
+	let x := 7
+	let y := 8
+	if eq(add(x, y), f()) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     function f() -> z
+//     {
+//         sstore(1, 15)
+//         z := 15
+//     }
+//     let x := 7
+//     let y := 8
+//     if eq(add(x, y), f()) { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul
new file mode 100644
index 000000000..31a342339
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul
@@ -0,0 +1,32 @@
+{
+    let vloc_x := calldataload(0)
+    let vloc_y := calldataload(1)
+    if lt(vloc_x, shl(100, 1)) {
+        if lt(vloc_y, shl(100, 1)) {
+            if iszero(and(iszero(iszero(vloc_x)), gt(vloc_y, div(not(0), vloc_x)))) {
+                let vloc := mul(vloc_x, vloc_y)
+                sstore(0, vloc)
+            }
+        }
+    }
+}
+// ====
+// EVMVersion: >=constantinople
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let vloc_x := calldataload(0)
+//     let vloc_y := calldataload(1)
+//     if lt(vloc_x, shl(100, 1))
+//     {
+//         if lt(vloc_y, shl(100, 1))
+//         {
+//             if 1
+//             {
+//                 let vloc := mul(vloc_x, vloc_y)
+//                 sstore(0, vloc)
+//             }
+//         }
+//     }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul
new file mode 100644
index 000000000..f5226acf7
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul
@@ -0,0 +1,31 @@
+{
+    let x := calldataload(0)
+    let y := calldataload(32)
+    let z := calldataload(64)
+    let result := mulmod(x, y, z)
+
+    // should be zero
+    if gt(result, z) { sstore(0, 1) }
+
+    // mulmod is equal to mod of product for small numbers
+    if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) {
+        if eq(result, mod(mul(x, y), z)) { sstore(0, 9) }
+    }
+
+    // but not in general
+    if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) {
+        if eq(result, mod(mul(x, y), z)) { sstore(0, 5) }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(32)
+//     let z := calldataload(64)
+//     let result := mulmod(x, y, z)
+//     if 0 { }
+//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } }
+//     if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { if 0 { } }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul
new file mode 100644
index 000000000..6e4b3f5ed
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul
@@ -0,0 +1,16 @@
+{
+    let x := sub(0, 7)
+    let y := 2
+    // (-7)/2 == -3 on the evm
+    if iszero(add(sdiv(x, y), 3)) { }
+    if iszero(add(sdiv(x, y), 4)) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := sub(0, 7)
+//     let y := 2
+//     if 1 { }
+//     if 0 { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul
new file mode 100644
index 000000000..d7002c99b
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul
@@ -0,0 +1,26 @@
+{
+    let x := calldataload(2)
+    let t := lt(x, 20)
+    if t {
+        if lt(x, 21) { }
+        if lt(x, 20) { }
+        if lt(x, 19) { }
+        if gt(x, 20) { }
+        if iszero(gt(x, 20)) { }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(2)
+//     let t := lt(x, 20)
+//     if t
+//     {
+//         if 1 { }
+//         if 1 { }
+//         if lt(x, 19) { }
+//         if 0 { }
+//         if 1 { }
+//     }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul
new file mode 100644
index 000000000..1e409079e
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul
@@ -0,0 +1,31 @@
+{
+    let y := calldataload(0)
+    let t := calldataload(32)
+
+    if sgt(sub(y, 1), y) {
+        // y - 1 > y, i.e. y is the most negative value
+        if eq(sdiv(y, sub(0, 1)), y) {
+            // should be true: y / -1 == y
+            sstore(0, 7)
+        }
+        if iszero(eq(y, t)) {
+            // t is not the most negative value
+            if eq(sdiv(t, sub(0, 1)), sub(0, t)) {
+                // should be true: t / -1 = 0 - t
+                sstore(1, 7)
+            }
+        }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let y := calldataload(0)
+//     let t := calldataload(32)
+//     if sgt(sub(y, 1), y)
+//     {
+//         if 1 { sstore(0, 7) }
+//         if iszero(eq(y, t)) { if 1 { sstore(1, 7) } }
+//     }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul
new file mode 100644
index 000000000..12f04c857
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul
@@ -0,0 +1,53 @@
+{
+    // 7 % 5 == 2
+    // 7 % -5 == 2
+    // -7 % 5 == -2
+    // -7 % -5 == -2
+    // -5 % -5 == 0
+    let x := calldataload(0)
+    let y := calldataload(32)
+    let result := smod(x, y)
+    if eq(x, 7) {
+        if eq(y, 5) {
+            if eq(result, 2) { sstore(0, 7)}
+        }
+        if eq(y, sub(0, 5)) {
+            if eq(result, 2) { sstore(0, 7)}
+        }
+    }
+    if eq(x, sub(0, 7)) {
+        if eq(y, 5) {
+            if eq(result, sub(0, 2)) { sstore(0, 7)}
+        }
+        if eq(y, sub(0, 5)) {
+            if eq(result, sub(0, 2)) { sstore(0, 7)}
+        }
+    }
+    if eq(x, sub(0, 5)) {
+        if eq(y, sub(0, 5)) {
+            if eq(result, 0) { sstore(0, 7)}
+        }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(32)
+//     let result := smod(x, y)
+//     if eq(x, 7)
+//     {
+//         if eq(y, 5) { if 1 { sstore(0, 7) } }
+//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
+//     }
+//     if eq(x, sub(0, 7))
+//     {
+//         if eq(y, 5) { if 1 { sstore(0, 7) } }
+//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
+//     }
+//     if eq(x, sub(0, 5))
+//     {
+//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
+//     }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul
new file mode 100644
index 000000000..6f860dc13
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul
@@ -0,0 +1,5 @@
+{ }
+// ----
+// step: reasoningBasedSimplifier
+//
+// { }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul
new file mode 100644
index 000000000..69f5c6769
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul
@@ -0,0 +1,15 @@
+{
+    let x := 7
+    let y := 8
+    if gt(sub(x, y), 20) { }
+    if eq(sub(x, y), 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) {}
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := 7
+//     let y := 8
+//     if 1 { }
+//     if 1 { }
+// }
diff --git a/test/tools/yulopti.cpp b/test/tools/yulopti.cpp
index e4605d10f..a15c426dc 100644
--- a/test/tools/yulopti.cpp
+++ b/test/tools/yulopti.cpp
@@ -36,6 +36,7 @@
 #include <libyul/optimiser/StackCompressor.h>
 #include <libyul/optimiser/VarNameCleaner.h>
 #include <libyul/optimiser/Suite.h>
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 
 #include <libyul/backends/evm/EVMDialect.h>
 
@@ -157,7 +158,7 @@ public:
 			map<char, string> const& extraOptions = {
 				{'#', "quit"},
 				{',', "VarNameCleaner"},
-				{';', "StackCompressor"},
+				{';', "StackCompressor"}
 			};
 
 			printUsageBanner(abbreviationMap, extraOptions, 4);
diff --git a/test/yulPhaser/Chromosome.cpp b/test/yulPhaser/Chromosome.cpp
index 4d0592e9a..1f66398be 100644
--- a/test/yulPhaser/Chromosome.cpp
+++ b/test/yulPhaser/Chromosome.cpp
@@ -138,7 +138,7 @@ BOOST_AUTO_TEST_CASE(output_operator_should_create_concise_and_unambiguous_strin
 
 	BOOST_TEST(chromosome.length() == allSteps.size());
 	BOOST_TEST(chromosome.optimisationSteps() == allSteps);
-	BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMNrmVatpud");
+	BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMNRrmVatpud");
 }
 
 BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names)