diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 88ade7e12..02f9374a1 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -680,9 +680,12 @@ let rec simp_eq x y =
   (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
   | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
       simp_cond c (simp_eq e t) (simp_eq e f)
-  (* e = e ==> true *)
-  | x, y when equal x y -> bool true
-  | x, y -> Ap2 (Eq, x, y)
+  | x, y -> (
+    match Int.sign (compare x y) with
+    (* e = e ==> true *)
+    | Zero -> bool true
+    | Neg -> Ap2 (Eq, x, y)
+    | Pos -> Ap2 (Eq, y, x) )
 
 and simp_dq x y =
   match (x, y) with
diff --git a/sledge/src/llair/term_test.ml b/sledge/src/llair/term_test.ml
index 6fde19254..ad8de1264 100644
--- a/sledge/src/llair/term_test.ml
+++ b/sledge/src/llair/term_test.ml
@@ -151,7 +151,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z = y) ;
-      [%expect {| (%z_2 = %y_1) |}]
+      [%expect {| (%y_1 = %z_2) |}]
 
     let%expect_test _ =
       pp (z = z) ;
@@ -191,7 +191,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
@@ -207,23 +207,23 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 42) = (3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 42) = (-3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((10 × %z_2 + 42) = (-3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
 
     let%expect_test _ =
       pp ~~(!2 < y && z <= !3) ;
@@ -241,9 +241,9 @@ let%test_module _ =
         {|
         (%z_2 = 0)
 
-        (0 = %z_2)
+        (%z_2 = 0)
 
-        (0 = %z_2) |}]
+        (%z_2 = 0) |}]
 
     let%expect_test _ =
       let z1 = z + !1 in