diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 50698c2..b671c00 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -22,7 +22,7 @@ jobs:
 
     env:
       OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
-      OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
+      OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
       CPU_CORES: "1"
       DENY_WARNINGS: "1"
       CI_RUNNER: "dummy"
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 83f61bc..66d14b7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -33,7 +33,7 @@ variables:
 build-coq.8.17.0-timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
+    OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
     DENY_WARNINGS: "1"
     # OPAM_PKG: "1"
   only:
@@ -46,7 +46,7 @@ build-coq.8.17.0-timing:
 build-coq.8.17.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
+    OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
     DENY_WARNINGS: "1"
   only:
   - /^ci/@iris/isla-coq
@@ -54,7 +54,7 @@ build-coq.8.17.0:
 trigger-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
+    OPAM_PINS: "coq version 8.17.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  isla-lang git git+https://github.com/rems-project/isla-lang.git"
   except:
   only:
   - triggers
diff --git a/Makefile b/Makefile
index 1d15447..ebc20c9 100644
--- a/Makefile
+++ b/Makefile
@@ -102,7 +102,7 @@ strip_license:
 
 # We cannot use builddep-pins as a dependency of builddep-opamfiles because the CI removes all pins.
 builddep-pins:
-	@opam pin add -n -y isla-lang "git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
+	@opam pin add -n -y isla-lang "git+https://github.com/rems-project/isla-lang.git"
 .PHONY: builddep-pins
 
 builddep-opamfiles: builddep/islaris-builddep.opam
diff --git a/README.md b/README.md
index 0972c3b..632b3df 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@ to point to a working checkout of Isla resp. Isla snapshots.)
 
 The following commits of isla and isla-snapshots are tested:
 ```
-isla: 473f9986832d95b6c4ebb192bb075f2095a92df1
+isla: b8e614bda4a20e42c37d8b216853653133d04322
 isla-snapshots: b58da9170470a422c9396983ac8f87f0a63ba6f8
 ```
 
diff --git a/deps/Makefile b/deps/Makefile
index bd1f45f..f64a580 100644
--- a/deps/Makefile
+++ b/deps/Makefile
@@ -1,5 +1,4 @@
 SAIL_COMMIT=605cd3cffe4b18fb5d0a99beef5d6ee33e1a7dcb
-BBV_COMMIT=6144e214583b72182a4ed89e4328ea62ba766e2e
 
 all: sail-riscv-coq
 .PHONY: all
@@ -7,16 +6,8 @@ all: sail-riscv-coq
 sail-%.tar.gz:
 	wget "https://github.com/rems-project/sail/archive/$*.tar.gz" -O $@
 
-bbv-%.tar.gz:
-	wget "https://github.com/mit-plv/bbv/archive/$*.tar.gz" -O $@
-
-# TODO: maybe add opam install z3?
-bbv: bbv-$(BBV_COMMIT).tar.gz
-	rm -rf coq-bbv
-	tar xf bbv-$(BBV_COMMIT).tar.gz
-	mv "bbv-${BBV_COMMIT}" coq-bbv
-	cp coq-bbv-1.3.opam coq-bbv/opam
-	opam pin add ./coq-bbv -n
+bbv: 
+	opam pin --yes coq-bbv 1.4
 .PHONY: bbv
 
 # TODO: maybe add opam install z3?
diff --git a/etc/aarch64_isla_coq.toml b/etc/aarch64_isla_coq.toml
index 60eee1c..9700cd6 100644
--- a/etc/aarch64_isla_coq.toml
+++ b/etc/aarch64_isla_coq.toml
@@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
 assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
 objdump = "aarch64-linux-gnu-objdump"
 linker = "aarch64-linux-gnu-ld"
+nm = "aarch64-linux-gnu-nm"
 
 [mmu]
 page_table_base = "0x300000"
diff --git a/etc/aarch64_isla_coq_el1.toml b/etc/aarch64_isla_coq_el1.toml
index b5fa739..cbe66dd 100644
--- a/etc/aarch64_isla_coq_el1.toml
+++ b/etc/aarch64_isla_coq_el1.toml
@@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
 assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
 objdump = "aarch64-linux-gnu-objdump"
 linker = "aarch64-linux-gnu-ld"
+nm = "aarch64-linux-gnu-nm"
 
 [mmu]
 page_table_base = "0x300000"
diff --git a/etc/aarch64_isla_coq_pkvm.toml b/etc/aarch64_isla_coq_pkvm.toml
index 9ad4627..a0ed37c 100644
--- a/etc/aarch64_isla_coq_pkvm.toml
+++ b/etc/aarch64_isla_coq_pkvm.toml
@@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
 assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
 objdump = "aarch64-linux-gnu-objdump"
 linker = "aarch64-linux-gnu-ld"
+nm = "aarch64-linux-gnu-nm"
 
 [mmu]
 page_table_base = "0x300000"
diff --git a/etc/riscv64_isla_coq.toml b/etc/riscv64_isla_coq.toml
index 99eb626..14dd9a6 100644
--- a/etc/riscv64_isla_coq.toml
+++ b/etc/riscv64_isla_coq.toml
@@ -11,6 +11,10 @@ write_exclusives = ["Write_RISCV_conditional", "Write_RISCV_conditional_release"
 assembler = "riscv64-linux-gnu-as -march=rv64imac"
 objdump = "riscv64-linux-gnu-objdump"
 linker = "riscv64-linux-gnu-ld"
+nm = "riscv64-linux-gnu-nm"
+
+[const_primops]
+platform_write_mem_ea = false
 
 # Currently not used for RISC-V
 [mmu]
diff --git a/frontend/coq_pp.ml b/frontend/coq_pp.ml
index 8d38b8c..a0e1c40 100644
--- a/frontend/coq_pp.ml
+++ b/frontend/coq_pp.ml
@@ -88,7 +88,7 @@ let pp_lrng ff _ =
 let pp_var_name ff i =
   Format.fprintf ff "%a" pp_Z i
 
-let pp_register_name ff r =
+let pp_sail_name ff r =
   Format.fprintf ff "%S" r
 
 let remove_zeroes digits =
@@ -127,13 +127,13 @@ let pp_bv ff s =
 let pp_accessor ff a =
   let pp fmt = Format.fprintf ff fmt in
   match a with
-  | Ast.Field(r) -> pp "Field %a" pp_register_name r
+  | Ast.Field(r) -> pp "Field %a" pp_sail_name r
 
 let pp_accessor_list ff l =
   pp_list pp_accessor ff (match l with Ast.Nil -> [] | Ast.Cons(l) -> l)
 
 let pp_enum_id ff i =
-  Format.fprintf ff "(Mk_enum_id %i%%nat)" i
+  Format.fprintf ff "\"%s\"" i  
 
 let rec pp_ty ff ty =
   let pp fmt = Format.fprintf ff fmt in
@@ -214,11 +214,11 @@ let pp_manyop ff o =
   | Ast.Concat         -> pp "Concat"
 
 let pp_enum_ctor ff n =
-  Format.fprintf ff "Mk_enum_ctor %i%%nat" n
+  Format.fprintf ff "\"%s\"" n
 
 let pp_enum ff e =
   let pp fmt = Format.fprintf ff fmt in
-  pp "(%a, %a)" pp_enum_id (fst e) pp_enum_ctor (snd e)
+  pp "%a" pp_enum_ctor e
 
 let pp_base_val ff v =
   let pp fmt = Format.fprintf ff fmt in
@@ -236,7 +236,7 @@ let pp_assume_val ff v =
   let pp fmt = Format.fprintf ff fmt in
   match v with
   | Ast.AVal_Var(r,l)  ->
-      pp "AVal_Var %a %a" pp_register_name r pp_accessor_list l
+      pp "AVal_Var %a %a" pp_sail_name r pp_accessor_list l
   | Ast.AVal_Bool(b)      ->
       pp "AVal_Bool %b" b
   | Ast.AVal_Bits(s)      ->
@@ -261,11 +261,11 @@ let rec pp_valu ff v =
       pp "RegVal_List %a" (pp_list pp_valu) l
   | Ast.RegVal_Struct(l)         ->
       let pp_elt ff (r, v) =
-        Format.fprintf ff "(%a, %a)" pp_register_name r pp_valu v
+        Format.fprintf ff "(%a, %a)" pp_sail_name r pp_valu v
       in
       pp "RegVal_Struct %a" (pp_list pp_elt) l
   | Ast.RegVal_Constructor(r, v) ->
-      pp "RegVal_Constructor %a (%a)" pp_register_name r pp_valu v
+      pp "RegVal_Constructor %a (%a)" pp_sail_name r pp_valu v
   | Ast.RegVal_Poison            ->
       pp "RegVal_Poison"
 
@@ -311,8 +311,8 @@ let pp_smt ff e =
       pp "DefineConst %a (%a)" pp_var_name i pp_exp e
   | Ast.Assert(e)          ->
       pp "Assert (%a)" pp_exp e
-  | Ast.DefineEnum(i)      ->
-      pp "DefineEnum %a" pp_Z i
+  | Ast.DefineEnum(name,len,l)      ->
+      pp "DefineEnum %a %a %a" pp_sail_name name pp_Z len (pp_list pp_sail_name) l   
 
 let pp_event ff e =
   let pp fmt = Format.fprintf ff fmt in
@@ -322,10 +322,10 @@ let pp_event ff e =
   | Ast.Branch(i,s,a)              ->
       pp "Branch %a %a %a" pp_Z i pp_str s pp_lrng a
   | Ast.ReadReg(r,l,v,a)           ->
-      pp "ReadReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
+      pp "ReadReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
         pp_valu v pp_lrng a
   | Ast.WriteReg(r,l,v,a)          ->
-      pp "WriteReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
+      pp "WriteReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
         pp_valu v pp_lrng a
   | Ast.ReadMem(v1,v2,v3,i,v,a)    ->
       (* TODO: We remove the kind information since it is quite big and not used.
@@ -362,18 +362,20 @@ let pp_event ff e =
   | Ast.SleepRequest(a)            ->
       pp "SleepRequest %a" pp_lrng a
   | Ast.AssumeReg(r,l,v,a)         ->
-      pp "AssumeReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
+      pp "AssumeReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
         pp_valu v pp_lrng a
   | Ast.Assume(e,a)                ->
       pp "Assume (%a) %a" pp_a_exp e pp_lrng a
   | Ast.FunAssume(r,v,args,a)      ->
-      pp "FunAssume %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
+      pp "FunAssume %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
   | Ast.UseFunAssume(r,v,args,a)   ->
-      pp "UseFunAssume %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
+      pp "UseFunAssume %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
   | Ast.AbstractCall(r,v,args,a)   ->
-      pp "AbstractCall %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
-  | Ast.AbstractPrimop(r,v,args,a)   ->
-      pp "AbstractPrimop %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
+      pp "AbstractCall %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
+  | Ast.AbstractPrimop(r,v,args,a) ->
+      pp "AbstractPrimop %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
+  | Call (_, _)                    -> () (* TODO: fill in here? *)
+  | Return (_, _)                  -> () (* TODO: fill in here? *)
 
 (** [pp_trace_def name] is a pretty-printer for the Coq definition of a trace,
 with given definition name [name]. *)
diff --git a/frontend/decomp.ml b/frontend/decomp.ml
index bde496c..bef7899 100644
--- a/frontend/decomp.ml
+++ b/frontend/decomp.ml
@@ -84,7 +84,7 @@ let event_filter : Arch.t -> int -> event -> bool = fun arch i e ->
   | Smt(Assert(_), _)                                    -> i = 0
   | Cycle(_)
   | MarkReg(_, _, _)
-  | Smt(DefineEnum(_), _)                                -> false
+  | Smt(DefineEnum(_,_,_), _)                            -> true
   | _                                                    -> true
 
 (** [gen_coq arch name isla_f coq_f] processes Isla file [isla_f] and produces
diff --git a/instructions/binary_search_riscv64/a0.v b/instructions/binary_search_riscv64/a0.v
index 20c1fb4..04fdfa4 100644
--- a/instructions/binary_search_riscv64/a0.v
+++ b/instructions/binary_search_riscv64/a0.v
@@ -4,10 +4,10 @@ Definition a0 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffc0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x2" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffc0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a10.v b/instructions/binary_search_riscv64/a10.v
index b609b4c..0abcd68 100644
--- a/instructions/binary_search_riscv64/a10.v
+++ b/instructions/binary_search_riscv64/a10.v
@@ -14,27 +14,27 @@ Definition a10 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x18" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x18" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a10_spec.v b/instructions/binary_search_riscv64/a10_spec.v
index 6170aee..9271643 100644
--- a/instructions/binary_search_riscv64/a10_spec.v
+++ b/instructions/binary_search_riscv64/a10_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a10.
 
 Lemma a10_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a10) ⊢
-  instr_body pc (sd_spec pc "x18" "x2" (32)).
+  instr pc (Some a10)
+  ⊢ instr_body pc (sd_spec pc "x18" "x2" (32)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a14.v b/instructions/binary_search_riscv64/a14.v
index 36a1109..7e2d7b6 100644
--- a/instructions/binary_search_riscv64/a14.v
+++ b/instructions/binary_search_riscv64/a14.v
@@ -14,27 +14,27 @@ Definition a14 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x19" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x19" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a14_spec.v b/instructions/binary_search_riscv64/a14_spec.v
index e5384ba..17135d3 100644
--- a/instructions/binary_search_riscv64/a14_spec.v
+++ b/instructions/binary_search_riscv64/a14_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a14.
 
 Lemma a14_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a14) ⊢
-  instr_body pc (sd_spec pc "x19" "x2" (24)).
+  instr pc (Some a14)
+  ⊢ instr_body pc (sd_spec pc "x19" "x2" (24)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a18.v b/instructions/binary_search_riscv64/a18.v
index b64b45b..6d6f5b6 100644
--- a/instructions/binary_search_riscv64/a18.v
+++ b/instructions/binary_search_riscv64/a18.v
@@ -14,27 +14,27 @@ Definition a18 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x20" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x20" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a18_spec.v b/instructions/binary_search_riscv64/a18_spec.v
index 899bf03..38d23ff 100644
--- a/instructions/binary_search_riscv64/a18_spec.v
+++ b/instructions/binary_search_riscv64/a18_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a18.
 
 Lemma a18_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a18) ⊢
-  instr_body pc (sd_spec pc "x20" "x2" (16)).
+  instr pc (Some a18)
+  ⊢ instr_body pc (sd_spec pc "x20" "x2" (16)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a1c.v b/instructions/binary_search_riscv64/a1c.v
index 58b5a79..47eabdc 100644
--- a/instructions/binary_search_riscv64/a1c.v
+++ b/instructions/binary_search_riscv64/a1c.v
@@ -14,27 +14,27 @@ Definition a1c : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a1c_spec.v b/instructions/binary_search_riscv64/a1c_spec.v
index 5b360e5..8daa593 100644
--- a/instructions/binary_search_riscv64/a1c_spec.v
+++ b/instructions/binary_search_riscv64/a1c_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a1c.
 
 Lemma a1c_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a1c) ⊢
-  instr_body pc (sd_spec pc "x21" "x2" (8)).
+  instr pc (Some a1c)
+  ⊢ instr_body pc (sd_spec pc "x21" "x2" (8)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a20.v b/instructions/binary_search_riscv64/a20.v
index 3220289..028b5e3 100644
--- a/instructions/binary_search_riscv64/a20.v
+++ b/instructions/binary_search_riscv64/a20.v
@@ -5,17 +5,17 @@ Definition a20 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Binop (Eq) (Val (Val_Symbolic 13%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 15%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x54%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Binop (Eq) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x54%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   tcases [
-    Smt (Assert (Val (Val_Symbolic 14%Z) Mk_annot)) Mk_annot :t:
-    Smt (DefineConst 16%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 15%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-    BranchAddress (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
-    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
+    Smt (Assert (Val (Val_Symbolic 3%Z) Mk_annot)) Mk_annot :t:
+    Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+    BranchAddress (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
     tnil;
-    Smt (Assert (Unop (Not) (Val (Val_Symbolic 14%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+    Smt (Assert (Unop (Not) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot)) Mk_annot :t:
     WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
     tnil
   ]
diff --git a/instructions/binary_search_riscv64/a24.v b/instructions/binary_search_riscv64/a24.v
index 126a5da..b50ae32 100644
--- a/instructions/binary_search_riscv64/a24.v
+++ b/instructions/binary_search_riscv64/a24.v
@@ -4,10 +4,10 @@ Definition a24 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x13" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x18" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x13" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x18" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a28.v b/instructions/binary_search_riscv64/a28.v
index 2a223a6..b315c74 100644
--- a/instructions/binary_search_riscv64/a28.v
+++ b/instructions/binary_search_riscv64/a28.v
@@ -4,10 +4,10 @@ Definition a28 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x21" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x21" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a2c.v b/instructions/binary_search_riscv64/a2c.v
index ca4cbca..786cd34 100644
--- a/instructions/binary_search_riscv64/a2c.v
+++ b/instructions/binary_search_riscv64/a2c.v
@@ -4,10 +4,10 @@ Definition a2c : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x19" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x19" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a30.v b/instructions/binary_search_riscv64/a30.v
index de900ec..45339d3 100644
--- a/instructions/binary_search_riscv64/a30.v
+++ b/instructions/binary_search_riscv64/a30.v
@@ -4,10 +4,10 @@ Definition a30 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x20" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x20" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a38.v b/instructions/binary_search_riscv64/a38.v
index 79f4f9f..7e8393d 100644
--- a/instructions/binary_search_riscv64/a38.v
+++ b/instructions/binary_search_riscv64/a38.v
@@ -5,8 +5,8 @@ Definition a38 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xc%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 2%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xc%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a3c.v b/instructions/binary_search_riscv64/a3c.v
index 091bb48..aedb7db 100644
--- a/instructions/binary_search_riscv64/a3c.v
+++ b/instructions/binary_search_riscv64/a3c.v
@@ -4,10 +4,10 @@ Definition a3c : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x21" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x21" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a4.v b/instructions/binary_search_riscv64/a4.v
index d2398c1..8b10427 100644
--- a/instructions/binary_search_riscv64/a4.v
+++ b/instructions/binary_search_riscv64/a4.v
@@ -14,27 +14,27 @@ Definition a4 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x1" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x1" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a40.v b/instructions/binary_search_riscv64/a40.v
index af24397..6f1ec9b 100644
--- a/instructions/binary_search_riscv64/a40.v
+++ b/instructions/binary_search_riscv64/a40.v
@@ -5,19 +5,19 @@ Definition a40 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DeclareConst 14%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
-  Smt (DefineConst 17%Z (Binop ((Bvcomp Bvsge)) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 13%Z) Mk_annot) Mk_annot) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 14%Z) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 18%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Binop ((Bvcomp Bvsge)) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 2%Z) Mk_annot) Mk_annot) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 7%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   tcases [
-    Smt (Assert (Val (Val_Symbolic 17%Z) Mk_annot)) Mk_annot :t:
-    Smt (DefineConst 19%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 18%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-    BranchAddress (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
-    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
+    Smt (Assert (Val (Val_Symbolic 6%Z) Mk_annot)) Mk_annot :t:
+    Smt (DefineConst 8%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 7%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+    BranchAddress (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
+    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
     tnil;
-    Smt (Assert (Unop (Not) (Val (Val_Symbolic 17%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+    Smt (Assert (Unop (Not) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
     WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
     tnil
   ]
diff --git a/instructions/binary_search_riscv64/a44.v b/instructions/binary_search_riscv64/a44.v
index f12591b..c85288f 100644
--- a/instructions/binary_search_riscv64/a44.v
+++ b/instructions/binary_search_riscv64/a44.v
@@ -4,12 +4,12 @@ Definition a44 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t:
-  Smt (DeclareConst 18%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
-  Smt (DefineConst 19%Z (Binop ((Bvarith Bvsub)) (Val (Val_Symbolic 17%Z) Mk_annot) (Val (Val_Symbolic 18%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 19%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Binop ((Bvarith Bvsub)) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a48.v b/instructions/binary_search_riscv64/a48.v
index 291e941..f97ae37 100644
--- a/instructions/binary_search_riscv64/a48.v
+++ b/instructions/binary_search_riscv64/a48.v
@@ -4,10 +4,10 @@ Definition a48 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 10%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 10%Z)) Mk_annot :t:
-  Smt (DefineConst 11%Z (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 10%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 11%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a4_spec.v b/instructions/binary_search_riscv64/a4_spec.v
index 581b63b..0011b25 100644
--- a/instructions/binary_search_riscv64/a4_spec.v
+++ b/instructions/binary_search_riscv64/a4_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a4.
 
 Lemma a4_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a4) ⊢
-  instr_body pc (sd_spec pc "x1" "x2" (56)).
+  instr pc (Some a4)
+  ⊢ instr_body pc (sd_spec pc "x1" "x2" (56)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a4c.v b/instructions/binary_search_riscv64/a4c.v
index 1452045..27dbec1 100644
--- a/instructions/binary_search_riscv64/a4c.v
+++ b/instructions/binary_search_riscv64/a4c.v
@@ -4,12 +4,12 @@ Definition a4c : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t:
-  Smt (DeclareConst 18%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
-  Smt (DefineConst 19%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 17%Z) Mk_annot; Val (Val_Symbolic 18%Z) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x8" [] (RegVal_Base (Val_Symbolic 19%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Symbolic 3%Z) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x8" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a50.v b/instructions/binary_search_riscv64/a50.v
index 82ccfcc..f3d3759 100644
--- a/instructions/binary_search_riscv64/a50.v
+++ b/instructions/binary_search_riscv64/a50.v
@@ -4,10 +4,10 @@ Definition a50 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 10%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 10%Z)) Mk_annot :t:
-  Smt (DefineConst 11%Z (Binop ((Bvarith Bvshl)) (Val (Val_Symbolic 10%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x3%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 11%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Binop ((Bvarith Bvshl)) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x3%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a54.v b/instructions/binary_search_riscv64/a54.v
index 577d112..7bc81da 100644
--- a/instructions/binary_search_riscv64/a54.v
+++ b/instructions/binary_search_riscv64/a54.v
@@ -4,12 +4,12 @@ Definition a54 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t:
-  Smt (DeclareConst 18%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x19" [] (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
-  Smt (DefineConst 19%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 17%Z) Mk_annot; Val (Val_Symbolic 18%Z) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 19%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x19" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Symbolic 3%Z) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a58.v b/instructions/binary_search_riscv64/a58.v
index 109b7dc..56d6693 100644
--- a/instructions/binary_search_riscv64/a58.v
+++ b/instructions/binary_search_riscv64/a58.v
@@ -14,29 +14,27 @@ Definition a58 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x10" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Val (AVal_Var "x10" []) Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Val (AVal_Var "x10" []) Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a5c.v b/instructions/binary_search_riscv64/a5c.v
index f666f99..6ebce73 100644
--- a/instructions/binary_search_riscv64/a5c.v
+++ b/instructions/binary_search_riscv64/a5c.v
@@ -4,10 +4,10 @@ Definition a5c : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x18" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x11" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x18" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x11" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a60.v b/instructions/binary_search_riscv64/a60.v
index 84f243b..eb6c41c 100644
--- a/instructions/binary_search_riscv64/a60.v
+++ b/instructions/binary_search_riscv64/a60.v
@@ -7,9 +7,9 @@ Definition a60 : isla_trace :=
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   Smt (DefineConst 2%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 1%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "x20" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
-  Smt (DefineConst 7%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 8%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 7%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
   WriteReg "x1" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a64.v b/instructions/binary_search_riscv64/a64.v
index 3f16b3e..b78cb23 100644
--- a/instructions/binary_search_riscv64/a64.v
+++ b/instructions/binary_search_riscv64/a64.v
@@ -5,17 +5,17 @@ Definition a64 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Binop (Eq) (Val (Val_Symbolic 13%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 15%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffd8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Binop (Eq) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffd8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   tcases [
-    Smt (Assert (Val (Val_Symbolic 14%Z) Mk_annot)) Mk_annot :t:
-    Smt (DefineConst 16%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 15%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-    BranchAddress (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
-    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
+    Smt (Assert (Val (Val_Symbolic 3%Z) Mk_annot)) Mk_annot :t:
+    Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+    BranchAddress (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
     tnil;
-    Smt (Assert (Unop (Not) (Val (Val_Symbolic 14%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+    Smt (Assert (Unop (Not) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot)) Mk_annot :t:
     WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
     tnil
   ]
diff --git a/instructions/binary_search_riscv64/a68.v b/instructions/binary_search_riscv64/a68.v
index cab25d7..22c8a3a 100644
--- a/instructions/binary_search_riscv64/a68.v
+++ b/instructions/binary_search_riscv64/a68.v
@@ -4,10 +4,10 @@ Definition a68 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x9" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x9" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a6c.v b/instructions/binary_search_riscv64/a6c.v
index efe0f64..9f403c4 100644
--- a/instructions/binary_search_riscv64/a6c.v
+++ b/instructions/binary_search_riscv64/a6c.v
@@ -5,19 +5,19 @@ Definition a6c : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DeclareConst 14%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
-  Smt (DefineConst 17%Z (Binop ((Bvcomp Bvslt)) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 13%Z) Mk_annot) Mk_annot) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 14%Z) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 18%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffd8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x21" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Binop ((Bvcomp Bvslt)) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 2%Z) Mk_annot) Mk_annot) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 7%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffd8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   tcases [
-    Smt (Assert (Val (Val_Symbolic 17%Z) Mk_annot)) Mk_annot :t:
-    Smt (DefineConst 19%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 18%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-    BranchAddress (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
-    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
+    Smt (Assert (Val (Val_Symbolic 6%Z) Mk_annot)) Mk_annot :t:
+    Smt (DefineConst 8%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 7%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+    BranchAddress (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
+    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
     tnil;
-    Smt (Assert (Unop (Not) (Val (Val_Symbolic 17%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+    Smt (Assert (Unop (Not) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
     WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
     tnil
   ]
diff --git a/instructions/binary_search_riscv64/a70.v b/instructions/binary_search_riscv64/a70.v
index 79372ad..c3dd2b5 100644
--- a/instructions/binary_search_riscv64/a70.v
+++ b/instructions/binary_search_riscv64/a70.v
@@ -5,8 +5,8 @@ Definition a70 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 2%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a78.v b/instructions/binary_search_riscv64/a78.v
index 9af909c..ea1d06e 100644
--- a/instructions/binary_search_riscv64/a78.v
+++ b/instructions/binary_search_riscv64/a78.v
@@ -4,10 +4,10 @@ Definition a78 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a7c.v b/instructions/binary_search_riscv64/a7c.v
index d59eb0b..15c2414 100644
--- a/instructions/binary_search_riscv64/a7c.v
+++ b/instructions/binary_search_riscv64/a7c.v
@@ -14,29 +14,27 @@ Definition a7c : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x21" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x21" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a7c_spec.v b/instructions/binary_search_riscv64/a7c_spec.v
index b5c74cf..e972fe5 100644
--- a/instructions/binary_search_riscv64/a7c_spec.v
+++ b/instructions/binary_search_riscv64/a7c_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a7c.
 
 Lemma a7c_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a7c) ⊢
-  instr_body pc (ld_spec pc "x21" "x2" (8)).
+  instr pc (Some a7c)
+  ⊢ instr_body pc (ld_spec pc "x21" "x2" (8)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a8.v b/instructions/binary_search_riscv64/a8.v
index 6715b28..77349f0 100644
--- a/instructions/binary_search_riscv64/a8.v
+++ b/instructions/binary_search_riscv64/a8.v
@@ -14,27 +14,27 @@ Definition a8 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x8" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a80.v b/instructions/binary_search_riscv64/a80.v
index 8d7975b..7e8c4ab 100644
--- a/instructions/binary_search_riscv64/a80.v
+++ b/instructions/binary_search_riscv64/a80.v
@@ -14,29 +14,27 @@ Definition a80 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x20" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x20" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a80_spec.v b/instructions/binary_search_riscv64/a80_spec.v
index e269747..9c9583d 100644
--- a/instructions/binary_search_riscv64/a80_spec.v
+++ b/instructions/binary_search_riscv64/a80_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a80.
 
 Lemma a80_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a80) ⊢
-  instr_body pc (ld_spec pc "x20" "x2" (16)).
+  instr pc (Some a80)
+  ⊢ instr_body pc (ld_spec pc "x20" "x2" (16)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a84.v b/instructions/binary_search_riscv64/a84.v
index 26cf766..0d73268 100644
--- a/instructions/binary_search_riscv64/a84.v
+++ b/instructions/binary_search_riscv64/a84.v
@@ -14,29 +14,27 @@ Definition a84 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x19" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x19" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a84_spec.v b/instructions/binary_search_riscv64/a84_spec.v
index 4845b8f..f25c7d4 100644
--- a/instructions/binary_search_riscv64/a84_spec.v
+++ b/instructions/binary_search_riscv64/a84_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a84.
 
 Lemma a84_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a84) ⊢
-  instr_body pc (ld_spec pc "x19" "x2" (24)).
+  instr pc (Some a84)
+  ⊢ instr_body pc (ld_spec pc "x19" "x2" (24)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a88.v b/instructions/binary_search_riscv64/a88.v
index dd098d7..996bd95 100644
--- a/instructions/binary_search_riscv64/a88.v
+++ b/instructions/binary_search_riscv64/a88.v
@@ -14,29 +14,27 @@ Definition a88 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x18" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x18" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a88_spec.v b/instructions/binary_search_riscv64/a88_spec.v
index 86e7126..a0b5387 100644
--- a/instructions/binary_search_riscv64/a88_spec.v
+++ b/instructions/binary_search_riscv64/a88_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a88.
 
 Lemma a88_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a88) ⊢
-  instr_body pc (ld_spec pc "x18" "x2" (32)).
+  instr pc (Some a88)
+  ⊢ instr_body pc (ld_spec pc "x18" "x2" (32)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a8_spec.v b/instructions/binary_search_riscv64/a8_spec.v
index d1e519f..64b6462 100644
--- a/instructions/binary_search_riscv64/a8_spec.v
+++ b/instructions/binary_search_riscv64/a8_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a8.
 
 Lemma a8_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a8) ⊢
-  instr_body pc (sd_spec pc "x8" "x2" (48)).
+  instr pc (Some a8)
+  ⊢ instr_body pc (sd_spec pc "x8" "x2" (48)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a8c.v b/instructions/binary_search_riscv64/a8c.v
index 7a190da..5c8e682 100644
--- a/instructions/binary_search_riscv64/a8c.v
+++ b/instructions/binary_search_riscv64/a8c.v
@@ -14,29 +14,27 @@ Definition a8c : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x9" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x9" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a8c_spec.v b/instructions/binary_search_riscv64/a8c_spec.v
index e11757b..f4b7500 100644
--- a/instructions/binary_search_riscv64/a8c_spec.v
+++ b/instructions/binary_search_riscv64/a8c_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a8c.
 
 Lemma a8c_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a8c) ⊢
-  instr_body pc (ld_spec pc "x9" "x2" (40)).
+  instr pc (Some a8c)
+  ⊢ instr_body pc (ld_spec pc "x9" "x2" (40)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a90.v b/instructions/binary_search_riscv64/a90.v
index 594bb66..b3ce29e 100644
--- a/instructions/binary_search_riscv64/a90.v
+++ b/instructions/binary_search_riscv64/a90.v
@@ -14,29 +14,27 @@ Definition a90 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x8" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x8" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a90_spec.v b/instructions/binary_search_riscv64/a90_spec.v
index 7c2eb71..d46646c 100644
--- a/instructions/binary_search_riscv64/a90_spec.v
+++ b/instructions/binary_search_riscv64/a90_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a90.
 
 Lemma a90_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a90) ⊢
-  instr_body pc (ld_spec pc "x8" "x2" (48)).
+  instr pc (Some a90)
+  ⊢ instr_body pc (ld_spec pc "x8" "x2" (48)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a94.v b/instructions/binary_search_riscv64/a94.v
index c57c095..348caa8 100644
--- a/instructions/binary_search_riscv64/a94.v
+++ b/instructions/binary_search_riscv64/a94.v
@@ -14,29 +14,27 @@ Definition a94 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 36%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 36%Z)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 57%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 72%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 72%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 8%N None Mk_annot :t:
-  Smt (DeclareConst 73%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 74%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 75%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 72%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x1" [] (RegVal_Base (Val_Symbolic 75%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t:
+  Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x1" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a94_spec.v b/instructions/binary_search_riscv64/a94_spec.v
index baaf40c..880a08a 100644
--- a/instructions/binary_search_riscv64/a94_spec.v
+++ b/instructions/binary_search_riscv64/a94_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a94.
 
 Lemma a94_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a94) ⊢
-  instr_body pc (ld_spec pc "x1" "x2" (56)).
+  instr pc (Some a94)
+  ⊢ instr_body pc (ld_spec pc "x1" "x2" (56)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/binary_search_riscv64/a98.v b/instructions/binary_search_riscv64/a98.v
index f7a1e44..1cd74ab 100644
--- a/instructions/binary_search_riscv64/a98.v
+++ b/instructions/binary_search_riscv64/a98.v
@@ -4,10 +4,10 @@ Definition a98 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x40%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x2" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x40%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/a9c.v b/instructions/binary_search_riscv64/a9c.v
index e9b972b..40e5f0d 100644
--- a/instructions/binary_search_riscv64/a9c.v
+++ b/instructions/binary_search_riscv64/a9c.v
@@ -7,8 +7,8 @@ Definition a9c : isla_trace :=
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   Smt (DefineConst 2%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 1%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "x1" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
-  Smt (DefineConst 7%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 8%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 7%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/aa0.v b/instructions/binary_search_riscv64/aa0.v
index 8a06e67..16ad403 100644
--- a/instructions/binary_search_riscv64/aa0.v
+++ b/instructions/binary_search_riscv64/aa0.v
@@ -4,12 +4,12 @@ Definition aa0 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t:
-  Smt (DeclareConst 18%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 18%Z)) Mk_annot :t:
-  Smt (DefineConst 23%Z (Unop (ZeroExtend 63%N) (Ite (Binop ((Bvcomp Bvslt)) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 17%Z) Mk_annot) Mk_annot) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 18%Z) Mk_annot) Mk_annot) Mk_annot) (Val (Val_Bits (BV 1%N 0x1%Z)) Mk_annot) (Val (Val_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 23%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 8%Z (Unop (ZeroExtend 63%N) (Ite (Binop ((Bvcomp Bvslt)) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 2%Z) Mk_annot) Mk_annot) (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot) Mk_annot) (Val (Val_Bits (BV 1%N 0x1%Z)) Mk_annot) (Val (Val_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/aa4.v b/instructions/binary_search_riscv64/aa4.v
index 96d0f22..2519b5a 100644
--- a/instructions/binary_search_riscv64/aa4.v
+++ b/instructions/binary_search_riscv64/aa4.v
@@ -4,10 +4,10 @@ Definition aa4 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvxor) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvxor) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/aa8.v b/instructions/binary_search_riscv64/aa8.v
index b024698..5f4a78e 100644
--- a/instructions/binary_search_riscv64/aa8.v
+++ b/instructions/binary_search_riscv64/aa8.v
@@ -7,8 +7,8 @@ Definition aa8 : isla_trace :=
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   Smt (DefineConst 2%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 1%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "x1" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
-  Smt (DefineConst 7%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 8%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 7%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/ac.v b/instructions/binary_search_riscv64/ac.v
index 2e0728f..fa56cee 100644
--- a/instructions/binary_search_riscv64/ac.v
+++ b/instructions/binary_search_riscv64/ac.v
@@ -14,27 +14,27 @@ Definition ac : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x9" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/binary_search_riscv64/ac_spec.v b/instructions/binary_search_riscv64/ac_spec.v
index d03d7f2..7519ceb 100644
--- a/instructions/binary_search_riscv64/ac_spec.v
+++ b/instructions/binary_search_riscv64/ac_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.ac.
 
 Lemma ac_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some ac) ⊢
-  instr_body pc (sd_spec pc "x9" "x2" (40)).
+  instr pc (Some ac)
+  ⊢ instr_body pc (sd_spec pc "x9" "x2" (40)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/memcpy_riscv64/a0.v b/instructions/memcpy_riscv64/a0.v
index 5df2fe3..0b7c4d9 100644
--- a/instructions/memcpy_riscv64/a0.v
+++ b/instructions/memcpy_riscv64/a0.v
@@ -5,17 +5,17 @@ Definition a0 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Binop (Eq) (Val (Val_Symbolic 13%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 15%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1c%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Binop (Eq) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1c%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   tcases [
-    Smt (Assert (Val (Val_Symbolic 14%Z) Mk_annot)) Mk_annot :t:
-    Smt (DefineConst 16%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 15%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-    BranchAddress (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
-    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
+    Smt (Assert (Val (Val_Symbolic 3%Z) Mk_annot)) Mk_annot :t:
+    Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+    BranchAddress (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
     tnil;
-    Smt (Assert (Unop (Not) (Val (Val_Symbolic 14%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+    Smt (Assert (Unop (Not) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot)) Mk_annot :t:
     WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
     tnil
   ]
diff --git a/instructions/memcpy_riscv64/a10.v b/instructions/memcpy_riscv64/a10.v
index a8aea62..06ff72f 100644
--- a/instructions/memcpy_riscv64/a10.v
+++ b/instructions/memcpy_riscv64/a10.v
@@ -4,10 +4,10 @@ Definition a10 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/memcpy_riscv64/a14.v b/instructions/memcpy_riscv64/a14.v
index f418a99..5c79b14 100644
--- a/instructions/memcpy_riscv64/a14.v
+++ b/instructions/memcpy_riscv64/a14.v
@@ -4,10 +4,10 @@ Definition a14 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x11" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x11" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/memcpy_riscv64/a18.v b/instructions/memcpy_riscv64/a18.v
index 2dacab3..212230a 100644
--- a/instructions/memcpy_riscv64/a18.v
+++ b/instructions/memcpy_riscv64/a18.v
@@ -5,17 +5,17 @@ Definition a18 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 1%N 1%N) (AExp_Val (AVal_Var "PC" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Unop (Not) (Binop (Eq) (Val (Val_Symbolic 13%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 15%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffec%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Unop (Not) (Binop (Eq) (Val (Val_Symbolic 2%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffec%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   tcases [
-    Smt (Assert (Val (Val_Symbolic 14%Z) Mk_annot)) Mk_annot :t:
-    Smt (DefineConst 16%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 15%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-    BranchAddress (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
-    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 15%Z)) Mk_annot :t:
+    Smt (Assert (Val (Val_Symbolic 3%Z) Mk_annot)) Mk_annot :t:
+    Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+    BranchAddress (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+    WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
     tnil;
-    Smt (Assert (Unop (Not) (Val (Val_Symbolic 14%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+    Smt (Assert (Unop (Not) (Val (Val_Symbolic 3%Z) Mk_annot) Mk_annot)) Mk_annot :t:
     WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
     tnil
   ]
diff --git a/instructions/memcpy_riscv64/a1c.v b/instructions/memcpy_riscv64/a1c.v
index 950591d..01a5eed 100644
--- a/instructions/memcpy_riscv64/a1c.v
+++ b/instructions/memcpy_riscv64/a1c.v
@@ -7,8 +7,8 @@ Definition a1c : isla_trace :=
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   Smt (DefineConst 2%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 1%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "x1" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
-  Smt (DefineConst 7%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 8%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 7%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Manyop (Bvmanyarith Bvor) [Manyop (Bvmanyarith Bvand) [Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffffe%Z)) Mk_annot] Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Unop (Extract 0%N 0%N) (Binop ((Bvarith Bvlshr)) (Val (Val_Symbolic 4%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/memcpy_riscv64/a4.v b/instructions/memcpy_riscv64/a4.v
index b48822e..1634c13 100644
--- a/instructions/memcpy_riscv64/a4.v
+++ b/instructions/memcpy_riscv64/a4.v
@@ -14,28 +14,26 @@ Definition a4 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Val (AVal_Var "x11" []) Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Val (AVal_Var "x11" []) Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 22%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 30%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t:
-  Smt (DefineConst 45%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 51%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 22%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 66%Z (Ty_BitVec 8%N)) Mk_annot :t:
-  ReadMem (RegVal_Base (Val_Symbolic 66%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 22%Z)) 1%N None Mk_annot :t:
-  Smt (DeclareConst 67%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DeclareConst 68%Z (Ty_BitVec 32%N)) Mk_annot :t:
-  Smt (DefineConst 69%Z (Unop (SignExtend 56%N) (Val (Val_Symbolic 66%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  WriteReg "x13" [] (RegVal_Base (Val_Symbolic 69%Z)) Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 14%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DefineConst 21%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 31%Z (Ty_BitVec 8%N)) Mk_annot :t:
+  ReadMem (RegVal_Base (Val_Symbolic 31%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 1%N None Mk_annot :t:
+  Smt (DefineConst 32%Z (Unop (SignExtend 56%N) (Val (Val_Symbolic 31%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  WriteReg "x13" [] (RegVal_Base (Val_Symbolic 32%Z)) Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/memcpy_riscv64/a8.v b/instructions/memcpy_riscv64/a8.v
index bc042cc..fe866c4 100644
--- a/instructions/memcpy_riscv64/a8.v
+++ b/instructions/memcpy_riscv64/a8.v
@@ -14,27 +14,27 @@ Definition a8 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Val (AVal_Var "x10" []) Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Val (AVal_Var "x10" []) Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x10" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 29%Z)) Mk_annot :t:
-  Smt (DeclareConst 47%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x13" [] (RegVal_Base (Val_Symbolic 47%Z)) Mk_annot :t:
-  Smt (DefineConst 50%Z (Unop (Extract 7%N 0%N) (Val (Val_Symbolic 47%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 56%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 62%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 66%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 66%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 50%Z)) 1%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 14%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 19%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x13" [] (RegVal_Base (Val_Symbolic 19%Z)) Mk_annot :t:
+  Smt (DefineConst 20%Z (Unop (Extract 7%N 0%N) (Val (Val_Symbolic 19%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 23%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 29%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 33%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 33%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 20%Z)) 1%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/memcpy_riscv64/ac.v b/instructions/memcpy_riscv64/ac.v
index 8808ca9..6d9e6ea 100644
--- a/instructions/memcpy_riscv64/ac.v
+++ b/instructions/memcpy_riscv64/ac.v
@@ -4,10 +4,10 @@ Definition ac : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffff%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x12" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x12" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffff%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x12" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/riscv64_test/a8.v b/instructions/riscv64_test/a8.v
index 88530f5..c9101ab 100644
--- a/instructions/riscv64_test/a8.v
+++ b/instructions/riscv64_test/a8.v
@@ -14,27 +14,27 @@ Definition a8 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x11" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .
diff --git a/instructions/riscv64_test/a8_spec.v b/instructions/riscv64_test/a8_spec.v
index 55564a0..521f7a5 100644
--- a/instructions/riscv64_test/a8_spec.v
+++ b/instructions/riscv64_test/a8_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.riscv64_test.a8.
 
 Lemma a8_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a8) ⊢
-  instr_body pc (sd_spec pc "x11" "x2" (8)).
+  instr pc (Some a8)
+  ⊢ instr_body pc (sd_spec pc "x11" "x2" (8)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/instructions/riscv64_test/ac.v b/instructions/riscv64_test/ac.v
index 68e69a0..b1b1d48 100644
--- a/instructions/riscv64_test/ac.v
+++ b/instructions/riscv64_test/ac.v
@@ -14,7 +14,7 @@ Definition ac : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 2%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
diff --git a/instructions/riscv64_test/ac_spec.v b/instructions/riscv64_test/ac_spec.v
index 85d9e90..b837838 100644
--- a/instructions/riscv64_test/ac_spec.v
+++ b/instructions/riscv64_test/ac_spec.v
@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.riscv64_test.ac.
 
 Lemma ac_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some ac) ⊢
-  instr_body pc (ld_spec pc "x11" "x2" (8)).
+  instr pc (Some ac)
+  ⊢ instr_body pc (ld_spec pc "x11" "x2" (8)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.
diff --git a/sail-riscv/sail_opsem.v b/sail-riscv/sail_opsem.v
index 744f2f2..ceb7c6a 100644
--- a/sail-riscv/sail_opsem.v
+++ b/sail-riscv/sail_opsem.v
@@ -417,7 +417,7 @@ Definition register_value_to_valu (v : register_value) : valu :=
   | Regval_bool b => RVal_Bool b
   | Regval_Misa m => RegVal_Struct [("bits", RVal_Bits (mword_to_bv (n2:=64) m.(Misa_bits)))]
   | Regval_Mstatus m => RegVal_Struct [("bits", RVal_Bits (mword_to_bv (n2:=64) m.(Mstatus_bits)))]
-  | Regval_Privilege p => RVal_Enum (Mk_enum_id 3, Mk_enum_ctor (match p with | User => 0 | Supervisor => 1 | Machine => 2 end))
+  | Regval_Privilege p => RVal_Enum (match p with | User => "User" | Supervisor => "Supervisor" | Machine => "Machine" end)
   | _ => RegVal_Poison
   end.
 
@@ -609,7 +609,7 @@ Proof.
     destruct (isla_regs !! "PC") eqn: HPC.
     - have [? [[<-] ->]]:= Hregs "PC" _ ltac:(done). done.
     - move: Hsafe => [[]|]// [?[?[?[? Hsafe]]]]. inv_seq_step.
-      revert select (∃ x, _) => -[?[??]]; unfold register_name in *; simplify_eq.
+      revert select (∃ x, _) => -[?[??]]; unfold sail_name in *; simplify_eq.
   }
   destruct (sail_instrs !! mword_to_bv (PC sail_regs)) as [si|] eqn: Hsi.
   - move: (Hsi) => /(elem_of_dom_2 _ _ _). rewrite -Hdom. move => /elem_of_dom[ii Hii]. clear Hdom.
@@ -978,7 +978,7 @@ Proof.
 Qed.
 
 Lemma sim_DeclareConstEnum A E Σ K e1 e2 ann x id c:
-  sim (A:=A) (E:=E) Σ e1 K (subst_trace (Val_Enum (id, c)) x e2) →
+  sim (A:=A) (E:=E) Σ e1 K (subst_trace (Val_Enum c) x e2) →
   sim (A:=A) (E:=E) Σ e1 K (Smt (DeclareConst x (Ty_Enum id)) ann :t: e2).
 Proof.
   move => Hsim ????????.
diff --git a/sail-riscv/tactics.v b/sail-riscv/tactics.v
index e05ce33..4b3b803 100644
--- a/sail-riscv/tactics.v
+++ b/sail-riscv/tactics.v
@@ -161,7 +161,6 @@ Ltac sim_simpl_goal :=
          | |- Val_Enum ?a = Val_Enum ?b => apply f_equal_help; [done|]
          | |- RegVal_Base ?a = RegVal_Base ?b => apply f_equal_help; [done|]
          | |- RegVal_Struct ?a = RegVal_Struct ?b => apply f_equal_help; [done|]
-         | |- Mk_enum_id ?a = Mk_enum_id ?b => apply f_equal_help; [done|]
          | |- (?a1, ?a2) = (?b1, ?b2) => apply f_equal_help; [apply f_equal_help; [done|] |]
          | |- _::_ = _::_ => apply f_equal_help; [apply f_equal_help; [done|] |]
          end;
diff --git a/theories/aarch64/sys_regs.v b/theories/aarch64/sys_regs.v
index 778854a..72e9966 100644
--- a/theories/aarch64/sys_regs.v
+++ b/theories/aarch64/sys_regs.v
@@ -108,7 +108,7 @@ Definition sys_regs_map : reg_map :=
     ("IT", RegVal_Poison); ("IL", RegVal_Poison);
     ("Z", RVal_Bits (BV 1 0)); ("BTYPE", RegVal_Poison);
     ("SSBS", RegVal_Poison); ("T", RegVal_Poison); ("J", RegVal_Poison);
-     ("V", RVal_Bits (BV 1 0)); ("DIT", RegVal_Poison)]) ]> $
+    ("V", RVal_Bits (BV 1 0)); ("DIT", RegVal_Poison)]) ]> $
   <[ "SCTLR_EL1" := RVal_Bits (BV 64 0x0000000004000002) ]> $
   <[ "SCTLR_EL2" := RVal_Bits (BV 64 0x0000000004000002) ]> $
   <[ "SCR_EL3" := RVal_Bits (BV 32 0x00000501) ]> $
diff --git a/theories/automation.v b/theories/automation.v
index 075fdbc..0c43fa7 100644
--- a/theories/automation.v
+++ b/theories/automation.v
@@ -424,9 +424,7 @@ Ltac is_fully_reduced_valu v :=
       ]
       | Val_Enum ?e => first [ is_var_no_let e |
         lazymatch e with
-        | (Mk_enum_id ?e1, Mk_enum_ctor ?e2) =>
-            first [ is_var_no_let e1 | lazymatch isnatcst e1 with | true => idtac end ];
-            first [ is_var_no_let e2 | lazymatch isnatcst e2 with | true => idtac end ]
+        | _ => is_var_no_let e
         end
       ]
       end
@@ -449,7 +447,7 @@ Goal ∀ (v : valu) (b : base_val) (b1 : bool) (b2 : bv 64) (z : Z) Heq,
   is_fully_reduced_valu (RVal_Bits (@BV 64 z Heq)).
   is_fully_reduced_valu (RVal_Bits (BV 64 100)).
   assert_fails (is_fully_reduced_valu (RVal_Bits x)).
-  is_fully_reduced_valu (RVal_Enum (Mk_enum_id 1, Mk_enum_ctor 4)).
+  (* is_fully_reduced_valu (RVal_Enum "Machine"). *)
 Abort.
 
 Ltac remember_regcol :=
@@ -1407,7 +1405,7 @@ Section instances.
   Proof. iApply wp_declare_const_bool. Qed.
 
   Lemma li_wp_declare_const_enum v es i ann:
-    (∀ c, WPasm (subst_trace (Val_Enum (i, c)) v es))
+    (∀ c, WPasm (subst_trace (Val_Enum c) v es))
     ⊢ WPasm (Smt (DeclareConst v (Ty_Enum i)) ann :t: es).
   Proof. iApply wp_declare_const_enum. Qed.
 
diff --git a/theories/lifting.v b/theories/lifting.v
index fd583ad..606b797 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -61,7 +61,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class Arch := {
-  arch_pc_reg : register_name;
+  arch_pc_reg : sail_name;
 }.
 
 Class islaG Σ := IslaG {
@@ -98,11 +98,11 @@ Definition wp_asm_eq `{!Arch} `{!islaG Σ} `{!threadG} : wp_asm = @wp_asm_def _
 Notation WPasm := wp_asm.
 
 Definition wpreadreg_def `{!islaG Σ} `{!threadG}
-     (r : register_name) (al : accessor_list) (G : valu → iProp Σ) : iProp Σ :=
+     (r : sail_name) (al : accessor_list) (G : valu → iProp Σ) : iProp Σ :=
   ∀ regs, regs_ctx regs -∗
     ∃ v v', ⌜regs !! r = Some v⌝ ∗ ⌜read_accessor al v = Some v'⌝ ∗ regs_ctx regs ∗ G v'.
 Definition wpreadreg_aux `{!islaG Σ} `{!threadG} : seal (@wpreadreg_def _ _ _). by eexists. Qed.
-Definition wpreadreg `{!islaG Σ} `{!threadG} : register_name → accessor_list → (valu → iProp Σ) → iProp Σ := (wpreadreg_aux).(unseal).
+Definition wpreadreg `{!islaG Σ} `{!threadG} : sail_name → accessor_list → (valu → iProp Σ) → iProp Σ := (wpreadreg_aux).(unseal).
 Definition wpreadreg_eq `{!islaG Σ} `{!threadG} : wpreadreg = @wpreadreg_def _ _ _ := (wpreadreg_aux).(seal_eq).
 Notation "'WPreadreg' r '@' al {{ G } }" := (wpreadreg r al G%I)
   (at level 20, r, al, G at level 200, only parsing) : bi_scope.
@@ -270,7 +270,7 @@ Section lifting.
     }
     iIntros "!>" (????) "_". iMod "HE" as "_". iModIntro.
     inv_seq_step.
-    revert select (∃ _, _) => -[?[?]]; unfold register_name in *; simplify_option_eq.
+    revert select (∃ _, _) => -[?[?]]; unfold sail_name in *; simplify_option_eq.
     move => [-> [? ->]].
     iFrame. iSplitL; [|done].
     iApply ("Hcont" with "HPC"); [done|done|done|].
@@ -297,7 +297,7 @@ Section lifting.
     }
     iIntros "!>" (????) "_". iMod "HE" as "_".
     inv_seq_step.
-    revert select (∃ _, _) => -[?[?]]. unfold register_name in *; simplify_option_eq.
+    revert select (∃ _, _) => -[?[?]]. unfold sail_name in *; simplify_option_eq.
     move => [-> ->].
     iMod (spec_ctx_cons with "Hsctx Hspec") as "[??]"; [done|]. iModIntro.
     iFrame. iSplitL; [|done].
@@ -479,7 +479,7 @@ Section lifting.
     iIntros "!>" (????) "_". iMod "HE" as "_". iModIntro.
     inv_seq_step.
     revert select (∃ _, _) => -[?[?[?[?[?[?[?[??]]]]]]]].
-    unfold register_name in *. simplify_eq.
+    unfold sail_name in *. simplify_eq.
     iFrame; iSplitL; [|done].
     iMod (reg_mapsto_update with "Hθ Hr") as "[Hθ Hr]".
     iApply ("Hcont" with "Hr"); [done..|].
@@ -505,7 +505,7 @@ Section lifting.
     iIntros "!>" (????) "_". iMod "HE" as "_". iModIntro.
     inv_seq_step.
     revert select (∃ _, _) => -[?[?[?[?[?[?[?[??]]]]]]]].
-    unfold register_name, write_accessor in *. simplify_option_eq.
+    unfold sail_name, write_accessor in *. simplify_option_eq.
     iFrame; iSplitL; [|done].
     iMod (struct_reg_mapsto_update with "Hθ Hr") as "[Hθ Hr]"; [done..|].
     iApply ("Hcont" with "Hr"); [done..|].
@@ -749,7 +749,7 @@ Section lifting.
   Qed.
 
   Lemma wp_declare_const_enum v es i ann:
-    (∀ c, WPasm (subst_trace (Val_Enum (i, c)) v es)) -∗
+    (∀ c, WPasm (subst_trace (Val_Enum (c)) v es)) -∗
     WPasm (Smt (DeclareConst v (Ty_Enum i)) ann :t: es).
   Proof.
     iIntros "Hcont". setoid_rewrite wp_asm_unfold.
diff --git a/theories/opsem.v b/theories/opsem.v
index 5484e2f..46c10a6 100644
--- a/theories/opsem.v
+++ b/theories/opsem.v
@@ -99,13 +99,6 @@ Definition parametric_trace (v : base_val) (t : isla_trace) : isla_trace :=
 Arguments parametric_trace : simpl never.
 
 Global Instance valu_inhabited : Inhabited valu := populate (RVal_Bool true).
-Global Instance enum_id_eq_decision : EqDecision enum_id.
-Proof. solve_decision. Qed.
-Global Instance enum_ctor_eq_decision : EqDecision enum_ctor.
-Proof. solve_decision. Qed.
-Global Instance enum_eq_decision : EqDecision enum.
-Proof. solve_decision. Qed.
-
 
 Definition ite {A} (b : bool) (x y : A) : A :=
   if b then x else y.
@@ -381,8 +374,8 @@ Fixpoint eval_a_exp (regs : reg_map) (e : a_exp) : option base_val :=
   end.
 
 Inductive trace_label : Set :=
-| LReadReg (r : register_name) (al : accessor_list) (v : valu)
-| LWriteReg (r : register_name) (al : accessor_list) (v : valu)
+| LReadReg (r : sail_name) (al : accessor_list) (v : valu)
+| LWriteReg (r : sail_name) (al : accessor_list) (v : valu)
 | LReadMem (data : valu) (kind : valu) (addr : valu) (len : N) (tag : tag_value)
 | LWriteMem (res : valu) (kind : valu) (addr : valu) (data : valu) (len : N) (tag : tag_value)
 | LBranchAddress (v : valu)
@@ -390,7 +383,7 @@ Inductive trace_label : Set :=
 | LDone (next : isla_trace)
 | LAssert (b : bool)
 | LAssume (b : bool)
-| LAssumeReg (r : register_name) (al : accessor_list) (v : valu)
+| LAssumeReg (r : sail_name) (al : accessor_list) (v : valu)
 .
 
 Inductive trace_step : isla_trace → reg_map → option trace_label → isla_trace → Prop :=
@@ -399,7 +392,7 @@ Inductive trace_step : isla_trace → reg_map → option trace_label → isla_tr
 | DeclareConstBoolS x ann es b regs:
     trace_step (Smt (DeclareConst x Ty_Bool) ann :t: es) regs None (subst_trace (Val_Bool b) x es)
 | DeclareConstEnumS x ann es regs i c:
-    trace_step (Smt (DeclareConst x (Ty_Enum i)) ann :t: es) regs None (subst_trace (Val_Enum (i, c)) x es)
+    trace_step (Smt (DeclareConst x (Ty_Enum i)) ann :t: es) regs None (subst_trace (Val_Enum (c)) x es)
 | DefineConstS x e v ann es regs:
     eval_exp e = Some v ->
     trace_step (Smt (DefineConst x e) ann :t: es) regs None (subst_trace v x es)
@@ -447,7 +440,7 @@ Global Instance eta_seq_global_state : Settable _ := settable! Build_seq_global_
 Record seq_local_state := {
   seq_trace    : isla_trace;
   seq_regs     : reg_map;
-  seq_pc_reg   : register_name;
+  seq_pc_reg   : sail_name;
   seq_nb_state : bool;
 }.
 Global Instance eta_seq_local_state : Settable _ := settable! Build_seq_local_state <seq_trace; seq_regs; seq_pc_reg ;seq_nb_state>.
@@ -574,7 +567,7 @@ Inductive seq_step : seq_local_state → seq_global_state → list seq_label →
 Record seq_val := {
   seq_val_trace  : isla_trace;
   seq_val_regs   : reg_map;
-  seq_val_pc_reg : register_name;
+  seq_val_pc_reg : sail_name;
 }.
 Definition seq_of_val (v : seq_val) : seq_local_state := {|
   seq_trace := v.(seq_val_trace);
diff --git a/theories/riscv64/sys_regs.v b/theories/riscv64/sys_regs.v
index 1a2fe3d..e5157f8 100644
--- a/theories/riscv64/sys_regs.v
+++ b/theories/riscv64/sys_regs.v
@@ -72,9 +72,9 @@ Definition sys_regs : list (reg_kind * valu_shape) := [
   (KindReg "rv_clint_base" , ExactShape (RVal_Bits (BV 64 0x0000000002000000)));
   (KindReg "rv_clint_size" , ExactShape (RVal_Bits (BV 64 0x00000000000c0000)));
   (KindReg "rv_htif_tohost" , ExactShape (RVal_Bits (BV 64 0x0000000040001000)));
-  (KindReg "cur_privilege" , ExactShape (RVal_Enum (Mk_enum_id 3, Mk_enum_ctor 2)));
+  (KindReg "cur_privilege" , ExactShape (RVal_Enum "Machine"));
   (* TODO: remove this *)
-  (KindReg "Machine" , ExactShape (RVal_Enum (Mk_enum_id 3, Mk_enum_ctor 2)));
+  (KindReg "Machine" , ExactShape (RVal_Enum "Machine"));
   (KindReg "misa" , ExactShape (RegVal_Struct [("bits", RVal_Bits misa_bits)]));
   (* MPRV disabled *)
   (KindReg "mstatus" , StructShape [("bits", MaskShape 64 0x20000 0)]);
@@ -91,8 +91,8 @@ Definition sys_regs_map (mstatus_bits satp : bv 64) : reg_map :=
   <[ "rv_clint_base" := RVal_Bits (BV 64 0x0000000002000000) ]> $
   <[ "rv_clint_size" := RVal_Bits (BV 64 0x00000000000c0000) ]> $
   <[ "rv_htif_tohost" := RVal_Bits (BV 64 0x0000000040001000) ]> $
-  <[ "cur_privilege" := RVal_Enum (Mk_enum_id 3, Mk_enum_ctor 2) ]> $
-  <[ "Machine" := RVal_Enum (Mk_enum_id 3, Mk_enum_ctor 2) ]> $
+  <[ "cur_privilege" := RVal_Enum "Machine" ]> $
+  <[ "Machine" := RVal_Enum "Machine" ]> $
   <[ "misa" := RegVal_Struct [("bits", RVal_Bits misa_bits)] ]> $
   <[ "mstatus" := RegVal_Struct [("bits", RVal_Bits mstatus_bits)] ]> $
   <[ "satp" := RVal_Bits satp ]> $