diff --git a/prusti-viper/src/encoder/high/procedures/inference/semantics.rs b/prusti-viper/src/encoder/high/procedures/inference/semantics.rs
index e330a95e69b..3fff0eae6cf 100644
--- a/prusti-viper/src/encoder/high/procedures/inference/semantics.rs
+++ b/prusti-viper/src/encoder/high/procedures/inference/semantics.rs
@@ -273,13 +273,21 @@ fn extract_managed_predicate_place(
         vir_typed::Predicate::OwnedNonAliased(predicate) => {
             Ok(Some(Permission::Owned(predicate.place.clone())))
         }
+        vir_typed::Predicate::UniqueRef(predicate) => {
+            Ok(Some(Permission::Owned(predicate.place.clone())))
+        }
+        vir_typed::Predicate::FracRef(predicate) => {
+            Ok(Some(Permission::Owned(predicate.place.clone())))
+        }
         vir_typed::Predicate::MemoryBlockStackDrop(_)
         | vir_typed::Predicate::LifetimeToken(_)
         | vir_typed::Predicate::MemoryBlockHeap(_)
         | vir_typed::Predicate::MemoryBlockHeapRange(_)
         | vir_typed::Predicate::MemoryBlockHeapDrop(_)
         | vir_typed::Predicate::OwnedRange(_)
-        | vir_typed::Predicate::OwnedSet(_) => {
+        | vir_typed::Predicate::OwnedSet(_)
+        | vir_typed::Predicate::UniqueRefRange(_)
+        | vir_typed::Predicate::FracRefRange(_) => {
             // Unmanaged predicates.
             Ok(None)
         }
diff --git a/prusti-viper/src/encoder/high/procedures/inference/unfolding_expressions.rs b/prusti-viper/src/encoder/high/procedures/inference/unfolding_expressions.rs
index bff3478157f..d8d4b1a8ab9 100644
--- a/prusti-viper/src/encoder/high/procedures/inference/unfolding_expressions.rs
+++ b/prusti-viper/src/encoder/high/procedures/inference/unfolding_expressions.rs
@@ -184,6 +184,10 @@ impl ExpressionFallibleFolder for Ensurer {
                         }
                         vir_typed::Predicate::OwnedRange(_) => todo!(),
                         vir_typed::Predicate::OwnedSet(_) => todo!(),
+                        vir_typed::Predicate::UniqueRef(_) => todo!(),
+                        vir_typed::Predicate::UniqueRefRange(_) => todo!(),
+                        vir_typed::Predicate::FracRef(_) => todo!(),
+                        vir_typed::Predicate::FracRefRange(_) => todo!(),
                     }
                 } else {
                     default_fallible_fold_binary_op(self, binary_op)
diff --git a/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs b/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
index 5225be6d8a3..62d88cf571c 100644
--- a/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
+++ b/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
@@ -27,7 +27,8 @@ use vir_crate::{
     middle::{
         self as vir_mid,
         operations::{
-            ty::Typed, TypedToMiddleExpression, TypedToMiddleStatement, TypedToMiddleType,
+            ty::Typed, TypedToMiddleExpression, TypedToMiddlePredicate, TypedToMiddleStatement,
+            TypedToMiddleType,
         },
     },
     typed::{self as vir_typed},
@@ -654,6 +655,58 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
                 );
                 self.current_statements.push(encoded_statement);
             }
+            vir_typed::Statement::Havoc(havoc_statement) => {
+                // The procedure encoder provides only Owned predicates. Based
+                // on the place and whether the reference is opened or not, we
+                // produce the actual predicate.
+                let predicate = match havoc_statement.predicate {
+                    vir_typed::Predicate::LifetimeToken(_) => todo!(),
+                    vir_typed::Predicate::MemoryBlockStack(predicate) => {
+                        vir_mid::Predicate::MemoryBlockStack(
+                            predicate.typed_to_middle_predicate(self.encoder)?,
+                        )
+                    }
+                    vir_typed::Predicate::MemoryBlockStackDrop(_) => todo!(),
+                    vir_typed::Predicate::MemoryBlockHeap(_) => todo!(),
+                    vir_typed::Predicate::MemoryBlockHeapRange(_) => todo!(),
+                    vir_typed::Predicate::MemoryBlockHeapDrop(_) => todo!(),
+                    vir_typed::Predicate::OwnedNonAliased(predicate) => {
+                        // TODO: Take into account whether the reference is opened or not.
+                        if let Some((lifetime, uniqueness)) = predicate.place.get_dereference_kind()
+                        {
+                            let lifetime = lifetime.typed_to_middle_type(self.encoder)?;
+                            let place = predicate.place.typed_to_middle_expression(self.encoder)?;
+                            match uniqueness {
+                                vir_typed::ty::Uniqueness::Unique => {
+                                    vir_mid::Predicate::unique_ref(
+                                        lifetime,
+                                        place,
+                                        predicate.position,
+                                    )
+                                }
+                                vir_typed::ty::Uniqueness::Shared => vir_mid::Predicate::frac_ref(
+                                    lifetime,
+                                    place,
+                                    predicate.position,
+                                ),
+                            }
+                        } else {
+                            vir_mid::Predicate::OwnedNonAliased(
+                                predicate.typed_to_middle_predicate(self.encoder)?,
+                            )
+                        }
+                    }
+                    vir_typed::Predicate::OwnedRange(_) => todo!(),
+                    vir_typed::Predicate::OwnedSet(_) => todo!(),
+                    vir_typed::Predicate::UniqueRef(_) => todo!(),
+                    vir_typed::Predicate::UniqueRefRange(_) => todo!(),
+                    vir_typed::Predicate::FracRef(_) => todo!(),
+                    vir_typed::Predicate::FracRefRange(_) => todo!(),
+                };
+                let encoded_statement =
+                    vir_mid::Statement::havoc(predicate, havoc_statement.position);
+                self.current_statements.push(encoded_statement);
+            }
             _ => {
                 self.current_statements
                     .push(statement.typed_to_middle_statement(self.encoder)?);
diff --git a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs
index 8b33af3918d..2e4f28c06f2 100644
--- a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs
+++ b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs
@@ -77,6 +77,7 @@ pub(in super::super) struct BuiltinMethodsState {
     encoded_duplicate_frac_ref_method: FxHashSet<String>,
     encoded_write_address_constant_methods: FxHashSet<String>,
     encoded_owned_non_aliased_havoc_methods: FxHashSet<String>,
+    encoded_unique_ref_havoc_methods: FxHashSet<String>,
     encoded_memory_block_copy_methods: FxHashSet<String>,
     encoded_memory_block_split_methods: FxHashSet<String>,
     encoded_memory_block_range_split_methods: FxHashSet<String>,
@@ -152,6 +153,10 @@ trait Private {
         &self,
         ty: &vir_mid::Type,
     ) -> SpannedEncodingResult<String>;
+    fn encode_havoc_unique_ref_method_name(
+        &self,
+        ty: &vir_mid::Type,
+    ) -> SpannedEncodingResult<String>;
     fn encode_assign_method(
         &mut self,
         method_name: &str,
@@ -531,6 +536,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<String> {
         Ok(format!("havoc_owned${}", ty.get_identifier()))
     }
+    fn encode_havoc_unique_ref_method_name(
+        &self,
+        ty: &vir_mid::Type,
+    ) -> SpannedEncodingResult<String> {
+        Ok(format!("havoc_unique_ref${}", ty.get_identifier()))
+    }
     fn encode_assign_method(
         &mut self,
         method_name: &str,
@@ -1694,6 +1705,7 @@ pub(in super::super) trait BuiltinMethodsInterface {
         &mut self,
         ty: &vir_mid::Type,
     ) -> SpannedEncodingResult<()>;
+    fn encode_havoc_unique_ref_method(&mut self, ty: &vir_mid::Type) -> SpannedEncodingResult<()>;
     fn encode_havoc_memory_block_method_name(
         &mut self,
         ty: &vir_mid::Type,
@@ -2258,6 +2270,65 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> {
         }
         Ok(())
     }
+    fn encode_havoc_unique_ref_method(&mut self, ty: &vir_mid::Type) -> SpannedEncodingResult<()> {
+        let ty_identifier = ty.get_identifier();
+        if !self
+            .builtin_methods_state
+            .encoded_unique_ref_havoc_methods
+            .contains(&ty_identifier)
+        {
+            self.builtin_methods_state
+                .encoded_unique_ref_havoc_methods
+                .insert(ty_identifier);
+            use vir_low::macros::*;
+            let method_name = self.encode_havoc_unique_ref_method_name(ty)?;
+            let type_decl = self.encoder.get_type_decl_mid(ty)?;
+            var_decls! {
+                place: PlaceOption,
+                root_address: Address,
+                lifetime: Lifetime,
+                fresh_snapshot: {ty.to_snapshot(self)?}
+            };
+            let position = vir_low::Position::default();
+            let validity =
+                self.encode_snapshot_valid_call_for_type(fresh_snapshot.clone().into(), ty)?;
+            let mut parameters = vec![place.clone(), root_address.clone(), lifetime.clone()];
+            parameters.extend(self.create_lifetime_parameters(&type_decl)?);
+            let TODO_target_slice_len = None;
+            let predicate_in = self.unique_ref_full_vars(
+                CallContext::BuiltinMethod,
+                ty,
+                &type_decl,
+                &place,
+                &root_address,
+                &lifetime,
+                TODO_target_slice_len.clone(),
+                position,
+            )?;
+            let predicate_out = self.unique_ref_full_vars_with_current_snapshot(
+                CallContext::BuiltinMethod,
+                ty,
+                &type_decl,
+                &place,
+                &root_address,
+                &fresh_snapshot,
+                &lifetime,
+                TODO_target_slice_len,
+                position,
+            )?;
+            let method = vir_low::MethodDecl::new(
+                method_name,
+                vir_low::MethodKind::Havoc,
+                parameters,
+                vec![fresh_snapshot.clone()],
+                vec![predicate_in],
+                vec![predicate_out, validity],
+                None,
+            );
+            self.declare_method(method)?;
+        }
+        Ok(())
+    }
     fn encode_memory_block_split_method(
         &mut self,
         ty: &vir_mid::Type,
@@ -2866,6 +2937,35 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> {
                     position,
                 )?;
             }
+            vir_mid::Predicate::UniqueRef(predicate) => {
+                let ty = predicate.place.get_type();
+                self.encode_havoc_unique_ref_method(ty)?;
+                self.mark_unique_ref_as_used(ty)?;
+                let lifetime =
+                    self.encode_lifetime_const_into_procedure_variable(predicate.lifetime)?;
+                let place = self.encode_expression_as_place(&predicate.place)?;
+                let address = self.encode_expression_as_place_address(&predicate.place)?;
+                let snapshot_type = ty.to_snapshot(self)?;
+                let fresh_snapshot = self.create_new_temporary_variable(snapshot_type)?;
+                let method_name = self.encode_havoc_unique_ref_method_name(ty)?;
+                let mut arguments = vec![place, address, lifetime.into()];
+                arguments.extend(self.create_lifetime_arguments(CallContext::Procedure, ty)?);
+                statements.push(vir_low::Statement::method_call(
+                    method_name,
+                    arguments,
+                    vec![fresh_snapshot.clone().into()],
+                    position,
+                ));
+                self.encode_snapshot_update(
+                    statements,
+                    &predicate.place,
+                    fresh_snapshot.into(),
+                    position,
+                )?;
+            }
+            vir_mid::Predicate::FracRef(_) => {
+                // Fractional references are immutable, so havoc is a no-op.
+            }
             vir_mid::Predicate::MemoryBlockStack(predicate) => {
                 let ty = predicate.place.get_type();
                 self.encode_havoc_memory_block_method(ty)?;
diff --git a/prusti-viper/src/encoder/middle/core_proof/footprint/interface.rs b/prusti-viper/src/encoder/middle/core_proof/footprint/interface.rs
index f5d59d7eddc..a785e52253c 100644
--- a/prusti-viper/src/encoder/middle/core_proof/footprint/interface.rs
+++ b/prusti-viper/src/encoder/middle/core_proof/footprint/interface.rs
@@ -148,6 +148,18 @@ impl<'l, 'p, 'v, 'tcx> vir_mid::visitors::ExpressionFolder
             vir_mid::Predicate::OwnedSet(predicate) => {
                 unimplemented!("predicate: {}", predicate);
             }
+            vir_mid::Predicate::UniqueRef(predicate) => {
+                unimplemented!("predicate: {}", predicate);
+            }
+            vir_mid::Predicate::UniqueRefRange(predicate) => {
+                unimplemented!("predicate: {}", predicate);
+            }
+            vir_mid::Predicate::FracRef(predicate) => {
+                unimplemented!("predicate: {}", predicate);
+            }
+            vir_mid::Predicate::FracRefRange(predicate) => {
+                unimplemented!("predicate: {}", predicate);
+            }
         }
     }
 
diff --git a/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs b/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs
index 49d62d40eb3..e5cee6be227 100644
--- a/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs
+++ b/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs
@@ -1701,6 +1701,10 @@ impl IntoLow for vir_mid::Predicate {
             }
             Predicate::OwnedRange(_) => todo!(),
             Predicate::OwnedSet(_) => todo!(),
+            Predicate::UniqueRef(_) => todo!(),
+            Predicate::UniqueRefRange(_) => todo!(),
+            Predicate::FracRef(_) => todo!(),
+            Predicate::FracRefRange(_) => todo!(),
         };
         Ok(result)
     }
diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/constructor.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/constructor.rs
index eac10dd29b9..23c5fb9be62 100644
--- a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/constructor.rs
+++ b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/constructor.rs
@@ -467,6 +467,10 @@ impl<'a, 'p, 'v: 'p, 'tcx: 'v> IntoSnapshotLowerer<'p, 'v, 'tcx>
                 ));
             }
             vir_mid::Predicate::OwnedSet(_) => todo!(),
+            vir_mid::Predicate::UniqueRef(_) => todo!(),
+            vir_mid::Predicate::UniqueRefRange(_) => todo!(),
+            vir_mid::Predicate::FracRef(_) => todo!(),
+            vir_mid::Predicate::FracRefRange(_) => todo!(),
         }
         Ok(true.into())
     }
diff --git a/vir/defs/high/ast/predicate.rs b/vir/defs/high/ast/predicate.rs
index 81b4f2db6eb..c94d135f6ac 100644
--- a/vir/defs/high/ast/predicate.rs
+++ b/vir/defs/high/ast/predicate.rs
@@ -16,6 +16,10 @@ pub enum Predicate {
     OwnedNonAliased(OwnedNonAliased),
     OwnedRange(OwnedRange),
     OwnedSet(OwnedSet),
+    UniqueRef(UniqueRef),
+    UniqueRefRange(UniqueRefRange),
+    FracRef(FracRef),
+    FracRefRange(FracRefRange),
 }
 
 #[display(fmt = "acc(LifetimeToken({}), {})", lifetime, permission)]
@@ -109,3 +113,53 @@ pub struct OwnedSet {
     pub set: Expression,
     pub position: Position,
 }
+
+/// A unique reference predicate of a specific type.
+#[display(fmt = "UniqueRef({}, {})", lifetime, place)]
+pub struct UniqueRef {
+    pub lifetime: LifetimeConst,
+    pub place: Expression,
+    pub position: Position,
+}
+
+/// A range of unique reference predicates of a specific type. `start_index` is
+/// inclusive and `end_index` is exclusive.
+#[display(
+    fmt = "UniqueRefRange({}, {}, {}, {})",
+    lifetime,
+    address,
+    start_index,
+    end_index
+)]
+pub struct UniqueRefRange {
+    pub lifetime: LifetimeConst,
+    pub address: Expression,
+    pub start_index: Expression,
+    pub end_index: Expression,
+    pub position: Position,
+}
+
+/// A shared reference predicate of a specific type.
+#[display(fmt = "FracRef({}, {})", lifetime, place)]
+pub struct FracRef {
+    pub lifetime: LifetimeConst,
+    pub place: Expression,
+    pub position: Position,
+}
+
+/// A range of shared reference predicates of a specific type. `start_index` is
+/// inclusive and `end_index` is exclusive.
+#[display(
+    fmt = "FracRefRange({}, {}, {}, {})",
+    lifetime,
+    address,
+    start_index,
+    end_index
+)]
+pub struct FracRefRange {
+    pub lifetime: LifetimeConst,
+    pub address: Expression,
+    pub start_index: Expression,
+    pub end_index: Expression,
+    pub position: Position,
+}
diff --git a/vir/defs/high/operations_internal/expression.rs b/vir/defs/high/operations_internal/expression.rs
index 8c8b49d34d8..8b7b3580a16 100644
--- a/vir/defs/high/operations_internal/expression.rs
+++ b/vir/defs/high/operations_internal/expression.rs
@@ -1106,6 +1106,18 @@ impl Expression {
                     Predicate::OwnedSet(predicate) => {
                         unimplemented!("predicate: {}", predicate);
                     }
+                    Predicate::UniqueRef(predicate) => {
+                        self.owned_places.push(predicate.place.clone());
+                    }
+                    Predicate::UniqueRefRange(predicate) => {
+                        self.owned_range_addresses.push(predicate.address.clone());
+                    }
+                    Predicate::FracRef(predicate) => {
+                        self.owned_places.push(predicate.place.clone());
+                    }
+                    Predicate::FracRefRange(predicate) => {
+                        self.owned_range_addresses.push(predicate.address.clone());
+                    }
                 }
             }
         }
@@ -1144,6 +1156,24 @@ impl Expression {
                     Predicate::OwnedSet(predicate) => {
                         unimplemented!("predicate: {}", predicate);
                     }
+                    Predicate::UniqueRef(predicate) => {
+                        self.owned_places.push((
+                            self.path_condition.iter().cloned().conjoin(),
+                            predicate.place.clone(),
+                        ));
+                    }
+                    Predicate::UniqueRefRange(predicate) => {
+                        unimplemented!("predicate: {}", predicate);
+                    }
+                    Predicate::FracRef(predicate) => {
+                        self.owned_places.push((
+                            self.path_condition.iter().cloned().conjoin(),
+                            predicate.place.clone(),
+                        ));
+                    }
+                    Predicate::FracRefRange(predicate) => {
+                        unimplemented!("predicate: {}", predicate);
+                    }
                 }
             }
             fn walk_binary_op(&mut self, binary_op: &BinaryOp) {
diff --git a/vir/defs/high/operations_internal/identifier/predicate.rs b/vir/defs/high/operations_internal/identifier/predicate.rs
index 99a6be27c01..3c3c371a294 100644
--- a/vir/defs/high/operations_internal/identifier/predicate.rs
+++ b/vir/defs/high/operations_internal/identifier/predicate.rs
@@ -19,6 +19,10 @@ impl WithIdentifier for Predicate {
             Self::OwnedNonAliased(predicate) => predicate.get_identifier(),
             Self::OwnedRange(predicate) => predicate.get_identifier(),
             Self::OwnedSet(predicate) => predicate.get_identifier(),
+            Self::UniqueRef(predicate) => predicate.get_identifier(),
+            Self::UniqueRefRange(predicate) => predicate.get_identifier(),
+            Self::FracRef(predicate) => predicate.get_identifier(),
+            Self::FracRefRange(predicate) => predicate.get_identifier(),
         }
     }
 }
@@ -76,3 +80,30 @@ impl WithIdentifier for predicate::OwnedSet {
         format!("OwnedSet${}", self.set.get_type().get_identifier())
     }
 }
+
+impl WithIdentifier for predicate::UniqueRef {
+    fn get_identifier(&self) -> String {
+        format!("UniqueRef${}", self.place.get_type().get_identifier())
+    }
+}
+
+impl WithIdentifier for predicate::UniqueRefRange {
+    fn get_identifier(&self) -> String {
+        format!(
+            "UniqueRefRange${}",
+            self.address.get_type().get_identifier()
+        )
+    }
+}
+
+impl WithIdentifier for predicate::FracRef {
+    fn get_identifier(&self) -> String {
+        format!("FracRef${}", self.place.get_type().get_identifier())
+    }
+}
+
+impl WithIdentifier for predicate::FracRefRange {
+    fn get_identifier(&self) -> String {
+        format!("FracRefRange${}", self.address.get_type().get_identifier())
+    }
+}
diff --git a/vir/defs/high/operations_internal/predicate.rs b/vir/defs/high/operations_internal/predicate.rs
index 3707679039d..e267ccf4ba1 100644
--- a/vir/defs/high/operations_internal/predicate.rs
+++ b/vir/defs/high/operations_internal/predicate.rs
@@ -59,6 +59,22 @@ impl Predicate {
                 // target of the pointer stored in the set.
                 vec![predicate.set.get_type().clone()]
             }
+            Self::UniqueRef(predicate) => {
+                vec![predicate.place.get_type().clone()]
+            }
+            Self::UniqueRefRange(predicate) => {
+                // FIXME: This is probably wrong: we need to use the type of the
+                // target.
+                vec![predicate.address.get_type().clone()]
+            }
+            Self::FracRef(predicate) => {
+                vec![predicate.place.get_type().clone()]
+            }
+            Self::FracRefRange(predicate) => {
+                // FIXME: This is probably wrong: we need to use the type of the
+                // target.
+                vec![predicate.address.get_type().clone()]
+            }
         }
     }
     pub fn check_no_default_position(&self) {