diff --git a/libsolidity/interface/OptimiserSettings.h b/libsolidity/interface/OptimiserSettings.h
index e1c35e9ea..a1bbda563 100644
--- a/libsolidity/interface/OptimiserSettings.h
+++ b/libsolidity/interface/OptimiserSettings.h
@@ -45,7 +45,7 @@ struct OptimiserSettings
 		"dhfoDgvulfnTUtnIf"            // None of these can make stack problems worse
 		"["
 			"xa[r]EscLM"               // Turn into SSA and simplify
-			"cCTUtTOntnfDIul"          // Perform structural simplification
+			"RcCTUtTOntnfDIul"          // Perform structural simplification
 			"Lcul"                     // Simplify again
 			"Vcul [j]"                 // Reverse SSA
 
diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 20dc27004..17a093236 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -247,9 +247,9 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
 
 pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const& _expressionsToEvaluate)
 {
-//	cout << "Solving boolean constraint system" << endl;
-//	cout << toString() << endl;
-//	cout << "--------------" << endl;
+	cout << "Solving boolean constraint system" << endl;
+	cout << toString() << endl;
+	cout << "--------------" << endl;
 
 	if (m_state.back().infeasible)
 		return make_pair(CheckResult::UNSATISFIABLE, vector<string>{});
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 94c7102bd..9f4c08efd 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -22,11 +22,14 @@
 #include <libyul/optimiser/Semantics.h>
 #include <libyul/AST.h>
 #include <libyul/Dialect.h>
+#include <libyul/Utilities.h>
 
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
 #include <libsolutil/CommonData.h>
+#include <libsolutil/BooleanLP.h>
+#include <libsolutil/Visitor.h>
 
 #include <utility>
 #include <memory>
@@ -43,31 +46,83 @@ void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _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)
 {
-	SMTSolver::encodeVariableDeclaration(_varDecl);
+	if (_varDecl.variables.size() != 1 || !_varDecl.value)
+		return;
+	YulString varName = _varDecl.variables.front().name;
+	if (!m_ssaVariables.count(varName))
+		return;
+
+	// TODO for a boolean variable, we could check if it is
+	// a constant.
+
+	smtutil::Expression variable = newRestrictedVariable(
+		"yul_" + varName.str(),
+		_varDecl.value && isBoolean(*_varDecl.value)
+	);
+	bool const inserted = m_variables.insert({varName, variable}).second;
+	yulAssert(inserted, "");
+	if (!_varDecl.value)
+		return; // TODO we could encode zero, but the variable should not be used anyway.
+
+	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)
+							handleDeclaration(varName, *builtin->instruction, _functionCall.arguments);
+		},
+		[&](Identifier const& _identifier)
+		{
+			if (
+				m_ssaVariables.count(_identifier.name) &&
+				m_variables.count(_identifier.name)
+			)
+				m_solver->addAssertion(variable == m_variables.at(_identifier.name));
+		},
+		[&](Literal const& _literal)
+		{
+			// TODO could avoid encoding the restrictions.
+			m_solver->addAssertion(variable == literalValue(_literal));
+		}
+	}, *_varDecl.value);
+
+	if (_varDecl.value && isBoolean(*_varDecl.value) && SideEffectsCollector{m_dialect, *_varDecl.value}.movable())
+	{
+		// TODO if we use this, then it actually already handles the if statement case...
+		if (makesInfeasible(!variable))
+			// TODO debug data
+			_varDecl.value = make_unique<yul::Expression>(m_dialect.trueLiteral());
+		else if (makesInfeasible(variable))
+			_varDecl.value = make_unique<yul::Expression>(m_dialect.zeroLiteralForType({}));
+	}
+// TODO could use 	SMTSolver::encodeVariableDeclaration(_varDecl);
 }
 
 void ReasoningBasedSimplifier::operator()(If& _if)
 {
-	if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
+	if (!holds_alternative<Identifier>(*_if.condition))
+	{
+		ASTModifier::operator()(_if.body);
 		return;
+	}
+	Identifier const& condition = get<Identifier>(*_if.condition);
+	if (!m_ssaVariables.count(condition.name) || !m_variables.count(condition.name))
+	{
+		ASTModifier::operator()(_if.body);
+		return;
+	}
+	smtutil::Expression cond = m_variables.at(condition.name);
 
-	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)
+	bool constantTrue = makesInfeasible(
+		isBoolean(*_if.condition) ?
+		!cond :
+		(cond == bigint(0))
+	);
+
+	if (constantTrue)
 	{
 		Literal trueCondition = m_dialect.trueLiteral();
 		trueCondition.debugData = debugDataOf(*_if.condition);
@@ -75,11 +130,13 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 	}
 	else
 	{
-		m_solver->push();
-		m_solver->addAssertion(condition != constantValue(0));
-		CheckResult result2 = m_solver->check({}).first;
-		m_solver->pop();
-		if (result2 == CheckResult::UNSATISFIABLE)
+		bool constantFalse = makesInfeasible(
+			isBoolean(*_if.condition) ?
+			cond :
+			(cond >= bigint(1))
+		);
+
+		if (constantFalse)
 		{
 			Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
 			falseCondition.debugData = debugDataOf(*_if.condition);
@@ -91,10 +148,61 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 	}
 
 	m_solver->push();
-	m_solver->addAssertion(condition != constantValue(0));
+	if (isBoolean(*_if.condition))
+		m_solver->addAssertion(cond);
+	else
+		m_solver->addAssertion(cond >= bigint(1));
 
 	ASTModifier::operator()(_if.body);
+	m_solver->pop();
 
+	// TODO if we do this, we have to push/pop inside for loops because
+	// 'leave' / 'continue' is considered terminating.
+	bool bodyTerminates =
+		!_if.body.statements.empty() &&
+		TerminationFinder(m_dialect).controlFlowKind(_if.body.statements.back()) !=
+		TerminationFinder::ControlFlow::FlowOut;
+
+	if (bodyTerminates)
+	{
+		cout << "Body always terminates." << endl;
+		if (isBoolean(*_if.condition))
+			m_solver->addAssertion(!cond);
+		else
+			m_solver->addAssertion(cond == bigint(0));
+	}
+}
+
+// TODO switch also needs push/pop?
+
+// TODO does break/continue need pecial handling in loops?
+// TODO leave in functions?
+
+void ReasoningBasedSimplifier::operator()(ForLoop& _for)
+{
+	(*this)(_for.pre);
+	visit(*_for.condition);
+	m_solver->push();
+
+	Identifier const* condition = get_if<Identifier>(_for.condition.get());
+	if (condition && m_ssaVariables.count(condition->name) && m_variables.count(condition->name))
+	{
+		smtutil::Expression cond = m_variables.at(condition->name);
+		if (isBoolean(*_for.condition))
+			m_solver->addAssertion(cond);
+		else
+			m_solver->addAssertion(cond >= bigint(1));
+	}
+	(*this)(_for.body);
+	(*this)(_for.post);
+
+	m_solver->pop();
+}
+
+void ReasoningBasedSimplifier::operator()(FunctionDefinition& _fun)
+{
+	m_solver->push();
+	ASTModifier::operator()(_fun);
 	m_solver->pop();
 }
 
@@ -102,125 +210,202 @@ ReasoningBasedSimplifier::ReasoningBasedSimplifier(
 	Dialect const& _dialect,
 	set<YulString> const& _ssaVariables
 ):
-	SMTSolver(_ssaVariables, _dialect),
-	m_dialect(_dialect)
+	m_dialect(_dialect),
+	m_ssaVariables(_ssaVariables),
+	m_solver(make_unique<util::BooleanLPSolver>())
 {
 }
 
-
-smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
+void ReasoningBasedSimplifier::handleDeclaration(
+	YulString _varName,
 	evmasm::Instruction _instruction,
 	vector<yul::Expression> const& _arguments
 )
 {
-	vector<smtutil::Expression> arguments = applyMap(
-		_arguments,
-		[this](yul::Expression const& _expr) { return encodeExpression(_expr); }
-	);
+	smtutil::Expression variable = m_variables.at(_varName);
+	vector<smtutil::Expression> arguments;
+	for (yul::Expression const& arg: _arguments)
+	{
+		if (holds_alternative<Identifier>(arg))
+		{
+			Identifier const& v = get<Identifier>(arg);
+			if (!m_ssaVariables.count(v.name) || !m_variables.count(v.name))
+				return;
+			arguments.push_back(m_variables.at(v.name));
+		}
+		else if (holds_alternative<Literal>(arg))
+			arguments.push_back(literalValue(get<Literal>(arg)));
+		else
+			return;
+	}
+
+	optional<smtutil::Expression> x;
+	optional<smtutil::Expression> y;
+	optional<smtutil::Expression> z;
+	if (arguments.size() > 0)
+		x = arguments.at(0);
+	if (arguments.size() > 1)
+		y = arguments.at(1);
+	if (arguments.size() > 2)
+		z = arguments.at(2);
+
 	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));
+	{
+		smtutil::Expression overflow = m_solver->newVariable(uniqueName(), SortProvider::boolSort);
+		m_solver->addAssertion(overflow || (variable == *x + *y));
+		m_solver->addAssertion(!overflow || (variable == *x + *y - smtutil::Expression(bigint(1) << 256)));
+		break;
+	}
 	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 `signedToTwosComplement`
-			signedToTwosComplement(smtutil::signedDivisionEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
-			))
-		);
-	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),
-			signedToTwosComplement(signedModuloEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
-			))
-		);
-	case evmasm::Instruction::LT:
-		return booleanValue(arguments.at(0) < arguments.at(1));
-	case evmasm::Instruction::SLT:
-		return booleanValue(twosComplementToSigned(arguments.at(0)) < twosComplementToSigned(arguments.at(1)));
-	case evmasm::Instruction::GT:
-		return booleanValue(arguments.at(0) > arguments.at(1));
-	case evmasm::Instruction::SGT:
-		return booleanValue(twosComplementToSigned(arguments.at(0)) > twosComplementToSigned(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))))
-		);
+	{
+		smtutil::Expression underflow = m_solver->newVariable(uniqueName(), SortProvider::boolSort);
+		m_solver->addAssertion(underflow || (variable == *x - *y));
+		m_solver->addAssertion(!underflow || (variable == *x - *y + smtutil::Expression(bigint(1) << 256)));
+		break;
+	}
+	//case evmasm::Instruction::MUL:
+		// TODO encode constants?
+	//case evmasm::Instruction::DIV:
 	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
+		m_solver->addAssertion(variable < *z);
+		break;
+	case evmasm::Instruction::LT:
+		m_solver->addAssertion(variable == (*x < *y));
+		break;
+	case evmasm::Instruction::GT:
+		m_solver->addAssertion(variable == (*x > *y));
+		break;
+	//	case evmasm::Instruction::SLT:
+	//	case evmasm::Instruction::SGT:
+	// TODO
+	case evmasm::Instruction::EQ:
+		m_solver->addAssertion(variable == (*x == *y));
+		break;
+	case evmasm::Instruction::ISZERO:
+		if (isBoolean(_arguments.at(0)))
+			m_solver->addAssertion(variable == (!*x));
+		else
+			m_solver->addAssertion(variable == (*x <= smtutil::Expression(bigint(0))));
+		break;
+	case evmasm::Instruction::NOT:
+		if (isBoolean(_arguments.at(0)))
+			m_solver->addAssertion(variable == (!*x));
+		else
+			// TODO is this correct?
+			m_solver->addAssertion(variable == ((smtutil::Expression(bigint(1) << 256) - 1) - *x));
+		break;
+	case evmasm::Instruction::AND:
+		if (m_booleanVariables.count(_varName.str()))
+			m_solver->addAssertion(variable == (*x && *y));
+		else
+			m_solver->addAssertion(variable <= *x && variable <= *y);
+		break;
+	case evmasm::Instruction::OR:
+		if (m_booleanVariables.count(_varName.str()))
+			m_solver->addAssertion(variable == (*x || *y));
+		else
+		{
+			m_solver->addAssertion(variable >= *x && variable >= *y);
+			m_solver->addAssertion(variable <= *x + *y);
+		}
+		break;
+	// TODO all builtins whose return values can be restricted.
 	default:
 		break;
 	}
-	return newRestrictedVariable();
+}
+
+smtutil::Expression ReasoningBasedSimplifier::newRestrictedVariable(string const& _name, bool _boolean)
+{
+	string name = _name.empty() ? uniqueName() : _name;
+	if (_boolean)
+		m_booleanVariables.insert(name);
+	smtutil::Expression var = m_solver->newVariable(name, _boolean ? SortProvider::boolSort : defaultSort());
+	if (!_boolean)
+		m_solver->addAssertion(var <= smtutil::Expression(bigint(1) << 256) - 1);
+	return var;
+}
+
+string ReasoningBasedSimplifier::uniqueName()
+{
+	return "expr_" + to_string(m_varCounter++);
+}
+bool ReasoningBasedSimplifier::makesInfeasible(smtutil::Expression _constraint)
+{
+	m_solver->push();
+	m_solver->addAssertion(_constraint);
+	bool result = infeasible();
+	m_solver->pop();
+	return result;
+}
+
+bool ReasoningBasedSimplifier::feasible()
+{
+	CheckResult result = m_solver->check({}).first;
+	return result == CheckResult::SATISFIABLE;
+}
+
+bool ReasoningBasedSimplifier::infeasible()
+{
+	CheckResult result = m_solver->check({}).first;
+	return result == CheckResult::UNSATISFIABLE;
+}
+
+YulString ReasoningBasedSimplifier::localVariableFromExpression(string const& _expressionName)
+{
+	solAssert(_expressionName.substr(0, 4) == "yul_", "");
+	return YulString(_expressionName.substr(4));
+
+}
+
+bool ReasoningBasedSimplifier::isBoolean(Expression const& _expression) const
+{
+	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))
+							  // TODO assert
+					switch (*builtin->instruction)
+					{
+					case evmasm::Instruction::LT:
+					case evmasm::Instruction::GT:
+					case evmasm::Instruction::SLT:
+					case evmasm::Instruction::SGT:
+					case evmasm::Instruction::EQ:
+					case evmasm::Instruction::ISZERO:
+						return true;
+					case evmasm::Instruction::AND:
+					case evmasm::Instruction::OR:
+						return
+							isBoolean(_functionCall.arguments.at(0)) &&
+							isBoolean(_functionCall.arguments.at(1));
+					case evmasm::Instruction::NOT:
+						return isBoolean(_functionCall.arguments.at(0));
+					default:
+						break;
+					}
+			return false;
+		},
+		[&](Identifier const& _identifier) -> bool
+		{
+			return m_booleanVariables.count("yul_" + _identifier.name.str());
+		},
+		[&](Literal const& _literal)
+		{
+			return _literal.kind == LiteralKind::Boolean;
+		}
+	}, _expression);
+}
+
+shared_ptr<Sort> ReasoningBasedSimplifier::defaultSort() const
+{
+	return SortProvider::intSort();
+}
+
+smtutil::Expression ReasoningBasedSimplifier::literalValue(Literal const& _literal) const
+{
+	return smtutil::Expression(valueOfLiteral(_literal));
 }
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h
index c458a36d0..9e2c424a0 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.h
+++ b/libyul/optimiser/ReasoningBasedSimplifier.h
@@ -47,16 +47,17 @@ namespace solidity::yul
  *
  * Prerequisite: Disambiguator, SSATransform.
  */
-class ReasoningBasedSimplifier: public ASTModifier, SMTSolver
+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;
+	void operator()(ForLoop& _for) override;
+	void operator()(FunctionDefinition& _function) override;
 
 private:
 	explicit ReasoningBasedSimplifier(
@@ -64,12 +65,36 @@ private:
 		std::set<YulString> const& _ssaVariables
 	);
 
-	smtutil::Expression encodeEVMBuiltin(
+	smtutil::Expression encodeExpression(
+		Expression const& _expression
+	);
+
+	void handleDeclaration(
+		YulString _varName,
 		evmasm::Instruction _instruction,
 		std::vector<Expression> const& _arguments
-	) override;
+	);
 
+	smtutil::Expression newRestrictedVariable(std::string const& _name = {}, bool _boolean = false);
+	std::string uniqueName();
+
+	bool makesInfeasible(smtutil::Expression _constraint);
+	bool feasible();
+	bool infeasible();
+
+	YulString localVariableFromExpression(std::string const& _expressionName);
+
+	bool isBoolean(Expression const& _expression) const;
+
+	std::shared_ptr<smtutil::Sort> defaultSort() const;
+	smtutil::Expression literalValue(Literal const& _literal) const;
 	Dialect const& m_dialect;
+	std::set<YulString> const& m_ssaVariables;
+	std::unique_ptr<smtutil::SolverInterface> m_solver;
+	std::map<YulString, smtutil::Expression> m_variables;
+	std::set<std::string> m_booleanVariables;
+
+	size_t m_varCounter = 0;
 };
 
 }
diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp
index 6404fa7c6..b50bcb38e 100644
--- a/test/libyul/YulOptimizerTest.cpp
+++ b/test/libyul/YulOptimizerTest.cpp
@@ -24,7 +24,6 @@
 #include <test/Common.h>
 
 #include <libyul/Object.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/AsmPrinter.h>
 
 #include <liblangutil/CharStreamProvider.h>
@@ -53,12 +52,6 @@ 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 ||
-		ReasoningBasedSimplifier::invalidInCurrentEnvironment()
-	))
-		m_shouldRun = false;
-
 	m_source = m_reader.source();
 
 	auto dialectName = m_reader.stringSetting("dialect", "evm");
diff --git a/test/libyul/YulOptimizerTestCommon.cpp b/test/libyul/YulOptimizerTestCommon.cpp
index e7711f586..77d4ee856 100644
--- a/test/libyul/YulOptimizerTestCommon.cpp
+++ b/test/libyul/YulOptimizerTestCommon.cpp
@@ -283,8 +283,17 @@ YulOptimizerTestCommon::YulOptimizerTestCommon(
 		}},
 		{"reasoningBasedSimplifier", [&]() {
 			disambiguate();
+			ExpressionSplitter::run(*m_context, *m_ast);
+			SSATransform::run(*m_context, *m_ast);
+			RedundantAssignEliminator::run(*m_context, *m_ast);
+
 			ReasoningBasedSimplifier::run(*m_context, *m_object->code);
-		}},
+
+			SSAReverser::run(*m_context, *m_ast);
+			UnusedPruner::run(*m_context, *m_ast);
+			ExpressionJoiner::run(*m_context, *m_ast);
+			ExpressionJoiner::run(*m_context, *m_ast);
+		 }},
 		{"equivalentFunctionCombiner", [&]() {
 			disambiguate();
 			ForLoopInitRewriter::run(*m_context, *m_ast);
diff --git a/test/libyul/yulOptimizerTests/fullSuite/clear_after_if_continue.yul b/test/libyul/yulOptimizerTests/fullSuite/clear_after_if_continue.yul
index 71ed36d97..738c828b9 100644
--- a/test/libyul/yulOptimizerTests/fullSuite/clear_after_if_continue.yul
+++ b/test/libyul/yulOptimizerTests/fullSuite/clear_after_if_continue.yul
@@ -16,16 +16,10 @@
 //         for { }
 //         iszero(_1)
 //         {
-//             if y
-//             {
-//                 let _2 := 0
-//                 revert(_2, _2)
-//             }
-//         }
-//         {
-//             if y { continue }
-//             sstore(1, 0)
+//             let _2 := 0
+//             revert(_2, _2)
 //         }
+//         { continue }
 //         if y { revert(0, 0) }
 //     }
 // }
diff --git a/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul b/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul
index 13683e8e6..4d16e3f81 100644
--- a/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul
+++ b/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul
@@ -40,6 +40,26 @@
 //
 // {
 //     {
+//         let _1 := gt(not(gcd(10, 15)), 1)
+//         let _2 := gcd(10, 15)
+//         let _3 := not(0)
+//         let _4 := lt(or(1, add(gcd(10, 15), _3)), 1)
+//         let _5 := gcd(10, 15)
+//         let _6 := gcd(10, 15)
+//         pop(keccak256(gcd(10, 15), or(gt(not(gcd(10, 15)), 1), 1)))
+//         mstore(lt(or(gt(1, or(or(gt(or(or(or(gt(or(gt(_3, _6), 1), _5), _4), _2), 1), 1), _1), 1)), 1), 1), 1)
+//         sstore(not(gcd(10, 15)), 1)
+//         let _1 := 15
+//         let _2 := 10
+//         pop(gcd(_2, _1))
+//         pop(gcd(_2, _1))
+//         pop(gcd(_2, _1))
+//         pop(gcd(_2, _1))
+//         pop(gcd(_2, _1))
+//         let _3 := 1
+//         pop(keccak256(gcd(_2, _1), or(gt(not(gcd(_2, _1)), _3), _3)))
+//         mstore(0, _3)
+//         sstore(not(gcd(_2, _1)), _3)
 //         let _1 := 1
 //         let _2 := 15
 //         let _3 := 10
@@ -53,6 +73,14 @@
 //         mstore(lt(or(gt(_1, or(or(gt(or(or(or(gt(or(gt(_6, _9), _1), _8), _7), _5), _1), _1), _4), _1)), _1), _1), _1)
 //         sstore(not(gcd(_3, _2)), _1)
 //         sstore(0, 0)
+//         sstore(2, 1)
+//         extcodecopy(1, msize(), 1, 1)
+//         sstore(0, 0)
+//         sstore(3, 1)
+//         sstore(2, _3)
+//         extcodecopy(_3, msize(), _3, _3)
+//         sstore(0, 0)
+//         sstore(3, _3)
 //         sstore(2, _1)
 //         extcodecopy(_1, msize(), _1, _1)
 //         sstore(3, _1)
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addcheck.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addcheck.yul
new file mode 100644
index 000000000..87ace6e57
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addcheck.yul
@@ -0,0 +1,21 @@
+{
+    let x := calldataload(0)
+    let y := calldataload(1)
+    if gt(x, 200) { revert(0, 0) }
+    if gt(y, 600) { revert(0, 0) }
+    if gt(x, not(y)) { revert(0, 0) }
+    sstore(0, add(x, y))
+}
+// ====
+// EVMVersion: >=constantinople
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(1)
+//     if gt(x, 200) { revert(0, 0) }
+//     if gt(y, 600) { revert(0, 0) }
+//     if 0 { }
+//     sstore(0, add(x, y))
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul
index 7ff930766..8492093c4 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul
@@ -6,8 +6,4 @@
 // ----
 // step: reasoningBasedSimplifier
 //
-// {
-//     let x := 7
-//     let y := 8
-//     if 1 { }
-// }
+// { if 1 { } }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul
index 31a342339..6dee0961c 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul
@@ -1,8 +1,8 @@
 {
     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 lt(vloc_x, 0x1000000000000000) {
+        if lt(vloc_y, 0x1000000000000000) {
             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)
@@ -18,14 +18,13 @@
 // {
 //     let vloc_x := calldataload(0)
 //     let vloc_y := calldataload(1)
-//     if lt(vloc_x, shl(100, 1))
+//     if lt(vloc_x, 0x1000000000000000)
 //     {
-//         if lt(vloc_y, shl(100, 1))
+//         if lt(vloc_y, 0x1000000000000000)
 //         {
-//             if 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)
+//                 sstore(0, mul(vloc_x, vloc_y))
 //             }
 //         }
 //     }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul
index f5226acf7..defc64063 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul
@@ -25,7 +25,13 @@
 //     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 { } }
+//     if gt(result, z) { sstore(0, 1) }
+//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000))
+//     {
+//         if eq(result, mod(mul(x, y), z)) { sstore(0, 9) }
+//     }
+//     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) }
+//     }
 // }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul
index 6e4b3f5ed..2680fc684 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul
@@ -11,6 +11,6 @@
 // {
 //     let x := sub(0, 7)
 //     let y := 2
-//     if 1 { }
-//     if 0 { }
+//     if iszero(add(sdiv(x, y), 3)) { }
+//     if iszero(add(sdiv(x, y), 4)) { }
 // }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul
index d7002c99b..bfe91fc2c 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul
@@ -14,8 +14,7 @@
 //
 // {
 //     let x := calldataload(2)
-//     let t := lt(x, 20)
-//     if t
+//     if lt(x, 20)
 //     {
 //         if 1 { }
 //         if 1 { }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul
index 1e409079e..5e90a35a9 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul
@@ -25,7 +25,10 @@
 //     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) } }
+//         if eq(sdiv(y, sub(0, 1)), y) { sstore(0, 7) }
+//         if iszero(eq(y, t))
+//         {
+//             if eq(sdiv(t, sub(0, 1)), sub(0, t)) { sstore(1, 7) }
+//         }
 //     }
 // }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul
index 12f04c857..a580899f7 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul
@@ -38,16 +38,31 @@
 //     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(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 1 { sstore(0, 7) } }
-//         if eq(y, sub(0, 5)) { if 1 { sstore(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 1 { sstore(0, 7) } }
+//         if eq(y, sub(0, 5))
+//         {
+//             if eq(result, 0) { sstore(0, 7) }
+//         }
 //     }
 // }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul
index 69f5c6769..d0644e7e5 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul
@@ -8,8 +8,6 @@
 // step: reasoningBasedSimplifier
 //
 // {
-//     let x := 7
-//     let y := 8
 //     if 1 { }
 //     if 1 { }
 // }