From ab0ab62ee26e4046902bdaba920fc18656d051bf Mon Sep 17 00:00:00 2001
From: Chris Hawblitzel <Chris.Hawblitzel@microsoft.com>
Date: Thu, 14 May 2026 14:17:28 -0700
Subject: [PATCH] Remove extra address-of operators to prepare for
 https://github.com/verus-lang/verus/pull/2377

---
 verified-node-replication/src/lib.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/verified-node-replication/src/lib.rs b/verified-node-replication/src/lib.rs
index 14afe32..3e75dc1 100644
--- a/verified-node-replication/src/lib.rs
+++ b/verified-node-replication/src/lib.rs
@@ -394,7 +394,7 @@ pub open spec fn add_ticket<DT: Dispatch>(
 ) -> bool {
     !pre.local_reads.dom().contains(rid) && !pre.local_updates.dom().contains(rid) && (match input {
         InputOperation::Read(read_op) => {
-            &&post == UnboundedLog::State::<DT> {
+            post == UnboundedLog::State::<DT> {
                 local_reads: pre.local_reads.insert(
                     rid,
                     crate::spec::unbounded_log::ReadonlyState::Init { op: read_op },
@@ -403,7 +403,7 @@ pub open spec fn add_ticket<DT: Dispatch>(
             }
         },
         InputOperation::Write(write_op) => {
-            &&post == UnboundedLog::State::<DT> {
+            post == UnboundedLog::State::<DT> {
                 local_updates: pre.local_updates.insert(
                     rid,
                     crate::spec::unbounded_log::UpdateState::Init { op: write_op },