From 4fd8789e4b064c0d3861ede298f0b89cd0dfc642 Mon Sep 17 00:00:00 2001
From: Yongwei Yuan <yuan311@purdue.edu>
Date: Sun, 4 Feb 2024 21:34:42 -0500
Subject: [PATCH] use "uXX" for unit type constraint

---
 srlexec/literal.ml | 2 +-
 srlexec/symexec.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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.