diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 67dc6f02a..758ae74c9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -19,7 +19,7 @@ concurrency:
 
 env:
   OBOL_REPO: soteria-tools/obol
-  OBOL_COMMIT_HASH: 3dbf5acb55ede0c2efe8648cd07e06d4830a12f4
+  OBOL_COMMIT_HASH: bf524f4242a874d716ab3964dd344cda833ba3f8
 
 jobs:
   build:
diff --git a/soteria-rust.opam b/soteria-rust.opam
index c830e9bc7..8699bc9db 100644
--- a/soteria-rust.opam
+++ b/soteria-rust.opam
@@ -52,6 +52,6 @@ build: [
 ]
 dev-repo: "git+https://github.com/soteria-tools/soteria.git"
 pin-depends: [
-  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
-  ["charon.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
+  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
+  ["charon.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
 ]
diff --git a/soteria-rust.opam.template b/soteria-rust.opam.template
index bcadd71aa..bab48f369 100644
--- a/soteria-rust.opam.template
+++ b/soteria-rust.opam.template
@@ -1,4 +1,4 @@
 pin-depends: [
-  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
-  ["charon.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
+  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
+  ["charon.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
 ]
diff --git a/soteria-rust/lib/builtins/intrinsics_impl.ml b/soteria-rust/lib/builtins/intrinsics_impl.ml
index cf93d51fb..47dce840f 100644
--- a/soteria-rust/lib/builtins/intrinsics_impl.ml
+++ b/soteria-rust/lib/builtins/intrinsics_impl.ml
@@ -615,9 +615,9 @@ module M (Rust_state_m : Rust_state_m.S) :
       (layout.size, layout.align)
     else
       match (t, meta) with
-      | TAdt { id = TBuiltin (TSlice | TStr); _ }, (Thin | VTable _) ->
+      | (TSlice _ | TAdt { id = TBuiltin TStr; _ }), (Thin | VTable _) ->
           failwith "size_and_align_of_val: Invalid metadata for slice type"
-      | TAdt { id = TBuiltin (TSlice | TStr); _ }, Len meta ->
+      | (TSlice _ | TAdt { id = TBuiltin TStr; _ }), Len meta ->
           let sub_ty = Layout.dst_slice_ty t in
           let* sub_ty =
             of_opt_not_impl "size_of_val: missing a DST slice type" sub_ty
diff --git a/soteria-rust/lib/builtins/rusteria.ml b/soteria-rust/lib/builtins/rusteria.ml
index 766addb3d..5dfe35d58 100644
--- a/soteria-rust/lib/builtins/rusteria.ml
+++ b/soteria-rust/lib/builtins/rusteria.ml
@@ -48,8 +48,7 @@ module M (Rust_state_m : Rust_state_m.S) = struct
     let+ () = assume [ Typed.BitVec.to_bool to_assume ] in
     unit_
 
-  let nondet (fun_sig : Charon.UllbcAst.fun_sig) _ =
-    Layout.nondet fun_sig.output
+  let nondet (fun_sig : Charon.Types.fun_sig) _ = Layout.nondet fun_sig.output
 
   let panic ?msg args =
     let* msg =
diff --git a/soteria-rust/lib/charon_util.ml b/soteria-rust/lib/charon_util.ml
index dfa8f0991..89b748f12 100644
--- a/soteria-rust/lib/charon_util.ml
+++ b/soteria-rust/lib/charon_util.ml
@@ -39,17 +39,10 @@ let rec pp_ty fmt : Types.ty -> unit = function
   | TAdt { id = TBuiltin TBox; generics = { types = [ ty ]; _ } } ->
       Fmt.pf fmt "Box<%a>" pp_ty ty
   | TAdt { id = TBuiltin TBox; _ } -> Fmt.string fmt "Box<?>"
-  | TAdt
-      {
-        id = TBuiltin TArray;
-        generics =
-          { types = [ ty ]; const_generics = [ CgValue (VScalar len) ]; _ };
-      } ->
+  | TArray (ty, CgValue (VScalar len)) ->
       Fmt.pf fmt "[%a; %a]" pp_ty ty Z.pp_print (z_of_scalar len)
-  | TAdt { id = TBuiltin TArray; _ } -> Fmt.string fmt "[?; ?]"
-  | TAdt { id = TBuiltin TSlice; generics = { types = [ ty ]; _ } } ->
-      Fmt.pf fmt "[%a]" pp_ty ty
-  | TAdt { id = TBuiltin TSlice; _ } -> Fmt.string fmt "[?]"
+  | TArray (ty, _) -> Fmt.pf fmt "[%a; ?]" pp_ty ty
+  | TSlice ty -> Fmt.pf fmt "[%a]" pp_ty ty
   | TAdt { id = TBuiltin TStr; _ } -> Fmt.string fmt "str"
   | TLiteral lit -> pp_literal_ty fmt lit
   | TNever -> Fmt.string fmt "!"
@@ -57,8 +50,11 @@ let rec pp_ty fmt : Types.ty -> unit = function
   | TRef (_, ty, RShared) -> Fmt.pf fmt "&%a" pp_ty ty
   | TRawPtr (ty, RMut) -> Fmt.pf fmt "*mut %a" pp_ty ty
   | TRawPtr (ty, RShared) -> Fmt.pf fmt "*const %a" pp_ty ty
-  | TFnPtr { binder_value = ins, out; _ } ->
-      Fmt.pf fmt "fn (%a) -> %a" Fmt.(list ~sep:(any ", ") pp_ty) ins pp_ty out
+  | TFnPtr { binder_value = { inputs; output; is_unsafe }; _ } ->
+      Fmt.pf fmt "%sfn (%a) -> %a"
+        (if is_unsafe then "unsafe " else "")
+        Fmt.(list ~sep:(any ", ") pp_ty)
+        inputs pp_ty output
   | TDynTrait _ -> Fmt.string fmt "dyn <trait>"
   | TTraitType (_, name) -> Fmt.pf fmt "Trait<?>::%s" name
   | TFnDef { binder_value = { kind = FunId (FRegular fid); _ }; _ } ->
@@ -116,17 +112,7 @@ let fields_of_tys : Types.ty list -> Types.field list =
       })
 
 let mk_array_ty ty len : Types.ty =
-  TAdt
-    {
-      id = TBuiltin TArray;
-      generics =
-        {
-          types = [ ty ];
-          const_generics = [ CgValue (VScalar (UnsignedScalar (Usize, len))) ];
-          regions = [];
-          trait_refs = [];
-        };
-    }
+  TArray (ty, CgValue (VScalar (UnsignedScalar (Usize, len))))
 
 (** The type [*const ()] *)
 let unit_ptr = Types.TRawPtr (TypesUtils.mk_unit_ty, RShared)
@@ -172,6 +158,7 @@ let pp_span_data ft ({ file; beg_loc; end_loc } : Meta.span_data) =
     match name with
     | Local name -> Fmt.string ft (clean_filename name)
     | Virtual name -> Fmt.pf ft "%s (virtual)" (clean_filename name)
+    | NotReal name -> Fmt.pf ft "%s (synthetic)" (clean_filename name)
   in
   let pp_range ft ((start, stop) : Meta.loc * Meta.loc) =
     if start.line = stop.line then
diff --git a/soteria-rust/lib/crate.ml b/soteria-rust/lib/crate.ml
index bc7ebf951..c0cf7d12a 100644
--- a/soteria-rust/lib/crate.ml
+++ b/soteria-rust/lib/crate.ml
@@ -29,14 +29,15 @@ let[@inline] mk_pp_indent to_string =
   let to_str = to_string (as_fmt_env ()) "" in
   Fmt.pf ft "%s" (to_str v)
 
-let pp_name = mk_pp PrintTypes.name_to_string
-let pp_statement = mk_pp_indent PrintUllbcAst.Ast.statement_to_string
-let pp_terminator = mk_pp_indent PrintUllbcAst.Ast.terminator_to_string
+let pp_constant_expr = mk_pp PrintExpressions.constant_expr_to_string
 let pp_fn_operand = mk_pp PrintUllbcAst.Ast.fn_operand_to_string
 let pp_fun_decl_ref = mk_pp PrintTypes.fun_decl_ref_to_string
 let pp_generic_args = mk_pp PrintTypes.generic_args_to_string
 let pp_global_decl_ref = mk_pp PrintTypes.global_decl_ref_to_string
+let pp_name = mk_pp PrintTypes.name_to_string
 let pp_place = mk_pp PrintExpressions.place_to_string
+let pp_statement = mk_pp_indent PrintUllbcAst.Ast.statement_to_string
+let pp_terminator = mk_pp_indent PrintUllbcAst.Ast.terminator_to_string
 
 let get_adt id =
   let crate = get_crate () in
diff --git a/soteria-rust/lib/encoder.ml b/soteria-rust/lib/encoder.ml
index 271bea57a..f7e7fca93 100644
--- a/soteria-rust/lib/encoder.ml
+++ b/soteria-rust/lib/encoder.ml
@@ -123,18 +123,10 @@ module Make (Sptr : Sptr.S) = struct
       @@
       match ty with
       | TAdt { id = TTuple; generics = { types; _ } } -> Iter.of_list types
-      | TAdt
-          {
-            id = TBuiltin TArray;
-            generics = { types = [ ty ]; const_generics = [ len ]; _ };
-          } ->
-          Iter.repeatz (z_of_const_generic len) ty
-      | TAdt { id = TBuiltin ((TStr | TSlice) as kind); generics } -> (
+      | TArray (ty, len) -> Iter.repeatz (z_of_const_generic len) ty
+      | TSlice _ | TAdt { id = TBuiltin TStr; _ } -> (
           let sub_ty =
-            match kind with
-            | TSlice -> List.hd generics.types
-            | TStr -> TLiteral (TUInt U8)
-            | _ -> failwith "unreachable"
+            match ty with TSlice ty -> ty | _ -> TLiteral (TUInt U8)
           in
           match meta with
           | Len len when Option.is_some (BV.to_z len) ->
diff --git a/soteria-rust/lib/frontend.ml b/soteria-rust/lib/frontend.ml
index 71eba1a2f..946287bd5 100644
--- a/soteria-rust/lib/frontend.ml
+++ b/soteria-rust/lib/frontend.ml
@@ -508,7 +508,7 @@ module Diagnostic = struct
             ?content:span.file.contents file (to_loc span.beg_loc)
             (to_loc span.end_loc);
         ]
-    | Virtual _ -> []
+    | Virtual _ | NotReal _ -> []
 
   let print_diagnostic ~fname ~call_trace ~error =
     Soteria.Terminal.Diagnostic.print_diagnostic ~call_trace ~as_ranges
diff --git a/soteria-rust/lib/interp.ml b/soteria-rust/lib/interp.ml
index 5eca4bc33..34a7580bf 100644
--- a/soteria-rust/lib/interp.ml
+++ b/soteria-rust/lib/interp.ml
@@ -252,6 +252,10 @@ module Make (State : State_intf.S) = struct
         in
         Union blocks
     | COpaque msg -> Fmt.kstr not_impl "Opaque constant: %s" msg
+    | CAdt _ | CArray _ | CSlice _ | CGlobal _ | CRef _ | CPtr _ | CFnPtr _
+    | CPtrNoProvenance _ ->
+        Fmt.kstr not_impl "TODO: complex constant %a" Crate.pp_constant_expr
+          const
     | CVar _ -> not_impl "TODO: resolve const Var (mono error)"
 
   (** Resolves a place to a pointer *)
@@ -315,14 +319,8 @@ module Make (State : State_intf.S) = struct
         let len =
           match (meta, base.ty) with
           (* Array with static size *)
-          | ( Thin,
-              TAdt
-                {
-                  id = TBuiltin TArray;
-                  generics = { const_generics = [ len ]; _ };
-                } ) ->
-              BV.usize_of_const_generic len
-          | Len len, TAdt { id = TBuiltin TSlice; _ } -> Typed.cast_i Usize len
+          | Thin, TArray (_, len) -> BV.usize_of_const_generic len
+          | Len len, TSlice _ -> Typed.cast_i Usize len
           | _ -> Fmt.failwith "Index projection: unexpected arguments"
         in
         let* idx = eval_operand idx in
@@ -341,17 +339,8 @@ module Make (State : State_intf.S) = struct
         let ty, len =
           match (meta, base.ty) with
           (* Array with static size *)
-          | ( Thin,
-              TAdt
-                {
-                  id = TBuiltin TArray;
-                  generics = { const_generics = [ len ]; types = [ ty ]; _ };
-                } ) ->
-              (ty, BV.usize_of_const_generic len)
-          | ( Len len,
-              TAdt { id = TBuiltin TSlice; generics = { types = [ ty ]; _ } } )
-            ->
-              (ty, Typed.cast len)
+          | Thin, TArray (ty, len) -> (ty, BV.usize_of_const_generic len)
+          | Len len, TSlice ty -> (ty, Typed.cast len)
           | _ -> Fmt.failwith "Index projection: unexpected arguments"
         in
         let* from = eval_operand from in
@@ -563,29 +552,29 @@ module Make (State : State_intf.S) = struct
               match meta with
               | MetaLength length ->
                   ok @@ Len (BV.usize_of_const_generic length)
-              | MetaVTableDirect (_, glob) ->
+              | MetaVTable (_, glob) ->
                   (* the global adds one level of indirection *)
                   let* glob = of_opt_not_impl "Missing VTable global" glob in
                   let* ptr = resolve_global glob in
                   let+ vtable = State.load ptr unit_ptr in
                   let vtable, _ = as_ptr vtable in
                   VTable vtable
-              (* We don't check validity of the metadata if the unsizing
-                  doesn't need to modify the VTable. *)
-              | MetaVTableNested (_, None) -> ok prev
-              | MetaVTableNested (_, Some field) -> (
+              | MetaVTableUpcast fields -> (
                   match prev with
                   | Thin -> failwith "Unsizing VTable with no meta?"
                   | Len _ -> error `UBDanglingPointer
                   | VTable vt ->
-                      let idx = Types.FieldId.to_int field in
-                      let* vt_addr =
-                        Sptr.offset ~ty:unit_ptr ~signed:false vt
-                          (BV.usizei idx)
+                      let+ vt' =
+                        fold_list fields ~init:vt ~f:(fun vt field ->
+                            let idx = Types.FieldId.to_int field in
+                            let* vt_addr =
+                              Sptr.offset ~ty:unit_ptr ~signed:false vt
+                                (BV.usizei idx)
+                            in
+                            let+ vt = State.load (vt_addr, Thin) unit_ptr in
+                            fst (as_ptr vt))
                       in
-                      let+ vt = State.load (vt_addr, Thin) unit_ptr in
-                      let vt, _ = as_ptr vt in
-                      VTable vt)
+                      VTable vt')
               | MetaUnknown ->
                   Fmt.kstr not_impl "Unsupported metadata in CastUnsize: %a"
                     Expressions.pp_unsizing_metadata meta
diff --git a/soteria-rust/lib/layout.ml b/soteria-rust/lib/layout.ml
index 09bf3500c..910878b15 100644
--- a/soteria-rust/lib/layout.ml
+++ b/soteria-rust/lib/layout.ml
@@ -113,7 +113,7 @@ let empty_generics = TypesUtils.empty_generic_args
 type meta_kind = LenKind | VTableKind | NoneKind
 
 let rec dst_kind : Types.ty -> meta_kind = function
-  | TAdt { id = TBuiltin TStr; _ } | TAdt { id = TBuiltin TSlice; _ } -> LenKind
+  | TAdt { id = TBuiltin TStr; _ } | TSlice _ -> LenKind
   | TDynTrait _ -> VTableKind
   | TAdt { id = TAdtId id; _ } when Crate.is_struct id -> (
       match List.last_opt (Crate.as_struct id) with
@@ -125,8 +125,7 @@ let rec dst_kind : Types.ty -> meta_kind = function
     element. *)
 let rec dst_slice_ty : Types.ty -> Types.ty option = function
   | TAdt { id = TBuiltin TStr; _ } -> Some (TLiteral (TUInt U8))
-  | TAdt { id = TBuiltin TSlice; generics = { types = [ sub_ty ]; _ } } ->
-      Some sub_ty
+  | TSlice sub_ty -> Some sub_ty
   | TAdt { id = TAdtId id; _ } when Crate.is_struct id -> (
       match List.last_opt (Crate.as_struct id) with
       | None -> None
@@ -184,11 +183,8 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t =
      the tail in a DST struct.
      FIXME: Maybe we should mark the layout as a DST, and ensure a DST layout's size is never
      used for an allocation. *)
-  | TAdt { id = TBuiltin (TStr as ty); generics }
-  | TAdt { id = TBuiltin (TSlice as ty); generics } ->
-      let sub_ty =
-        if ty = TSlice then List.hd generics.types else TLiteral (TUInt U8)
-      in
+  | TAdt { id = TBuiltin TStr; _ } | TSlice _ ->
+      let sub_ty = match ty with TSlice ty -> ty | _ -> TLiteral (TUInt U8) in
       let++ sub_layout = layout_of sub_ty in
       mk ~size:(BV.usizei 0) ~align:sub_layout.align
         ~fields:(Array sub_layout.size) ()
@@ -207,14 +203,12 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t =
       | _, Enum variants -> compute_enum_layout ty variants
       | _, (Opaque | TDeclError _ | Alias _) -> not_impl_layout "unexpected" ty)
   (* Arrays *)
-  | TAdt { id = TBuiltin TArray; generics } ->
+  | TArray (subty, size) ->
       let max_array_len sub_size =
         (* We calculate the max array size for a 32bit architecture, like Miri does. *)
         let isize_bits = 32 - 1 in
         BV.usize Z.(one lsl isize_bits) /@ Typed.cast sub_size
       in
-      let size = List.hd generics.const_generics in
-      let subty = List.hd generics.types in
       let len = BV.of_const_generic size in
       let** sub_layout = layout_of subty in
       let++ () =
@@ -497,11 +491,7 @@ let rec nondet : Types.ty -> ('a rust_val, 'e, 'f) Result.t =
   | TAdt { id = TTuple; generics = { types; _ } } ->
       let++ fields = nondets types in
       Tuple fields
-  | TAdt
-      {
-        id = TBuiltin TArray;
-        generics = { const_generics = [ len ]; types = [ ty ]; _ };
-      } ->
+  | TArray (ty, len) ->
       let size = Charon_util.int_of_const_generic len in
       let++ fields = nondets @@ List.init size (fun _ -> ty) in
       Tuple fields
@@ -573,9 +563,7 @@ let rec as_zst : Types.ty -> 'a rust_val option =
   let as_zsts tys = Monad.OptionM.all as_zst tys in
   function
   | TNever -> Some (Tuple [])
-  | TAdt { id = TBuiltin TArray; generics = { const_generics = [ len ]; _ } }
-    when int_of_const_generic len = 0 ->
-      Some (Tuple [])
+  | TArray (_, len) when z_of_const_generic len = Z.zero -> Some (Tuple [])
   | TAdt { id = TAdtId id; _ } -> (
       let adt = Crate.get_adt id in
       match adt.kind with
@@ -628,9 +616,7 @@ let rec is_unsafe_cell : Types.ty -> bool = function
             @@ Iter.flat_map_l (fun (v : Types.variant) -> field_tys v.fields)
             @@ Iter.of_list vs
         | _ -> false)
-  | TAdt { id = TBuiltin (TArray | TSlice); generics = { types = [ ty ]; _ } }
-    ->
-      is_unsafe_cell ty
+  | TArray (ty, _) | TSlice ty -> is_unsafe_cell ty
   | TAdt { id = TTuple; generics = { types; _ } } ->
       List.exists is_unsafe_cell types
   | _ -> false
@@ -650,9 +636,7 @@ let rec ref_tys_in ?(include_ptrs = false) (v : 'a rust_val) (ty : Types.ty) :
   | Tuple vs, TAdt { id = TAdtId adt_id; _ } ->
       let fields = Crate.as_struct adt_id in
       List.concat_map2 f vs (field_tys fields)
-  | ( Tuple vs,
-      TAdt { id = TBuiltin (TArray | TSlice); generics = { types = [ ty ]; _ } }
-    ) ->
+  | Tuple vs, (TArray (ty, _) | TSlice ty) ->
       List.concat_map (fun v -> f v ty) vs
   | Tuple vs, TAdt { id = TTuple; generics = { types; _ } } ->
       List.concat_map2 f vs types
@@ -712,9 +696,7 @@ let rec update_ref_tys_in
       let fields = Crate.as_struct adt_id in
       let++ vs, acc = fs2 init vs (field_tys fields) in
       (Tuple vs, acc)
-  | ( Tuple vs,
-      TAdt { id = TBuiltin (TArray | TSlice); generics = { types = [ ty ]; _ } }
-    ) ->
+  | Tuple vs, (TArray (ty, _) | TSlice ty) ->
       let++ vs, acc = fs init vs ty in
       (Tuple vs, acc)
   | Tuple vs, TAdt { id = TTuple; generics = { types; _ } } ->
diff --git a/soteria-rust/lib/tree_borrow.ml b/soteria-rust/lib/tree_borrow.ml
index 4a836ccc4..01f538ecd 100644
--- a/soteria-rust/lib/tree_borrow.ml
+++ b/soteria-rust/lib/tree_borrow.ml
@@ -21,15 +21,10 @@ type access = Read | Write
 and locality = Local | Foreign
 and state = Reserved of bool | Unique | Frozen | ReservedIM | Disabled | UB
 
-(** The tag of the node, whether it has a protector (this is distinct from
-    having the protector toggled!), its parents (including this node's ID!), and
-    its initial state if it doesn't exist in the state. *)
-and node = {
-  tag : tag;
-  protector : bool;
-  parents : tag list;
-  initial_state : state;
-}
+(** Whether this node has a protector (this is distinct from having the
+    protector toggled!), its parents (including this node's ID!), and its
+    initial state if it doesn't exist in the state. *)
+and node = { protector : bool; parents : tag list; initial_state : state }
 [@@deriving show { with_path = false }]
 
 let pp_state fmt = function
@@ -94,9 +89,7 @@ let pp ft t =
 
 let init ~state () =
   let tag = fresh_tag () in
-  let node =
-    { tag; protector = false; parents = [ tag ]; initial_state = state }
-  in
+  let node = { protector = false; parents = [ tag ]; initial_state = state } in
   (TagMap.singleton tag node, tag)
 
 let ub_state = fst @@ init ~state:UB ()
@@ -105,12 +98,7 @@ let add_child ~parent ?(protector = false) ~state st =
   let tag = fresh_tag () in
   let node_parent = TagMap.find parent st in
   let node =
-    {
-      tag;
-      protector;
-      parents = tag :: node_parent.parents;
-      initial_state = state;
-    }
+    { protector; parents = tag :: node_parent.parents; initial_state = state }
   in
   (TagMap.add tag node st, tag)
 
@@ -141,36 +129,22 @@ let set_protector ~protected tag root =
 (** [access accessed im e structure state]: Update all nodes in the mapping
     [state] for the tree structure [structure] with an event [e], that happened
     at [accessed]. *)
-let access accessed e (root : t) st =
+let access accessed e (root : t) (st : tb_state) =
   let ub_happened = ref false in
-  let st =
-    TagMap.fold
-      (fun tag node ->
-        TagMap.update tag (function
-          | None -> Some (false, node.initial_state)
-          | Some _ as st -> st))
-      root st
-  in
-  L.trace (fun m ->
-      let pp_binding fmt (tag, (protected, st)) =
-        Fmt.pf fmt "%a -> %a%s" pp_tag tag pp_state st
-          (if protected then " (p)" else "")
-      in
-      m "TB: %a at %a, for tree %a, state@[<hov 2> %a@]" pp_access e pp_tag
-        accessed pp root
-        Fmt.(iter_bindings ~sep:(Fmt.any ", ") TagMap.iter pp_binding)
-        st);
   let accessed_node = TagMap.find accessed root in
   let st' =
-    TagMap.mapi
-      (fun tag (protected, st) ->
+    TagMap.filter_map_no_share
+      (fun tag { protector; initial_state; _ } ->
+        let protected, st =
+          match TagMap.find_opt tag st with
+          | None -> (false, initial_state)
+          | Some ps -> ps
+        in
         let rel =
           if List.mem tag accessed_node.parents then Local else Foreign
         in
         (* if the tag has a protector and is accessed, this toggles the protector! *)
-        let protected =
-          (tag = accessed || protected) && (TagMap.find tag root).protector
-        in
+        let protected = (tag = accessed || protected) && protector in
         let st' = transition ~protected st (rel, e) in
         if st' = UB then (
           ub_happened := true;
@@ -180,8 +154,9 @@ let access accessed e (root : t) st =
                  %b): %a -> %a in structure@.%a"
                 pp_tag tag pp_locality rel pp_access e protected pp_state st
                 pp_state st' pp root));
-        (protected, st'))
-      st
+        if (not protected) && st' = initial_state then None
+        else Some (protected, st'))
+      root
   in
   if !ub_happened then Result.error `AliasingError else Result.ok st'
 
diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml
index 9b40c997d..1fb9fb74f 100644
--- a/soteria/lib/sym_states/pmap.ml
+++ b/soteria/lib/sym_states/pmap.ml
@@ -37,7 +37,6 @@ module type MapS = sig
   val find_opt : key -> 'a t -> 'a option
   val iter : (key -> 'a -> unit) -> 'a t -> unit
   val to_seq : 'a t -> (key * 'a) Seq.t
-  val bindings : 'a t -> (key * 'a) list
 end
 
 module S
@@ -138,16 +137,6 @@ module Mk_concrete_key (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) :
   let iter_vars _ = fun _ -> ()
 end
 
-module PatriciaTreeMakeMap (K : sig
-  type t
-
-  val to_int : t -> int
-end) : MapS with type key = K.t = struct
-  include PatriciaTree.MakeMap (K)
-
-  let bindings m = to_seq m |> List.of_seq
-end
-
 module Build_from_find_opt_sym
     (Symex : Symex.Base)
     (Key : KeyS(Symex).S)
@@ -208,7 +197,8 @@ struct
     let st = of_opt st in
     let* key = Key.fresh () in
     let* () =
-      Symex.assume [ Key.distinct (key :: (M.bindings st |> List.map fst)) ]
+      Symex.assume
+        [ Key.distinct (key :: (M.to_seq st |> Seq.map fst |> List.of_seq)) ]
     in
     Result.ok (key, to_opt (M.add key new_codom st))
 
@@ -223,7 +213,9 @@ struct
     in
     let out_keys = List.rev out_keys in
     let st = M.add_seq bindings st in
-    let+ () = Symex.assume [ Key.distinct @@ List.map fst @@ M.bindings st ] in
+    let+ () =
+      Symex.assume [ M.to_seq st |> Seq.map fst |> List.of_seq |> Key.distinct ]
+    in
     Compo_res.Ok (out_keys, to_opt st)
 
   let wrap (f : 'a option -> ('b * 'a option, 'err, 'fix) Symex.Result.t)
@@ -292,7 +284,7 @@ struct
     in
     match M.find_opt key st with
     | Some v -> Symex.return (key, Some v)
-    | None -> find_bindings (M.bindings st)
+    | None -> M.to_seq st |> List.of_seq |> find_bindings
 
   include
     Build_from_find_opt_sym (Symex) (Key) (M)
@@ -307,7 +299,7 @@ module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) =
 module Make_patricia_tree
     (Symex : Symex.Base)
     (Key : KeyS(Symex).S_patricia_tree) =
-  Build_base (Symex) (Key) (PatriciaTreeMakeMap (Key))
+  Build_base (Symex) (Key) (PatriciaTree.MakeMap (Key))
 
 (** Sound to use when the keys of the map may depend on symbolic variables *)
 
@@ -333,7 +325,7 @@ struct
           M.to_seq st |> Seq.map fst |> List.of_seq |> Key.distinct
         in
         if%sat1 not_in_map then Symex.return (key, None)
-        else find_bindings (M.bindings st)
+        else M.to_seq st |> List.of_seq |> find_bindings
 
   include
     Build_from_find_opt_sym (Symex) (Key) (M)
@@ -350,7 +342,7 @@ module Direct_access_patricia_tree
     (Symex : Symex.Base)
     (Key : KeyS(Symex).S_patricia_tree) =
 struct
-  module M' = PatriciaTreeMakeMap (Key)
+  module M' = PatriciaTree.MakeMap (Key)
   include Build_direct_access (Symex) (Key) (M')
 end