diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 0d14776e4..65940541d 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1173,16 +1173,10 @@ let v_map_ses : (var -> var) -> Ses.Var.t -> Ses.Var.t =
   if v' == v then x else v_to_ses v'
 
 let ses_map : (Ses.Term.t -> Ses.Term.t) -> exp -> exp =
- fun f x ->
-  let e = to_ses x in
-  let e' = f e in
-  if e' == e then x else of_ses e'
+ fun f x -> of_ses (f (to_ses x))
 
 let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
- fun f x ->
-  let e = f_to_ses x in
-  let e' = f e in
-  if e' == e then x else f_of_ses e'
+ fun f x -> f_of_ses (f (f_to_ses x))
 
 (*
  * Contexts
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 9c36ca6d2..5208e2522 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -236,7 +236,9 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
+            %l_6
+              -[ %l_6, 16 )->
+              ⟨(8 × %n_9),%a_2⟩^⟨((16 × 1) + (-8 × %n_9)),%a_3⟩
           * ( (  2 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -269,8 +271,10 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            ((%n_9 ≤ 2) ∧ (tt ∧ tt))
-          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
+            (%n_9 ≤ 2)
+          ∧ %l_6
+              -[ %l_6, 16 )->
+              ⟨(8 × %n_9),%a_2⟩^⟨((16 × 1) + (-8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]