diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java
index 6540007bbd1..9621f33483e 100644
--- a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java
+++ b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java
@@ -574,6 +574,68 @@ public void bvConstantsCase() {
 		runUnfTest(new FunDecl[0], formulaAsString, expected, mMgdScript);
 	}
 
+	// --- Operator mirroring (bvugt/bvuge/bvsgt/bvsge -> bvult/bvule/bvslt/bvsle) ---
+
+	@Test
+	public void bvugtMirroredToBvult() {
+		// Unsigned "greater than" is eliminated by swapping operands into "less than": (x bvugt 1) -> (1 bvult x).
+		final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") };
+		final String formulaAsString = "(bvugt x (_ bv1 8))";
+		final String expected = "(bvult (_ bv1 8) x)";
+
+		runUnfTest(funDecls, formulaAsString, expected, mMgdScript);
+	}
+
+	@Test
+	public void bvugeMirroredToBvule() {
+		// Same mirroring for the non-strict unsigned variant: (x bvuge 1) -> (1 bvule x).
+		final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") };
+		final String formulaAsString = "(bvuge x (_ bv1 8))";
+		final String expected = "(bvule (_ bv1 8) x)";
+
+		runUnfTest(funDecls, formulaAsString, expected, mMgdScript);
+	}
+
+	@Test
+	public void bvsgtMirroredToBvslt() {
+		// Signed "greater than" is mirrored the same way as the unsigned case: (x bvsgt 1) -> (1 bvslt x).
+		final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") };
+		final String formulaAsString = "(bvsgt x (_ bv1 8))";
+		final String expected = "(bvslt (_ bv1 8) x)";
+
+		runUnfTest(funDecls, formulaAsString, expected, mMgdScript);
+	}
+
+	@Test
+	public void bvsgeMirroredToBvsle() {
+		// Same mirroring for the non-strict signed variant: (x bvsge 1) -> (1 bvsle x).
+		final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") };
+		final String formulaAsString = "(bvsge x (_ bv1 8))";
+		final String expected = "(bvsle (_ bv1 8) x)";
+
+		runUnfTest(funDecls, formulaAsString, expected, mMgdScript);
+	}
+
+	@Test
+	public void bvugtConstantFoldingAfterMirroring() {
+		// Guards against a purely syntactic swap: mirroring to bvult must still trigger the existing constant
+		// folding, not just rewrite the operator. Both operands are literals here, so the result must be "true",
+		// not an unevaluated (bvult (_ bv3 8) (_ bv5 8)) term.
+		final String formulaAsString = "(bvugt (_ bv5 8) (_ bv3 8))";
+		final String expected = "true";
+
+		runUnfTest(new FunDecl[0], formulaAsString, expected, mMgdScript);
+	}
+
+	@Test
+	public void bvsgtConstantFoldingAfterMirroring() {
+		// Same guard for the signed variant, to confirm signed constant folding also still works after mirroring.
+		final String formulaAsString = "(bvsgt (_ bv5 8) (_ bv3 8))";
+		final String expected = "true";
+
+		runUnfTest(new FunDecl[0], formulaAsString, expected, mMgdScript);
+	}
+
 	static void runUnfTest(final FunDecl[] funDecls, final String eliminationInputAsString,
 			final String expectedResultAsString, final ManagedScript mgdScript) {
 		for (final FunDecl funDecl : funDecls) {
diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java
index 887688de095..994c14366c0 100644
--- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java
+++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java
@@ -34,6 +34,7 @@
 import java.util.function.Function;
 import java.util.function.Predicate;
 
+import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.binaryrelation.RelationSymbol;
 import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
 import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
 import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol;
@@ -236,12 +237,9 @@ public static Term unfTerm(final Script script, final String funcname, final Big
 					.simplifiedResult(script, funcname, indices, params);
 			break;
 		case bvugt:
-			result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvugt(x, y))
-					.simplifiedResult(script, funcname, indices, params);
-			break;
 		case bvuge:
-			result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvuge(x, y))
-					.simplifiedResult(script, funcname, indices, params);
+			// Mirror to the "less" form instead of folding these separately, e.g. (bvugt a b) -> (bvult b a).
+			result = mirrorGreaterOperator(script, funcname, indices, params);
 			break;
 		case bvslt:
 			result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvslt(x, y))
@@ -252,12 +250,9 @@ public static Term unfTerm(final Script script, final String funcname, final Big
 					.simplifiedResult(script, funcname, indices, params);
 			break;
 		case bvsgt:
-			result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvsgt(x, y))
-					.simplifiedResult(script, funcname, indices, params);
-			break;
 		case bvsge:
-			result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvsge(x, y))
-					.simplifiedResult(script, funcname, indices, params);
+			// Same mirroring for the signed "greater" operators, e.g. (bvsge a b) -> (bvsle b a).
+			result = mirrorGreaterOperator(script, funcname, indices, params);
 			break;
 		default:
 			if (BitvectorUtils.allTermsAreBitvectorConstants(params)) {
@@ -269,6 +264,24 @@ public static Term unfTerm(final Script script, final String funcname, final Big
 		return result;
 	}
 
+	/**
+	 * Rewrites a "greater than" comparison ({@code bvugt}, {@code bvuge}, {@code bvsgt}, {@code bvsge}) into its
+	 * mirrored "less than" form by swapping the two operands, e.g. {@code (bvugt a b)} becomes {@code (bvult b a)}.
+	 * This keeps only 4 comparison operators in normal form instead of 8. The mirrored operator name comes from
+	 * {@link RelationSymbol#swapParameters()}; the actual term is then built by dispatching back into {@link #unfTerm},
+	 * so the existing bvult/bvule/bvslt/bvsle handling (including constant folding) is reused as-is instead of being
+	 * duplicated here.
+	 *
+	 * @param params
+	 *            the two operands of the "greater than" comparison, in their original (unswapped) order
+	 * @return the term constructed for the mirrored "less than" comparison
+	 */
+	private static Term mirrorGreaterOperator(final Script script, final String funcname, final BigInteger[] indices,
+			final Term... params) {
+		final String mirroredFuncname = RelationSymbol.convert(funcname).swapParameters().toString();
+		return unfTerm(script, mirroredFuncname, indices, params[1], params[0]);
+	}
+
 	private static abstract class BitvectorOperation {
 
 		public final Term simplifiedResult(final Script script, final String funcname, final BigInteger[] indices,