diff --git a/srlexec/literal.ml b/srlexec/literal.ml
index ff73c41..f9f1638 100644
--- a/srlexec/literal.ml
+++ b/srlexec/literal.ml
@@ -188,7 +188,7 @@ let refine (rctx, { events; op_filter }) =
           in
           let rctx =
             RTypectx.new_to_right rctx
-            @@ ((Rename.unique "a") #:: (mk_unit_rty_from_prop phi))
+            @@ ((Rename.unique "u") #:: (mk_unit_rty_from_prop phi))
           in
           (* Pp.printf "rctx:\n%s\n" @@ RTypectx.layout_typed_l rctx; *)
           Right (rctx, of_sevent ~ghosts:[] @@ EffEvent ev))
diff --git a/srlexec/symexec.ml b/srlexec/symexec.ml
index 541c5ef..6855e04 100644
--- a/srlexec/symexec.ml
+++ b/srlexec/symexec.ml
@@ -82,7 +82,7 @@ let add_prop_to_rctx phi rctx =
         rctx []
   | None ->
       RTypectx.new_to_right rctx
-      @@ ((Rename.unique "a") #:: (mk_unit_rty_from_prop phi))
+      @@ ((Rename.unique "u") #:: (mk_unit_rty_from_prop phi))
 
 (** Eagerly prune away infeasible branch, otherwise it may make the
     current trace infeasible.