diff --git a/clang/lib/Verify/Backend/Certify.cpp b/clang/lib/Verify/Backend/Certify.cpp
index 44abc9b9a3..4a7002032f 100644
--- a/clang/lib/Verify/Backend/Certify.cpp
+++ b/clang/lib/Verify/Backend/Certify.cpp
@@ -3414,9 +3414,227 @@ class Evaluator {
            false,
            Value});
     }
+    // A choice is a function of the values its condition reads: in two
+    // memories where its condition reads the same values, it is one value.
+    // Two values are evidence only where some value read differs.
+    for (size_t I = 0; I < ChoicesRead.size(); ++I)
+      for (size_t J = I + 1; J < ChoicesRead.size(); ++J) {
+        const auto &[Function, First, FirstValue] = ChoicesRead[I];
+        const auto &[Other, Second, SecondValue] = ChoicesRead[J];
+        if (Function != Other || FirstValue == SecondValue)
+          continue;
+        bool OnlyMemory = true;
+        for (size_t K = 0; K != First.size() && OnlyMemory; ++K)
+          OnlyMemory = Function->Parameters[K].Sort.Kind ==
+                           LogicSortKind::Heap ||
+                       First[K] == Second[K];
+        if (!OnlyMemory)
+          continue;
+        const std::string SavedFailure = Failure;
+        std::optional<bool> Apart = readsApart(*Function, First, Second);
+        if (!Apart) {
+          Failure = "whether " + shown(*Function, First) + " and " +
+                    shown(*Function, Second) +
+                    " read different values: " + Failure;
+          return false;
+        }
+        if (!*Apart) {
+          Failure = "the model gives " + shown(*Function, First) + " and " +
+                    shown(*Function, Second) +
+                    " different values, but its condition reads the same "
+                    "values in both memories";
+          return false;
+        }
+        Failure = SavedFailure;
+      }
     return true;
   }
 
+  /// The condition of a choice: the quantifier of its axiom
+  /// `!exists(k, [lo, hi,] body) || ...`.
+  static const LogicExpr *choiceCondition(const LogicFunctionDecl &Choice) {
+    if (Choice.Postconditions.empty())
+      return nullptr;
+    const LogicExpr *Axiom = Choice.Postconditions.front().get();
+    if (Axiom->K != LogicExpr::Or || Axiom->Children.empty())
+      return nullptr;
+    const LogicExpr *Not = Axiom->Children.front().get();
+    if (Not->K != LogicExpr::Not || Not->Children.size() != 1 ||
+        Not->Children.front()->K != LogicExpr::Exists)
+      return nullptr;
+    return Not->Children.front().get();
+  }
+
+  static bool readsMemory(const LogicExpr &E) {
+    if (E.K == LogicExpr::Select)
+      return true;
+    for (const auto &Child : E.Children)
+      if ((E.K == LogicExpr::SpecCall &&
+           Child->Sort.Kind == LogicSortKind::Heap) ||
+          readsMemory(*Child))
+        return true;
+    return false;
+  }
+
+  static std::unique_ptr<LogicExpr>
+  connective(LogicExpr::Kind K, std::unique_ptr<LogicExpr> L,
+             std::unique_ptr<LogicExpr> R) {
+    auto E = std::make_unique<LogicExpr>(K);
+    E->Sort = LogicSort::boolSort();
+    E->Children.push_back(std::move(L));
+    if (R)
+      E->Children.push_back(std::move(R));
+    return E;
+  }
+
+  static std::unique_ptr<LogicExpr> either(std::unique_ptr<LogicExpr> L,
+                                           std::unique_ptr<LogicExpr> R) {
+    if (!L)
+      return R;
+    if (!R)
+      return L;
+    return connective(LogicExpr::Or, std::move(L), std::move(R));
+  }
+
+  /// A formula that holds where evaluating \p E reads a different value in
+  /// the two memories, \p Second giving the term in the second: the first
+  /// such read in evaluation order, each read under the condition that
+  /// reaches it. Null when \p E reads no memory.
+  static std::unique_ptr<LogicExpr> readsDiffer(
+      const LogicExpr &E,
+      const std::function<std::unique_ptr<LogicExpr>(const LogicExpr &)>
+          &Second) {
+    if (!readsMemory(E))
+      return nullptr;
+    auto differ = [&](const LogicExpr &Child) {
+      return readsDiffer(Child, Second);
+    };
+    switch (E.K) {
+    case LogicExpr::Select:
+    case LogicExpr::SpecCall: {
+      std::unique_ptr<LogicExpr> Differ;
+      for (const auto &Child : E.Children)
+        Differ = either(std::move(Differ), differ(*Child));
+      if (E.K == LogicExpr::Select ||
+          llvm::any_of(E.Children, [](const auto &Child) {
+            return Child->Sort.Kind == LogicSortKind::Heap;
+          }))
+        Differ = either(std::move(Differ),
+                        connective(LogicExpr::Ne, cloneLogicExpr(&E),
+                                   Second(E)));
+      return Differ;
+    }
+    case LogicExpr::And:
+    case LogicExpr::Or: {
+      // An operand is evaluated where those before it did not decide.
+      std::unique_ptr<LogicExpr> Differ, Reached;
+      for (const auto &Child : E.Children) {
+        std::unique_ptr<LogicExpr> Here = differ(*Child);
+        if (Here && Reached)
+          Here = connective(LogicExpr::And, cloneLogicExpr(Reached.get()),
+                            std::move(Here));
+        Differ = either(std::move(Differ), std::move(Here));
+        std::unique_ptr<LogicExpr> Continues =
+            E.K == LogicExpr::And
+                ? cloneLogicExpr(Child.get())
+                : connective(LogicExpr::Not, cloneLogicExpr(Child.get()),
+                             nullptr);
+        Reached = Reached ? connective(LogicExpr::And, std::move(Reached),
+                                       std::move(Continues))
+                          : std::move(Continues);
+      }
+      return Differ;
+    }
+    case LogicExpr::Ite: {
+      auto orFalse = [](std::unique_ptr<LogicExpr> F) {
+        if (F)
+          return F;
+        auto False = std::make_unique<LogicExpr>(LogicExpr::False);
+        False->Sort = LogicSort::boolSort();
+        return False;
+      };
+      std::unique_ptr<LogicExpr> Branches;
+      std::unique_ptr<LogicExpr> Then = differ(*E.Children[1]);
+      std::unique_ptr<LogicExpr> Else = differ(*E.Children[2]);
+      if (Then || Else) {
+        Branches = std::make_unique<LogicExpr>(LogicExpr::Ite);
+        Branches->Sort = LogicSort::boolSort();
+        Branches->Children.push_back(cloneLogicExpr(E.Children[0].get()));
+        Branches->Children.push_back(orFalse(std::move(Then)));
+        Branches->Children.push_back(orFalse(std::move(Else)));
+      }
+      return either(differ(*E.Children[0]), std::move(Branches));
+    }
+    case LogicExpr::Forall:
+    case LogicExpr::Exists: {
+      std::unique_ptr<LogicExpr> Differ;
+      for (size_t I = 0; I + 1 < E.Children.size(); ++I)
+        Differ = either(std::move(Differ), differ(*E.Children[I]));
+      if (std::unique_ptr<LogicExpr> Body = differ(*E.Children.back())) {
+        auto Some = std::make_unique<LogicExpr>(LogicExpr::Exists);
+        Some->Sort = LogicSort::boolSort();
+        Some->Binder = E.Binder;
+        for (size_t I = 0; I + 1 < E.Children.size(); ++I)
+          Some->Children.push_back(cloneLogicExpr(E.Children[I].get()));
+        Some->Children.push_back(std::move(Body));
+        Differ = either(std::move(Differ), std::move(Some));
+      }
+      return Differ;
+    }
+    default: {
+      std::unique_ptr<LogicExpr> Differ;
+      for (const auto &Child : E.Children)
+        Differ = either(std::move(Differ), differ(*Child));
+      return Differ;
+    }
+    }
+  }
+
+  /// Whether the condition of \p Choice reads a different value at \p First
+  /// and at \p Second; nullopt when it cannot be told.
+  std::optional<bool> readsApart(const LogicFunctionDecl &Choice,
+                                 const std::vector<LogicValue> &First,
+                                 const std::vector<LogicValue> &Second) {
+    const LogicExpr *Condition = choiceCondition(Choice);
+    if (!Condition) {
+      Failure = "the axiom of " + displayName(Choice) + " has no condition";
+      return std::nullopt;
+    }
+    std::set<std::string> Names;
+    for (const LogicFunctionParameter &Parameter : Choice.Parameters)
+      Names.insert(Parameter.Name);
+    const std::string Suffix = "\x1f" "second";
+    std::function<void(LogicExpr &)> rename = [&](LogicExpr &E) {
+      if (E.K == LogicExpr::Var && Names.count(E.Name))
+        E.Name += Suffix;
+      for (auto &Child : E.Children)
+        rename(*Child);
+    };
+    auto second = [&](const LogicExpr &E) {
+      std::unique_ptr<LogicExpr> Copy = cloneLogicExpr(&E);
+      rename(*Copy);
+      return Copy;
+    };
+    // The choice's own quantifier: its bounds, then its body at every value
+    // in range.
+    std::unique_ptr<LogicExpr> Differ = readsDiffer(*Condition, second);
+    if (!Differ)
+      return false;
+    const size_t SavedBase = ScopeBase;
+    const size_t SavedSize = Scope.size();
+    ScopeBase = SavedSize;
+    for (unsigned K = 0; K != First.size(); ++K) {
+      Scope.emplace_back(Choice.Parameters[K].Name, First[K]);
+      Scope.emplace_back(Choice.Parameters[K].Name + Suffix, Second[K]);
+    }
+    Active.push_back(&Choice);
+    std::optional<bool> Apart = truthOf(Differ.get());
+    Active.pop_back();
+    Scope.resize(SavedSize);
+    ScopeBase = SavedBase;
+    return Apart;
+  }
+
   const std::string &failure() const { return Failure; }
   bool limitInDefinition() const { return LimitInDefinition; }
   /// A choice the model gives a value its axioms exclude.
diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp
index 49997a782c..dcc801cfc4 100644
--- a/clang/lib/Verify/Frontend/ASTConverter.cpp
+++ b/clang/lib/Verify/Frontend/ASTConverter.cpp
@@ -3903,6 +3903,135 @@ static std::unique_ptr<VExpr> replaceVariable(const VExpr *E,
   return Out;
 }
 
+static void typeKey(const VType &Ty, std::string &Key) {
+  Key += '<';
+  for (uint64_t Field :
+       {static_cast<uint64_t>(Ty.Kind), static_cast<uint64_t>(Ty.IntMode),
+        static_cast<uint64_t>(Ty.IsSigned), static_cast<uint64_t>(Ty.BitWidth),
+        Ty.PointeeSizeBytes, Ty.ObjectSizeBytes, Ty.ObjectAlignBytes,
+        Ty.ArrayCount, Ty.ArrayStrideBytes})
+    Key += std::to_string(Field) + ',';
+  Key += Ty.TypeIdentity + ',' + Ty.EnumMin + ',' + Ty.EnumMax + '>';
+}
+
+/// A key two expressions share exactly when they are equal up to the names
+/// of their bound variables, or false.
+static bool structuralKey(const VExpr *E,
+                          std::map<std::string, std::string> &Bound,
+                          std::string &Key) {
+  if (!E) {
+    Key += '_';
+    return true;
+  }
+  Key += '(' + std::to_string(static_cast<int>(E->K));
+  typeKey(E->Ty, Key);
+  auto sub = [&](const VExpr *Child) {
+    return structuralKey(Child, Bound, Key);
+  };
+  switch (E->K) {
+  case VExpr::Literal:
+    Key += static_cast<const VLiteralExpr *>(E)->Value;
+    break;
+  case VExpr::Var: {
+    const auto *V = static_cast<const VVarExpr *>(E);
+    if (!V->ProvenanceVariable.empty() || V->Origins ||
+        !V->OriginCompanion.empty())
+      return false;
+    auto It = Bound.find(V->Name);
+    Key += It != Bound.end() ? It->second : V->Name;
+    break;
+  }
+  case VExpr::BinOp: {
+    const auto *B = static_cast<const VBinOpExpr *>(E);
+    Key += std::to_string(static_cast<int>(B->Op));
+    if (!sub(B->Lhs.get()) || !sub(B->Rhs.get()))
+      return false;
+    break;
+  }
+  case VExpr::UnaryOp: {
+    const auto *U = static_cast<const VUnaryOpExpr *>(E);
+    Key += std::to_string(static_cast<int>(U->Op)) + U->AllocationHeapVar +
+           ',' + U->LivenessHeapVar + ',' + U->InitializationHeapVar;
+    if (!sub(U->Operand.get()))
+      return false;
+    break;
+  }
+  case VExpr::Cast: {
+    const auto *Cast = static_cast<const VCastExpr *>(E);
+    typeKey(Cast->FromTy, Key);
+    Key += Cast->IsTrigger ? 't' : 'c';
+    if (!sub(Cast->Inner.get()))
+      return false;
+    break;
+  }
+  case VExpr::Load: {
+    const auto *L = static_cast<const VLoadExpr *>(E);
+    Key += L->HeapVar;
+    if (!sub(L->Ptr.get()) || !sub(L->AccessCondition.get()))
+      return false;
+    break;
+  }
+  case VExpr::Result:
+    break;
+  case VExpr::Old:
+    if (!sub(static_cast<const VOldExpr *>(E)->Inner.get()))
+      return false;
+    break;
+  case VExpr::Conditional: {
+    const auto *C = static_cast<const VConditionalExpr *>(E);
+    if (!sub(C->Cond.get()) || !sub(C->Then.get()) || !sub(C->Else.get()))
+      return false;
+    break;
+  }
+  case VExpr::Forall:
+  case VExpr::Exists: {
+    const auto *Q = static_cast<const VQuantifiedExpr *>(E);
+    typeKey(Q->BinderType, Key);
+    if (!sub(Q->Lo.get()) || !sub(Q->Hi.get()))
+      return false;
+    std::optional<std::string> Outer;
+    if (auto It = Bound.find(Q->Binder); It != Bound.end())
+      Outer = It->second;
+    Bound[Q->Binder] = '#' + std::to_string(Bound.size());
+    const bool Keyed = sub(Q->Body.get());
+    if (Outer)
+      Bound[Q->Binder] = *Outer;
+    else
+      Bound.erase(Q->Binder);
+    if (!Keyed)
+      return false;
+    break;
+  }
+  case VExpr::FieldAccess: {
+    const auto *F = static_cast<const VFieldAccessExpr *>(E);
+    Key += F->Field;
+    if (!sub(F->Base.get()))
+      return false;
+    break;
+  }
+  case VExpr::SpecCall: {
+    const auto *S = static_cast<const VSpecCallExpr *>(E);
+    Key += S->CalleeIdentity + (S->ReadsHeap ? "@" : "") + S->HeapVar;
+    for (const auto &Arg : S->Args)
+      if (!sub(Arg.get()))
+        return false;
+    break;
+  }
+  case VExpr::OverflowCheck: {
+    const auto *O = static_cast<const VOverflowCheckExpr *>(E);
+    Key += std::to_string(static_cast<int>(O->Op));
+    if (!sub(O->Lhs.get()) || !sub(O->Rhs.get()))
+      return false;
+    break;
+  }
+  case VExpr::HeapStore:
+  case VExpr::HeapFrame:
+    return false;
+  }
+  Key += ')';
+  return true;
+}
+
 std::unique_ptr<VExpr>
 ASTConverter::convertChoose(const ContractChooseExpr *C) {
   const VarDecl *BoundVar = C->getBoundVar();
@@ -3966,6 +4095,24 @@ ASTConverter::convertChoose(const ContractChooseExpr *C) {
   if (Hi)
     abstract(Hi);
 
+  // A choose with the same condition, up to the names of its bound
+  // variables, is the same choice, as Verus shares one closure function.
+  std::string Condition;
+  typeKey(ValueType, Condition);
+  Condition += Unbounded ? 'u' : 'b';
+  std::map<std::string, std::string> Canonical{{Binder, "#"}};
+  const bool Keyed = structuralKey(Lo.get(), Canonical, Condition) &&
+                     structuralKey(Hi.get(), Canonical, Condition) &&
+                     structuralKey(Body.get(), Canonical, Condition);
+  if (auto It = Keyed ? ChoiceByCondition.find(Condition)
+                      : ChoiceByCondition.end();
+      It != ChoiceByCondition.end())
+    return choiceApplication(C, It->second, std::move(Args), ValueType,
+                             expressionReadsHeap(Body.get()) ||
+                                 expressionReadsHeap(Lo.get()) ||
+                                 expressionReadsHeap(Hi.get()),
+                             Loc);
+
   auto Fn = std::make_unique<VFunction>();
   Fn->Name = "choose";
   Fn->Identity = "__cppverify_choose_" + std::to_string(ChoiceFunctions.size()) +
@@ -4010,7 +4157,19 @@ ASTConverter::convertChoose(const ContractChooseExpr *C) {
       std::move(Holds), VType::makeBool(), Loc));
   const std::string Identity = Fn->Identity;
   const bool ReadsHeap = Fn->ReadsHeap;
+  if (Keyed)
+    ChoiceByCondition.emplace(std::move(Condition), Identity);
   ChoiceFunctions.push_back(std::move(Fn));
+  return choiceApplication(C, Identity, std::move(Args), ValueType, ReadsHeap,
+                           Loc);
+}
+
+std::unique_ptr<VExpr>
+ASTConverter::choiceApplication(const ContractChooseExpr *C,
+                                const std::string &Identity,
+                                std::vector<std::unique_ptr<VExpr>> Args,
+                                const VType &ValueType, bool ReadsHeap,
+                                SourceLocation Loc) {
   auto Call = std::make_unique<VSpecCallExpr>("choose", Identity,
                                               std::move(Args), ValueType, Loc,
                                               ReadsHeap);
diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h
index 398e67f843..28b7d475e0 100644
--- a/clang/lib/Verify/Frontend/ASTConverter.h
+++ b/clang/lib/Verify/Frontend/ASTConverter.h
@@ -96,9 +96,15 @@ class ASTConverter {
   unsigned NextAssertBy = 0;
   /// The functions choose(...) expressions are lifted to.
   std::vector<std::unique_ptr<VFunction>> ChoiceFunctions;
+  /// The lifted choice of each condition, by its structural key.
+  std::map<std::string, std::string> ChoiceByCondition;
   /// Specs of <cppverify.h> the translation unit calls, such as valid.
   std::vector<std::unique_ptr<VFunction>> BuiltinFunctions;
   std::unique_ptr<VExpr> convertChoose(const ContractChooseExpr *C);
+  std::unique_ptr<VExpr>
+  choiceApplication(const ContractChooseExpr *C, const std::string &Identity,
+                    std::vector<std::unique_ptr<VExpr>> Args,
+                    const VType &ValueType, bool ReadsHeap, SourceLocation Loc);
   /// A cppverify collection operation or copy, with Handled set; null and
   /// Handled clear for anything else.
   std::unique_ptr<VExpr> convertCollection(const Expr *E, bool &Handled);
diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp
index fcfabb5a96..29e8f65c8f 100644
--- a/clang/lib/Verify/Transform/Passivize.cpp
+++ b/clang/lib/Verify/Transform/Passivize.cpp
@@ -2914,11 +2914,14 @@ void verify::addChoiceAxioms(std::vector<std::unique_ptr<PassiveStmt>> &Facts,
   }
 }
 
-/// A store outside the reads ranges of a spec leaves its value unchanged. For
-/// each application, relate it across every store back from its heap state.
+/// A store outside the reads ranges of a spec leaves its value unchanged, and
+/// a step that keeps every value a choice's condition reads keeps the choice.
+/// For each application, relate it across every store back from its heap
+/// state.
 static void addFrameInstances(PassiveProgram &P, const FunctionMap &FnMap) {
   auto Framed = [](const VSpecCallExpr &Call, const VFunction &Spec) {
-    return Call.ReadsHeap && !Call.HeapVar.empty() && !Spec.Reads.empty();
+    return Call.ReadsHeap && !Call.HeapVar.empty() &&
+           (!Spec.Reads.empty() || Spec.IsChoice);
   };
   std::map<std::string, FramedApplication> Applications;
   std::vector<const VQuantifiedExpr *> Enclosing;
@@ -3020,7 +3023,9 @@ static void addFrameInstances(PassiveProgram &P, const FunctionMap &FnMap) {
       const Store &S = It->second;
       const SourceLocation Loc = S.Loc;
       std::unique_ptr<VExpr> Outside;
-      if (S.Address) {
+      if (Spec.IsChoice) {
+        Outside = choiceReadsAgree(Spec, *Call, S.Before, S.After, FnMap, Loc);
+      } else if (S.Address) {
         Outside = addressOutsideReads(Spec, Call->Args, S.Address, Loc);
       } else {
         Outside = makeBoolLiteral(true, Loc);
diff --git a/clang/lib/Verify/Transform/SpecInline.cpp b/clang/lib/Verify/Transform/SpecInline.cpp
index 9873c6f760..9aea9bec38 100644
--- a/clang/lib/Verify/Transform/SpecInline.cpp
+++ b/clang/lib/Verify/Transform/SpecInline.cpp
@@ -1990,8 +1990,9 @@ std::unique_ptr<VExpr> anyOf(std::vector<std::unique_ptr<VExpr>> Terms,
 
 /// A load or a spec call in a spec body, with the condition that reaches it.
 struct BodySite {
-  /// The address of a load.
+  /// The address of a load, and the type it reads.
   std::unique_ptr<VExpr> Address;
+  VType LoadType;
   const VSpecCallExpr *Call = nullptr;
   /// The callee of a spec call, if known.
   const VFunction *Callee = nullptr;
@@ -2052,6 +2053,7 @@ struct SpecBodyCollector {
       const auto *L = static_cast<const VLoadExpr *>(E);
       BodySite Site;
       Site.Address = substParamsInExpr(L->Ptr.get(), Env);
+      Site.LoadType = L->Ty;
       Site.Loc = L->Loc;
       site(std::move(Site), Env, Guard, Quantifiers);
       expr(L->Ptr.get(), Env, Guard, Quantifiers);
@@ -2412,6 +2414,55 @@ static void readHeapAt(VExpr *E, const std::string &Heap) {
   }
 }
 
+std::unique_ptr<VExpr>
+verify::choiceReadsAgree(const VFunction &Choice, const VSpecCallExpr &Call,
+                         const std::string &Before, const std::string &After,
+                         const FunctionMap &FnMap, SourceLocation Loc) {
+  std::unique_ptr<VExpr> Witness = choiceWitness(Choice, Call);
+  if (!Witness)
+    return nullptr;
+  SpecBodyCollector Collector{FnMap};
+  const VLiteralExpr Always(true, VType::makeBool(), Loc);
+  Collector.expr(Witness.get(), {}, &Always, {});
+  if (Collector.Unsupported)
+    return nullptr;
+  auto at = [](const VExpr *E, const std::string &Heap) {
+    std::unique_ptr<VExpr> Copy = cloneVExpr(E);
+    readHeapAt(Copy.get(), Heap);
+    return Copy;
+  };
+  std::unique_ptr<VExpr> Agree =
+      std::make_unique<VLiteralExpr>(true, VType::makeBool(), Loc);
+  for (const BodySite &Site : Collector.Sites) {
+    std::unique_ptr<VExpr> Later, Earlier;
+    if (Site.Address) {
+      Later = std::make_unique<VLoadExpr>(at(Site.Address.get(), After),
+                                          Site.LoadType, Loc, After);
+      Earlier = std::make_unique<VLoadExpr>(at(Site.Address.get(), Before),
+                                            Site.LoadType, Loc, Before);
+    } else if (Site.Call->ReadsHeap) {
+      Later = at(Site.Call, After);
+      Earlier = at(Site.Call, Before);
+    } else {
+      continue;
+    }
+    std::unique_ptr<VExpr> Same = std::make_unique<VBinOpExpr>(
+        VBinOp::Eq, std::move(Later), std::move(Earlier), VType::makeBool(),
+        Loc);
+    if (Site.Guard)
+      Same = std::make_unique<VBinOpExpr>(
+          VBinOp::Or, makeDecreaseNot(at(Site.Guard.get(), Before), Loc),
+          std::move(Same), VType::makeBool(), Loc);
+    for (auto It = Site.Quantifiers.rbegin(); It != Site.Quantifiers.rend();
+         ++It)
+      Same = std::make_unique<VForallExpr>(
+          It->Binder, at(It->Lo.get(), Before), at(It->Hi.get(), Before),
+          std::move(Same), Loc, It->BinderType);
+    Agree = makeDecreaseAnd(std::move(Agree), std::move(Same), Loc);
+  }
+  return Agree;
+}
+
 std::unique_ptr<VExpr> verify::specPostcondition(
     const VFunction &Spec, const std::vector<std::unique_ptr<VExpr>> &Args,
     const VExpr *Value, SourceLocation Loc, const std::string &Heap) {
diff --git a/clang/lib/Verify/Transform/SpecInline.h b/clang/lib/Verify/Transform/SpecInline.h
index fb78e1e1e3..2a53bbfb87 100644
--- a/clang/lib/Verify/Transform/SpecInline.h
+++ b/clang/lib/Verify/Transform/SpecInline.h
@@ -105,6 +105,17 @@ regionOutsideReads(const VFunction &Spec,
                    const std::vector<std::unique_ptr<VExpr>> &Args,
                    const VExpr *Lo, const VExpr *Hi, SourceLocation Loc);
 
+/// Every value the condition of the choice applied by \p Call reads, at
+/// every value of its binder where it is evaluated, is the same in the
+/// memories \p Before and \p After: then so is the choice. Null when the
+/// body cannot be followed.
+std::unique_ptr<VExpr> choiceReadsAgree(const VFunction &Choice,
+                                        const VSpecCallExpr &Call,
+                                        const std::string &Before,
+                                        const std::string &After,
+                                        const FunctionMap &FnMap,
+                                        SourceLocation Loc);
+
 /// \p Check, a check of \p Spec, with the user's proof blocks of the kinds
 /// \p Kinds run after its assumptions and before its obligations. Within a
 /// block, result is the value the body returns, and an application of the
diff --git a/clang/test/Verify/suite/choose_identity.cpp b/clang/test/Verify/suite/choose_identity.cpp
new file mode 100644
index 0000000000..46efc598de
--- /dev/null
+++ b/clang/test/Verify/suite/choose_identity.cpp
@@ -0,0 +1,114 @@
+// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s --implicit-check-not=Verified:
+//
+// A choice is a function of the values its condition reads: two chooses with
+// the same condition, up to the name of the bound variable, are one choice,
+// as Verus shares one closure function, and a write to a cell the condition
+// does not read keeps it.
+
+namespace cv = cppverify;
+using namespace cppverify;
+
+cv::proof void same(int n)
+  cv::post(cv::choose(k, k > n) == cv::choose(k, k > n))
+{
+}
+// CHECK-DAG: Verified: same [backend=z3]
+
+cv::proof void renamed(int n)
+  cv::post(cv::choose(k, k > n) == cv::choose(j, j > n))
+{
+}
+// CHECK-DAG: Verified: renamed [backend=z3]
+
+// A quantifier inside the condition is compared up to its variable too.
+cv::proof void same_inner()
+  cv::post(cv::choose(k, 0, 10, cv::forall(j, 0, k, j < 5)) ==
+           cv::choose(k, 0, 10, cv::forall(i, 0, k, i < 5)))
+{
+}
+// CHECK-DAG: Verified: same_inner [backend=z3]
+
+int same_in_ghost(int n)
+  cv::post(cv::result == n)
+{
+  cv::ghost {
+    int a = cv::choose(k, 0, 10, k == 3);
+    int b = cv::choose(i, 0, 10, i == 3);
+    cv::check(a == b);
+  }
+  return n;
+}
+// CHECK-DAG: Verified: same_in_ghost [backend=z3]
+
+// Another condition, another value, or another range is another choice.
+cv::proof void other_condition(int n)
+  cv::post(cv::choose(k, k > n) == cv::choose(k, k >= n))
+{
+}
+// CHECK-DAG: error: verification failed: other_condition [{{.*}}] (counterexample:
+
+cv::proof void other_value(int n, int m)
+  cv::post(cv::choose(k, k > n) == cv::choose(k, k > m))
+{
+}
+// CHECK-DAG: error: verification failed: other_value [{{.*}}] (counterexample:
+
+cv::proof void other_range()
+  cv::post(cv::choose(k, 0, 10, k >= 0) == cv::choose(k, 0, 11, k >= 0))
+{
+}
+// CHECK-DAG: error: verification failed: other_range [{{.*}}] [backend=z3] [reason=counterexample]
+
+// The condition reads a[0] to a[n - 1]; b is another object.
+void write_other(const int *a, int n, int *b, int x)
+  cv::pre(valid(a, n) && n >= 1 && n <= 100 && valid(b, 1))
+  cv::modifies(*b)
+  cv::post(cv::choose(k, 0, n, a[k] == x) ==
+           cv::old(cv::choose(k, 0, n, a[k] == x)))
+{
+  *b = 5;
+}
+// CHECK-DAG: Verified: write_other [backend=z3]
+
+void clear(int *b)
+  cv::pre(valid(b, 1))
+  cv::modifies(*b)
+  cv::post(*b == 0)
+{
+  *b = 0;
+}
+// CHECK-DAG: Verified: clear [backend=z3]
+
+void call_writes_other(const int *a, int n, int *b, int x)
+  cv::pre(valid(a, n) && n >= 1 && n <= 100 && valid(b, 1))
+  cv::modifies(*b)
+  cv::post(cv::choose(k, 0, n, a[k] == x) ==
+           cv::old(cv::choose(k, 0, n, a[k] == x)))
+{
+  clear(b);
+}
+// CHECK-DAG: Verified: call_writes_other [backend=z3]
+
+// A write to a cell the condition reads may change the choice.
+void write_inside(int *a, int n, int x)
+  cv::pre(valid(a, n) && n >= 1 && n <= 100)
+  cv::modifies(a[0])
+  cv::post(cv::choose(k, 0, n, a[k] == x) ==
+           cv::old(cv::choose(k, 0, n, a[k] == x)))
+{
+  a[0] = x == 0 ? 1 : 0;
+}
+// CHECK-DAG: error: verification failed: write_inside [{{.*}}] (counterexample:
+
+// Which cells c[a[k]] reads depends on memory too: each read compares what it
+// reads in each memory, its address included, so the write to b keeps it.
+void write_other_indirect(const int *a, const int *c, int n, int *b, int x)
+  cv::pre(valid(a, n) && valid(c, n) && n >= 1 && n <= 100 && valid(b, 1))
+  cv::pre(cv::forall(k, 0, n, 0 <= a[k] && a[k] < n))
+  cv::modifies(*b)
+  cv::post(cv::choose(k, 0, n, c[a[k]] == x) ==
+           cv::old(cv::choose(k, 0, n, c[a[k]] == x)))
+{
+  *b = 5;
+}
+// CHECK-DAG: Verified: write_other_indirect [backend=z3]
diff --git a/clang/unittests/Verify/CertifyTest.cpp b/clang/unittests/Verify/CertifyTest.cpp
index a286037faa..0e8b528503 100644
--- a/clang/unittests/Verify/CertifyTest.cpp
+++ b/clang/unittests/Verify/CertifyTest.cpp
@@ -1389,6 +1389,77 @@ TEST(CertifyTest, ChoiceValuesMeetTheirAxioms) {
             CertifyOutcome::Undetermined);
 }
 
+TEST(CertifyTest, ChoicesAreFunctionsOfTheValuesTheyRead) {
+  // pick(h, a) = choose(k, 0, 2, h[a + k] == 7).
+  const LogicSort I32 = LogicSort::bitVector(32, true);
+  auto read = [&](Expr Offset) {
+    return node(LogicExpr::Select, I32, variable("h", LogicSort::heap()),
+                node(LogicExpr::Add, LogicSort::pointer(),
+                     variable("a", LogicSort::pointer()), std::move(Offset)));
+  };
+  auto seven = [&](Expr Offset) {
+    return boolean(LogicExpr::Eq, read(std::move(Offset)), literal("7", I32));
+  };
+  auto result = [] {
+    return variable(LogicFunctionDecl::ResultVariable, math());
+  };
+  LogicFunctionDecl Pick;
+  Pick.Identity = "pick_id";
+  Pick.DisplayName = "pick";
+  Pick.Parameters.push_back({"h", LogicSort::heap()});
+  Pick.Parameters.push_back({"a", LogicSort::pointer()});
+  Pick.ResultSort = math();
+  Pick.Choice = true;
+  Expr Witnessed = node(LogicExpr::Exists, LogicSort::boolSort(),
+                        mathLiteral(0), mathLiteral(2),
+                        seven(variable("k", math())));
+  Witnessed->Binder = "k";
+  Pick.Postconditions.push_back(boolean(
+      LogicExpr::Or, negation(std::move(Witnessed)),
+      boolean(LogicExpr::And,
+              boolean(LogicExpr::And,
+                      boolean(LogicExpr::Le, mathLiteral(0), result()),
+                      boolean(LogicExpr::Lt, result(), mathLiteral(2))),
+              seven(result()))));
+  ObligationModule Module = withFunction(std::move(Pick));
+  const LogicFunctionDecl &Choice = Module.LogicFunctions.at("pick_id");
+  auto pick = [&](const char *Heap) {
+    std::vector<Expr> Args;
+    Args.push_back(variable(Heap, LogicSort::heap()));
+    Args.push_back(variable("a", LogicSort::pointer()));
+    return call(Choice, std::move(Args));
+  };
+  Expr Query = boolean(LogicExpr::Ne, pick("h1"), pick("h2"));
+  TableModel Model;
+  Model.Constants["a"] = integerValue(100);
+  auto choose = [&](const LogicValue &Heap, int64_t Value) {
+    Model.Applications[TableModel::key("pick_id", {Heap, integerValue(100)})] =
+        integerValue(Value);
+  };
+
+  // The memories differ only at a cell the condition does not read, so the
+  // two values break the choice's meaning: no counterexample.
+  const LogicValue Both = heapOf({{100, 7}, {101, 7}}, 0);
+  const LogicValue Elsewhere = heapOf({{100, 7}, {101, 7}, {300, 1}}, 0);
+  Model.Constants["h1"] = Both;
+  Model.Constants["h2"] = Elsewhere;
+  choose(Both, 0);
+  choose(Elsewhere, 1);
+  CertifyResult Same = certifyCounterexample(Module, *Query, Model);
+  EXPECT_EQ(Same.Outcome, CertifyOutcome::Undetermined);
+  EXPECT_NE(Same.Detail.find("reads the same values in both memories"),
+            std::string::npos)
+      << Same.Detail;
+
+  // The condition reads h[101], which differs: two choices are allowed.
+  const LogicValue First = heapOf({{100, 7}, {101, 3}}, 0);
+  Model.Constants["h2"] = First;
+  choose(Both, 1);
+  choose(First, 0);
+  EXPECT_EQ(certifyCounterexample(Module, *Query, Model).Outcome,
+            CertifyOutcome::Certified);
+}
+
 TEST(CertifyTest, MutualRecursionAndMachineResults) {
   // even(n) = n == 0 || odd(n - 1); odd(n) = n != 0 && even(n - 1), over u8.
   const LogicSort U8 = LogicSort::bitVector(8, false);
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 58cd771142..877e28aca0 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -166,7 +166,10 @@ ranges over all mathematical integers. A `cppverify::trigger(term)` mark is an i
 `Cast` flagged `IsTrigger` around the term. Each `cppverify::choose` is lifted to a
 synthesized uninterpreted spec function (`IsChoice`) of the values its body
 mentions, whose postcondition is the Hilbert axiom `!cppverify::exists(k, P) || P(cppverify::result)`
-(with the range for a bounded choose). The calls in its body are calls of the
+(with the range for a bounded choose). Chooses with the same condition, compared
+by a structural key of its range and body that names bound variables by
+position, are lifted once (as Verus's `choose_map` shares closure functions), so
+they are one function. The calls in its body are calls of the
 function it is written in, for recursion and termination. A collection
 operation is a `SpecCall` whose identity is `__cppverify.<op>`, such as
 `__cppverify.seq.push`.
@@ -534,6 +537,18 @@ Terms added for the R3 language features:
   broke the axiom of a choice applied only inside an unfolding certified
   false counterexamples. A claim true only for some choices still fails
   certified, with choices the axioms allow.
+  A choice is a function of the values its condition reads, so the same
+  choice in two memories is one value where those values agree: for each
+  application of a choice that reads memory and each step back from its
+  memory, `addFrameInstances` assumes `agree -> c(after) == c(before)`, where
+  `agree` (`choiceReadsAgree`) says that every load of the condition, at
+  every binder value where it is evaluated and with its address read in
+  each memory, and every application in it that reads memory, has the same
+  value on both sides. The certifier holds a model to the same rule: two
+  values of one choice with the same other arguments are evidence only when
+  some value the condition reads differs between the memories
+  (`readsApart`, a formula that follows the condition's evaluation order),
+  and otherwise the counterexample is unchecked.
 - A comparison between a machine and a mathematical operand is lifted to
   the integers when the mathematical side mentions a quantifier binder or a
   collection, and otherwise split by range so the machine side keeps its
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index d08bbc23dd..6a5a303422 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -817,7 +817,13 @@ cppverify::spec int index_of(const int *a, int n, int x) { return cppverify::cho
 - `cppverify::choose(k, body)` is an integer for which `body` holds, when one exists,
   and otherwise an unspecified integer (Hilbert ε); `cppverify::choose(k, lo, hi, body)`
   chooses in `[lo, hi)`. Each `cppverify::choose` is a function of the values its body
-  mentions, so it is the same for the same values.
+  mentions, so it is the same for the same values. Two chooses whose
+  conditions are written the same way, up to the names of their variables,
+  are one choice (as Verus shares one closure function); one whose condition
+  is written differently is another, even when the conditions are
+  equivalent. The values a condition mentions include the cells it reads:
+  across a write that leaves every value it reads as it was, a choice keeps
+  its value.
 - The verifier knows only that, and knows it wherever a proof meets a
   choose, inside the unfoldings, postconditions, and induction hypotheses
   it assumes too. A claim true for some choices but not all fails with a
diff --git a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst
index 2b41863930..94feae927d 100644
--- a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst
+++ b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst
@@ -922,6 +922,68 @@ counterexample. A checked counterexample uses only choices that satisfy
 their bodies wherever some value does, including the chooses inside the
 definitions and postconditions a proof unfolds.
 
+"The same" is meant exactly. Two chooses whose conditions are written the
+same way, up to the names of their variables, are one choice, as Verus
+shares one function between them. The values a condition mentions include
+the cells it reads, so a choice over memory keeps its value across a write
+that leaves those cells as they were:
+
+.. code-block:: cpp
+
+   cv::proof void written_alike(int n)
+     cv::post(cv::choose(k, k > n) == cv::choose(j, j > n))
+   {
+   }
+
+   void write_other(const int *a, int n, int *b, int x)
+     cv::pre(valid(a, n) && n >= 1 && n <= 100 && valid(b, 1))
+     cv::modifies(*b)
+     cv::post(cv::choose(k, 0, n, a[k] == x) ==
+              cv::old(cv::choose(k, 0, n, a[k] == x)))
+   {
+     *b = 5;
+   }
+
+.. code-block:: text
+
+   Verified: written_alike [backend=z3]
+   Verified: write_other [backend=z3]
+
+The condition of ``write_other``'s choice reads ``a[0]`` to ``a[n - 1]``,
+and ``b`` is another object. A write to one of those cells may change the
+choice, and a condition written another way is another choice, even when
+it means the same:
+
+.. cppverify-example: fails write_inside written_differently
+
+.. code-block:: cpp
+
+   void write_inside(int *a, int n, int x)
+     cv::pre(valid(a, n) && n >= 1 && n <= 100)
+     cv::modifies(a[0])
+     cv::post(cv::choose(k, 0, n, a[k] == x) ==
+              cv::old(cv::choose(k, 0, n, a[k] == x)))
+   {
+     a[0] = x == 0 ? 1 : 0;
+   }
+
+   cv::proof void written_differently(int n)
+     cv::post(cv::choose(k, k > n) == cv::choose(k, n < k))
+   {
+   }
+
+.. code-block:: text
+
+   choose.cpp:5:43: error: verification failed: write_inside [...] (counterexample: a [ssa=a_0] [type=pointer] = ..., n [ssa=n_0] [type=i32] = 1, ...)
+   choose.cpp:12:33: error: verification failed: written_differently [...] (counterexample: n [ssa=n_0] [type=i32] = <unknown>)
+
+In every counterexample to ``write_inside`` the write changes ``a[0]``, a
+cell the condition reads, so the choice may move. When a proof needs equivalent conditions to choose alike, write
+them the same way, or put the choice in one spec function and apply it in
+both places. A counterexample is checked against this too: it may give one
+choice two values only in memories where its condition reads some
+different value.
+
 Spec collections
 ----------------
 
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index b8abf5d90b..d291445b57 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -95,6 +95,14 @@ that writes it (``int a; init(a);``) was a failure, or stopped the file; it is
 now ``Unresolved`` with reason ``construct.unsupported``, until a contract can
 say that a function writes its parameter first (:doc:`language/pointers`).
 
+**One condition, one choice.** Every ``cv::choose`` was a choice of its own, so
+``cv::choose(k, k > n) == cv::choose(k, k > n)`` failed with a counterexample,
+and so did a choice over memory compared across a write to another object.
+Chooses whose conditions are written alike are now one choice, a choice
+keeps its value across a write that leaves what its condition reads as it
+was, and a counterexample may give one choice two values only where
+something it reads differs (:doc:`book/part-ii/ch13-spec-and-proof-functions`).
+
 **Choices in counterexamples.** A counterexample could use a value of
 ``cv::choose`` that its body excludes, so true claims about a choice failed.
 Every choice a counterexample uses is now checked against its body