diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt
index a02b3d592..8d71c04a2 100644
--- a/libyul/CMakeLists.txt
+++ b/libyul/CMakeLists.txt
@@ -141,6 +141,8 @@ add_library(yul
 	optimiser/LoopInvariantCodeMotion.h
 	optimiser/MainFunction.cpp
 	optimiser/MainFunction.h
+	optimiser/MemoryLoadResolver.cpp
+	optimiser/MemoryLoadResolver.h
 	optimiser/Metrics.cpp
 	optimiser/Metrics.h
 	optimiser/NameCollector.cpp
diff --git a/libyul/optimiser/MemoryLoadResolver.cpp b/libyul/optimiser/MemoryLoadResolver.cpp
new file mode 100644
index 000000000..d50879503
--- /dev/null
+++ b/libyul/optimiser/MemoryLoadResolver.cpp
@@ -0,0 +1,344 @@
+/*
+	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 "libyul/optimiser/CallGraphGenerator.h"
+#include "libyul/optimiser/OptimiserStep.h"
+#include "libyul/optimiser/SSAValueTracker.h"
+#include <libyul/optimiser/MemoryLoadResolver.h>
+#include <libyul/optimiser/Semantics.h>
+
+#include <libyul/AST.h>
+#include <libyul/SideEffects.h>
+#include <libyul/Utilities.h>
+
+#include <libsolutil/Visitor.h>
+#include <libsolutil/CommonData.h>
+
+#include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/SolverInterface.h>
+#include <libsmtutil/Helpers.h>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::yul;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+void MemoryLoadResolver::run(OptimiserStepContext& _context, Block& _ast)
+{
+	MemoryLoadResolver{
+		_context.dialect,
+		SideEffectsPropagator::sideEffects(_context.dialect, CallGraphGenerator::callGraph(_ast)),
+		SSAValueTracker::ssaVariables(_ast),
+		MSizeFinder::containsMSize(_context.dialect, _ast)
+	}(_ast);
+}
+
+void MemoryLoadResolver::visit(Expression& _e)
+{
+	Scoper::visit(_e);
+
+	// We skip the replacing if there is msize. TODO do we need this, and can we do it earlier?
+	if (m_containsMsize)
+		return;
+
+	// Check and replace the value of mload(x), if possible
+	if (FunctionCall const* functionCall = get_if<FunctionCall>(&_e))
+		if (functionCall->functionName.name == m_dialect.memoryLoadFunction(YulString{})->name)
+
+			if (Identifier const* identifier = get_if<Identifier>(&functionCall->arguments.front()))
+				if (m_memory.count(identifier->name))
+				{
+					auto& value = m_memory.at(identifier->name);
+					if (inScope(value))
+						_e = Identifier{locationOf(_e), value};
+				}
+}
+
+void MemoryLoadResolver::operator()(VariableDeclaration& _v)
+{
+	// Otherwise, we simply assign a free variable to it.
+	Scoper::operator()(_v);
+
+	if (
+		_v.variables.size() == 1 &&
+		_v.value &&
+		m_ssaVariables.count(_v.variables.front().name)
+	)
+	{
+		YulString& variableName = _v.variables.front().name;
+		bool const inserted = m_variables.insert({
+			variableName,
+			m_solver->newVariable("yul_" + variableName.str(), defaultSort())
+			}).second;
+		yulAssert(inserted, "");
+		m_solver->addAssertion(m_variables.at(variableName) == encodeExpression(*_v.value));
+	}
+	else
+	{
+		for(auto const& v: _v.variables)
+		{
+			YulString const& variableName = v.name;
+			bool const inserted = m_variables.insert({
+				variableName,
+				m_solver->newVariable("yul_" + variableName.str(), defaultSort())
+				}).second;
+			yulAssert(inserted, "");
+			// TODO improve this by adding assertions directly, without the restricted variable.
+			m_solver->addAssertion(m_variables.at(variableName) == newRestrictedVariable());
+		}
+	}
+}
+
+void MemoryLoadResolver::operator()(FunctionCall& _f)
+{
+	Scoper::operator()(_f);
+
+	SideEffectsCollector sideEffects{m_dialect, _f, &m_functionSideEffects};
+
+	if (sideEffects.invalidatesMemory())
+	{
+		set<YulString> keysToErase;
+		for ([[maybe_unused]] auto const& [key, value]: m_memory)
+			if (invalidatesMemoryLocation(key, _f))
+				m_memory.erase(key); // TODO iterator invalidation?
+	}
+
+	if (auto memoryMapping = isSimpleMStore(_f))
+		// TODO can the key be already present in the m_memory?
+		m_memory[memoryMapping->first] = memoryMapping->second;
+
+}
+
+std::optional<pair<YulString, YulString>> MemoryLoadResolver::isSimpleMStore(
+	FunctionCall const& _functionCall
+) const
+{
+	if (_functionCall.functionName.name == m_dialect.memoryStoreFunction({})->name)
+		if (Identifier const* key = std::get_if<Identifier>(&_functionCall.arguments.front()))
+			if (Identifier const* value = std::get_if<Identifier>(&_functionCall.arguments.back()))
+				if (m_ssaVariables.count(key->name) && m_ssaVariables.count(value->name))
+					return make_pair(key->name, value->name);
+	return {};
+}
+
+smtutil::Expression MemoryLoadResolver::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 (// TODO do we need to check if it's an SSAVariable?
+				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 MemoryLoadResolver::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)
+	{
+	// TODO during the encoding for Real, change the wrapping.
+	case evmasm::Instruction::ADD:
+		return wrap(arguments.at(0) + arguments.at(1));
+
+	// Restrictions from EIP-1985
+	case evmasm::Instruction::CALLDATASIZE:
+	case evmasm::Instruction::CODESIZE:
+	case evmasm::Instruction::EXTCODESIZE:
+	case evmasm::Instruction::MSIZE:
+	case evmasm::Instruction::RETURNDATASIZE:
+		return newRestrictedVariable(bigint(1) << 32);
+		break;
+	default:
+		break;
+	}
+	return newRestrictedVariable();
+}
+
+smtutil::Expression MemoryLoadResolver::newVariable()
+{
+	return m_solver->newVariable(uniqueName(), defaultSort());
+}
+
+smtutil::Expression MemoryLoadResolver::newRestrictedVariable(bigint _maxValue)
+{
+	smtutil::Expression var = newVariable();
+	m_solver->addAssertion(0 <= var && var < smtutil::Expression(_maxValue));
+	return var;
+}
+
+string MemoryLoadResolver::uniqueName()
+{
+	return "expr_" + to_string(m_varCounter++);
+}
+
+shared_ptr<Sort> MemoryLoadResolver::defaultSort() const
+{
+	// TODO Change into realsort
+	return SortProvider::intSort();
+}
+
+
+smtutil::Expression MemoryLoadResolver::constantValue(size_t _value) const
+{
+	return _value;
+}
+
+smtutil::Expression MemoryLoadResolver::literalValue(Literal const& _literal) const
+{
+	return smtutil::Expression(valueOfLiteral(_literal));
+}
+
+
+smtutil::Expression MemoryLoadResolver::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;
+}
+
+// TODO does it have to be _expr
+bool MemoryLoadResolver::invalidatesMemoryLocation(YulString const& _name, Expression const& _expression)
+{
+	if (!holds_alternative<FunctionCall>(_expression))
+		return true;
+
+	FunctionCall const& functionCall = get<FunctionCall>(_expression);
+
+	auto addMemoryConstraints = [&](
+		evmasm::Instruction _instruction,
+		smtutil::Expression _memoryLocation,
+		vector<yul::Expression> const& _arguments
+	)
+	{
+		vector<smtutil::Expression> arguments = applyMap(
+			_arguments,
+			[this](yul::Expression const& _expr) { return encodeExpression(_expr); }
+		);
+
+		switch (_instruction)
+		{
+
+		case evmasm::Instruction::CALLDATACOPY:
+		case evmasm::Instruction::CODECOPY:
+		case evmasm::Instruction::RETURNDATACOPY:
+			yulAssert(arguments.size() == 3, "");
+			m_solver->addAssertion(arguments.at(0) <= _memoryLocation);
+			m_solver->addAssertion(_memoryLocation < arguments.at(0) + arguments.at(2));
+			break;
+
+		case evmasm::Instruction::EXTCODECOPY:
+			yulAssert(arguments.size() == 4, "");
+			m_solver->addAssertion(arguments.at(1) <= _memoryLocation);
+			m_solver->addAssertion(_memoryLocation < arguments.at(1) + arguments.at(3));
+			break;
+
+		// TODO Should mstore and mstore8 be dealt with separately?
+		case evmasm::Instruction::MSTORE:
+			yulAssert(arguments.size() == 2, "");
+			m_solver->addAssertion(arguments.at(0) <= _memoryLocation);
+			m_solver->addAssertion(_memoryLocation < arguments.at(0) + constantValue(32));
+			break;
+
+		case evmasm::Instruction::MSTORE8:
+			yulAssert(arguments.size() == 2, "");
+			m_solver->addAssertion(arguments.at(0) <= _memoryLocation);
+			m_solver->addAssertion(_memoryLocation < arguments.at(0) + constantValue(1));
+			break;
+
+		case evmasm::Instruction::CALL:
+		case evmasm::Instruction::CALLCODE:
+			yulAssert(arguments.size() == 7, "");
+			m_solver->addAssertion(arguments.at(5) <= _memoryLocation);
+			m_solver->addAssertion(_memoryLocation < arguments.at(5) + arguments.at(6));
+			break;
+
+		case evmasm::Instruction::STATICCALL:
+		case evmasm::Instruction::DELEGATECALL:
+			yulAssert(arguments.size() == 6, "");
+			m_solver->addAssertion(arguments.at(4) <= _memoryLocation);
+			m_solver->addAssertion(_memoryLocation < arguments.at(4) + arguments.at(5));
+			break;
+
+		default:
+			;
+		}
+	};
+
+	if (auto dialect = dynamic_cast<EVMDialect const*>(&m_dialect))
+		if (auto builtin = dialect->builtin(functionCall.functionName.name))
+			if (builtin->instruction)
+			{
+				// TODO at this point, the constraints should be satisfiable.
+				// ADD an assert about it?
+				m_solver->push();
+				addMemoryConstraints(
+					*builtin->instruction,
+					m_variables.at(_name),
+					functionCall.arguments
+				);
+
+				CheckResult result1 = m_solver->check({}).first;
+				m_solver->pop();
+
+				m_solver->push();
+				addMemoryConstraints(
+					*builtin->instruction,
+					m_variables.at(_name) + constantValue(31),
+					functionCall.arguments
+				);
+
+				CheckResult result2 = m_solver->check({}).first;
+				m_solver->pop();
+
+				if (
+					(result1 == CheckResult::UNSATISFIABLE) &&
+					(result2 == CheckResult::UNSATISFIABLE)
+				)
+						return false;
+
+			}
+
+	return true;
+}
diff --git a/libyul/optimiser/MemoryLoadResolver.h b/libyul/optimiser/MemoryLoadResolver.h
new file mode 100644
index 000000000..cde764cd8
--- /dev/null
+++ b/libyul/optimiser/MemoryLoadResolver.h
@@ -0,0 +1,118 @@
+/*
+	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 <libyul/optimiser/OptimiserStep.h>
+#include <libyul/optimiser/Scoper.h>
+#include <libyul/optimiser/ASTWalker.h>
+
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <libyul/SideEffects.h>
+#include <libyul/AST.h>
+#include <libyul/Dialect.h>
+#include <libyul/YulString.h>
+
+#include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/SolverInterface.h>
+
+#include <set>
+
+namespace solidity::yul
+{
+
+class MemoryLoadResolver: public Scoper
+{
+
+public:
+	static constexpr char const* name{"MemoryLoadResolver"};
+	static void run(OptimiserStepContext& _context, Block& _ast);
+
+	using ASTModifier::operator();
+	void operator()(VariableDeclaration& _v) override;
+	void operator()(FunctionCall& _f) override;
+
+	using ASTModifier::visit;
+	void visit(Expression& _e) override;
+
+private:
+	MemoryLoadResolver(
+		Dialect const& _dialect,
+		std::map<YulString, SideEffects> _functionSideEffects,
+		std::set<YulString> _ssaVariables,
+		bool _containsMsize
+	) :
+		m_functionSideEffects(std::move(_functionSideEffects)),
+		m_ssaVariables(std::move(_ssaVariables)),
+		m_containsMsize(_containsMsize),
+		m_dialect(_dialect),
+		m_solver(std::make_unique<smtutil::SMTPortfolio>())
+	{}
+
+	/// The mapping for memory
+	std::map<YulString, YulString> m_memory;
+
+	/// Side-effects of user-defined functions. Worst-case side-effects are assumed
+	/// if this is not provided or the function is not found.
+	std::map<YulString, SideEffects> const m_functionSideEffects;
+
+	/// A set of all SSA variables in the AST
+	std::set<YulString> const m_ssaVariables;
+
+	// TODO is this needed? loadresolver seems to use it
+	bool m_containsMsize = true;
+
+	Dialect const& m_dialect;
+
+	/// Checks if a function call is identical to a mstore(x, y), where x and y are SSA variables.
+	std::optional<std::pair<YulString, YulString>> isSimpleMStore(
+		FunctionCall const& _functionCall
+	) const;
+
+
+	smtutil::Expression encodeExpression(
+		Expression const& _expression
+	);
+
+	virtual smtutil::Expression encodeEVMBuiltin(
+		evmasm::Instruction _instruction,
+		std::vector<Expression> const& _arguments
+	);
+
+	smtutil::Expression newVariable();
+	virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256));
+	std::string uniqueName();
+
+	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
+	virtual smtutil::Expression wrap(smtutil::Expression _value);
+
+	virtual smtutil::Expression constantValue(size_t _value) const;
+	virtual smtutil::Expression literalValue(Literal const& _literal) const;
+
+	bool invalidatesMemoryLocation(YulString const& _name, Expression const& _expression);
+
+	std::unique_ptr<smtutil::SolverInterface> m_solver;
+	std::map<YulString, smtutil::Expression> m_variables;
+
+	size_t m_varCounter = 0;
+
+	// TODO have a variable for function side effects
+};
+
+}
diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp
index 3f59e89e6..3fcefe9a4 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/MemoryLoadResolver.h>
 #include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/UnusedFunctionParameterPruner.h>
@@ -195,6 +196,7 @@ map<string, unique_ptr<OptimiserStep>> const& OptimiserSuite::allSteps()
 			LiteralRematerialiser,
 			LoadResolver,
 			LoopInvariantCodeMotion,
+			MemoryLoadResolver,
 			RedundantAssignEliminator,
 			ReasoningBasedSimplifier,
 			Rematerialiser,
@@ -234,6 +236,7 @@ map<string, char> const& OptimiserSuite::stepNameToAbbreviationMap()
 		{LiteralRematerialiser::name,         'T'},
 		{LoadResolver::name,                  'L'},
 		{LoopInvariantCodeMotion::name,       'M'},
+		{MemoryLoadResolver::name,            'y'},
 		{ReasoningBasedSimplifier::name,      'R'},
 		{RedundantAssignEliminator::name,     'r'},
 		{Rematerialiser::name,                'm'},