use "uXX" for unit type constraint

yongweiy · May 13, 2024 · 4fd8789 · 4fd8789
1 parent 75e3ec9
commit 4fd8789
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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.