diff --git a/libsmtutil/Helpers.h b/libsmtutil/Helpers.h
index fa6081b16..feeb9a7d5 100644
--- a/libsmtutil/Helpers.h
+++ b/libsmtutil/Helpers.h
@@ -25,7 +25,7 @@ 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)
+inline Expression signedDivisionEVM(Expression _left, Expression _right)
 {
 	return Expression::ite(
 		_left >= 0,
@@ -42,7 +42,7 @@ inline Expression abs(Expression _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)
+inline Expression signedModuloEVM(Expression _left, Expression _right)
 {
 	return Expression::ite(
 		_left >= 0,
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index cb7322d62..90df7a908 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1506,7 +1506,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.
 	if (_type.isSigned())
-		return signedDivision(_left, _right);
+		return signedDivisionEVM(_left, _right);
 	else
 		return _left / _right;
 }
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 90c3916c2..ea464f248 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -176,12 +176,11 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 			// 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(
+			signedToUnsigned(smtutil::signedDivisionEVM(
 				unsignedToSigned(arguments.at(0)),
 				unsignedToSigned(arguments.at(1))
 			))
 		);
-		break;
 	case evmasm::Instruction::MOD:
 		return smtutil::Expression::ite(
 			arguments.at(1) == constantValue(0),
@@ -192,12 +191,11 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 		return smtutil::Expression::ite(
 			arguments.at(1) == constantValue(0),
 			constantValue(0),
-			signedToUnsigned(signedModulo(
+			signedToUnsigned(signedModuloEVM(
 				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: