diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 1fe2e9d30..acac0c1bc 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -160,8 +160,8 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 			// 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))
+				twosComplementToUpscaledUnsigned(arguments.at(0)),
+				twosComplementToUpscaledUnsigned(arguments.at(1))
 			))
 		);
 	case evmasm::Instruction::MOD:
@@ -175,18 +175,24 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 			arguments.at(1) == constantValue(0),
 			constantValue(0),
 			signedToTwosComplement(signedModuloEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
+				twosComplementToUpscaledUnsigned(arguments.at(0)),
+				twosComplementToUpscaledUnsigned(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)));
+		return booleanValue(
+			twosComplementToUpscaledUnsigned(arguments.at(0)) + smtutil::Expression(bigint(1) << 256) <
+			twosComplementToUpscaledUnsigned(arguments.at(1)) + smtutil::Expression(bigint(1) << 256)
+		);
 	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)));
+		return booleanValue(
+			twosComplementToUpscaledUnsigned(arguments.at(0)) + smtutil::Expression(bigint(1) << 256) >
+			twosComplementToUpscaledUnsigned(arguments.at(1)) + smtutil::Expression(bigint(1) << 256)
+		);
 	case evmasm::Instruction::EQ:
 		return booleanValue(arguments.at(0) == arguments.at(1));
 	case evmasm::Instruction::ISZERO:
diff --git a/libyul/optimiser/SMTSolver.cpp b/libyul/optimiser/SMTSolver.cpp
index 2cd662063..033597a13 100644
--- a/libyul/optimiser/SMTSolver.cpp
+++ b/libyul/optimiser/SMTSolver.cpp
@@ -105,7 +105,6 @@ shared_ptr<Sort> SMTSolver::defaultSort() const
 
 smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value)
 {
-	// TODO should not use ite
 	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
 }
 
@@ -119,13 +118,12 @@ smtutil::Expression SMTSolver::literalValue(Literal const& _literal)
 	return smtutil::Expression(valueOfLiteral(_literal));
 }
 
-smtutil::Expression SMTSolver::twosComplementToSigned(smtutil::Expression _value)
+smtutil::Expression SMTSolver::twosComplementToUpscaledUnsigned(smtutil::Expression _value)
 {
-	// TODO will that work for LP?
 	return smtutil::Expression::ite(
 		_value < smtutil::Expression(bigint(1) << 255),
-		_value,
-		_value - smtutil::Expression(bigint(1) << 256)
+		_value + smtutil::Expression(bigint(1) << 256),
+		_value
 	);
 }
 
diff --git a/libyul/optimiser/SMTSolver.h b/libyul/optimiser/SMTSolver.h
index dfc54687e..3541a74d7 100644
--- a/libyul/optimiser/SMTSolver.h
+++ b/libyul/optimiser/SMTSolver.h
@@ -76,7 +76,8 @@ protected:
 	static smtutil::Expression booleanValue(smtutil::Expression _value);
 	static smtutil::Expression constantValue(bigint _value);
 	static smtutil::Expression literalValue(Literal const& _literal);
-	static smtutil::Expression twosComplementToSigned(smtutil::Expression _value);
+	/// Returns _value interpreted as a two's complement number and adds 2**256
+	static smtutil::Expression twosComplementToUpscaledUnsigned(smtutil::Expression _value);
 	static smtutil::Expression signedToTwosComplement(smtutil::Expression _value);
 	smtutil::Expression wrap(smtutil::Expression _value);