From 72b1f98f036ab3c6b8cf4bf12d39d61eec22a42b Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:27 +0530
Subject: [PATCH 01/14] verify: Share the subterms of logic terms, which no
 code changes.

---
 clang/lib/Verify/Backend/Obligation.h | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h
index e7d74d813f..a3281d8f53 100644
--- a/clang/lib/Verify/Backend/Obligation.h
+++ b/clang/lib/Verify/Backend/Obligation.h
@@ -4,6 +4,7 @@
 #define LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H
 
 #include "clang/Basic/SourceLocation.h"
+#include "llvm/ADT/IntrusiveRefCntPtr.h"
 #include "llvm/Support/Error.h"
 #include <cstdint>
 #include <map>
@@ -149,8 +150,16 @@ struct ObligationSource {
   bool hasRange() const { return isValid() && EndLine != 0; }
 };
 
+class LogicExpr;
+
+/// A subterm, shared and immutable: a goal states each assumption before it
+/// and a query its goal without copying them, so a module grows with what
+/// its terms say rather than with how often they repeat it (as Verus's AIR
+/// shares `Arc<ExprX>` and Frama-C's Qed hash-conses its terms).
+using LogicExprRef = llvm::IntrusiveRefCntPtr<const LogicExpr>;
+
 /// A typed logical term shared by every proof backend and IR dump.
-class LogicExpr {
+class LogicExpr : public llvm::ThreadSafeRefCountedBase<LogicExpr> {
 public:
   enum Kind {
     True,
@@ -201,9 +210,12 @@ class LogicExpr {
   LogicSort Sort;
   SourceLocation Loc;
   SourceLocation EndLoc;
-  ObligationSource Source;
+  /// Where Loc lies, filled in by the driver once the term is built
+  /// (annotateObligationSources): the one field written after a term is
+  /// shared, a function of Loc alone.
+  mutable ObligationSource Source;
 
-  std::vector<std::unique_ptr<LogicExpr>> Children;
+  std::vector<LogicExprRef> Children;
   std::string IntVal = "0";
   bool BoolVal = false;
   std::string Name;
@@ -215,7 +227,7 @@ class LogicExpr {
   /// For Forall and Exists: one multi-pattern for instantiating the
   /// quantifier, a solver hint outside the term's meaning, its identity, and
   /// archives.
-  std::vector<std::unique_ptr<LogicExpr>> Patterns;
+  std::vector<LogicExprRef> Patterns;
   /// For an Or that states one assumption of a goal (`!A || rest`): where A
   /// comes from (`pre`, `call:f`, `def:x_1`), so a goal can be shown as
   /// named hypotheses. Outside the term's meaning, identity, and archives.
@@ -231,7 +243,8 @@ using VCExpr = LogicExpr;
 /// trigger a quantifier.
 bool isCollectionRead(const LogicExpr &E);
 
-/// A deep copy of \p Expr, patterns included.
+/// A copy of \p Expr that may be changed: its own fields copied, its
+/// children and patterns shared, since no term changes a subterm.
 std::unique_ptr<LogicExpr> cloneLogicExpr(const LogicExpr *Expr);
 
 /// What an obligation establishes. Only Unwinding changes result semantics;

From 859ce5e591a1887eeb758d9ddc88d5a90acabeaa Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:28 +0530
Subject: [PATCH 02/14] verify: Copy only the root of a logic term, and
 simplify each shared subterm once.

---
 .../lib/Verify/Backend/ObligationSimplify.cpp | 154 ++++++++++++------
 1 file changed, 102 insertions(+), 52 deletions(-)

diff --git a/clang/lib/Verify/Backend/ObligationSimplify.cpp b/clang/lib/Verify/Backend/ObligationSimplify.cpp
index 27875e481e..3fc0f03d45 100644
--- a/clang/lib/Verify/Backend/ObligationSimplify.cpp
+++ b/clang/lib/Verify/Backend/ObligationSimplify.cpp
@@ -3,6 +3,7 @@
 #include "ObligationSimplify.h"
 #include "LogicTerms.h"
 #include "llvm/ADT/APInt.h"
+#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/CheckedArithmetic.h"
 #include <algorithm>
@@ -29,10 +30,8 @@ std::unique_ptr<LogicExpr> cloneLogicExpr(const LogicExpr *Expr) {
   Copy->CollectionOp = Expr->CollectionOp;
   Copy->SpecCallee = Expr->SpecCallee;
   Copy->Premise = Expr->Premise;
-  for (const auto &Child : Expr->Children)
-    Copy->Children.push_back(cloneLogicExpr(Child.get()));
-  for (const auto &Pattern : Expr->Patterns)
-    Copy->Patterns.push_back(cloneLogicExpr(Pattern.get()));
+  Copy->Children = Expr->Children;
+  Copy->Patterns = Expr->Patterns;
   return Copy;
 }
 
@@ -75,8 +74,10 @@ std::optional<bool> boolConstant(const LogicExpr *Expr) {
 }
 
 bool equalLogicExpr(const LogicExpr *Left, const LogicExpr *Right) {
+  if (Left == Right)
+    return true;
   if (!Left || !Right)
-    return Left == Right;
+    return false;
   if (Left->K != Right->K || Left->Sort.Kind != Right->Sort.Kind ||
       Left->Sort.BitWidth != Right->Sort.BitWidth ||
       Left->Sort.Signedness != Right->Sort.Signedness ||
@@ -131,11 +132,10 @@ std::optional<LogicSort> unsignedMathSourceSort(const LogicExpr *Expr) {
   return SourceSort;
 }
 
-std::unique_ptr<LogicExpr>
-lowerUnsignedMathArithmetic(std::unique_ptr<LogicExpr> Expr,
-                            const LogicSort &SourceSort) {
+LogicExprRef lowerUnsignedMathArithmetic(const LogicExprRef &Expr,
+                                         const LogicSort &SourceSort) {
   if (Expr->K == LogicExpr::BvToInt)
-    return std::move(Expr->Children.front());
+    return Expr->Children.front();
 
   auto Divisor = std::make_unique<LogicExpr>(LogicExpr::IntLit);
   Divisor->Sort = SourceSort;
@@ -150,19 +150,19 @@ lowerUnsignedMathArithmetic(std::unique_ptr<LogicExpr> Expr,
   MachineArithmetic->EndLoc = Expr->EndLoc;
   MachineArithmetic->Source = Expr->Source;
   MachineArithmetic->Children.push_back(
-      lowerUnsignedMathArithmetic(std::move(Expr->Children[0]), SourceSort));
+      lowerUnsignedMathArithmetic(Expr->Children[0], SourceSort));
   MachineArithmetic->Children.push_back(std::move(Divisor));
-  return MachineArithmetic;
+  return LogicExprRef(std::move(MachineArithmetic));
 }
 
-std::unique_ptr<LogicExpr>
-simplifyUnsignedMathToBitVector(std::unique_ptr<LogicExpr> Expr,
+LogicExprRef
+simplifyUnsignedMathToBitVector(const LogicExprRef &Expr,
                                 ObligationSimplificationStats &Stats) {
   if (!Expr || Expr->K != LogicExpr::IntToBv ||
       Expr->Sort.Kind != LogicSortKind::BitVector || Expr->Children.size() != 1)
     return Expr;
 
-  LogicExpr *Arithmetic = Expr->Children.front().get();
+  const LogicExpr *Arithmetic = Expr->Children.front().get();
   if (!Arithmetic ||
       (Arithmetic->K != LogicExpr::Div && Arithmetic->K != LogicExpr::Rem) ||
       Arithmetic->Sort.Kind != LogicSortKind::MathematicalInteger ||
@@ -172,8 +172,8 @@ simplifyUnsignedMathToBitVector(std::unique_ptr<LogicExpr> Expr,
   std::optional<LogicSort> SourceSort = unsignedMathSourceSort(Arithmetic);
   if (!SourceSort)
     return Expr;
-  auto MachineArithmetic = lowerUnsignedMathArithmetic(
-      std::move(Expr->Children.front()), *SourceSort);
+  LogicExprRef MachineArithmetic =
+      lowerUnsignedMathArithmetic(Expr->Children.front(), *SourceSort);
   ++Stats.Rewrites;
   if (Expr->Sort.BitWidth == SourceSort->BitWidth &&
       Expr->Sort.Signedness == SourceSort->Signedness)
@@ -185,63 +185,111 @@ simplifyUnsignedMathToBitVector(std::unique_ptr<LogicExpr> Expr,
   Resize->EndLoc = Expr->EndLoc;
   Resize->Source = Expr->Source;
   Resize->Children.push_back(std::move(MachineArithmetic));
-  return Resize;
+  return LogicExprRef(std::move(Resize));
 }
 
-std::unique_ptr<LogicExpr> simplifyExpr(std::unique_ptr<LogicExpr> Expr,
-                                        ObligationSimplificationStats &Stats) {
-  if (!Expr)
-    return nullptr;
-  for (auto &Child : Expr->Children)
-    Child = simplifyExpr(std::move(Child), Stats);
+/// What each subterm simplified to, and the rewrites that took, so a term
+/// shared by many goals is simplified once and stays shared. The key is held
+/// too, so no node is freed and its address reused while the memo lives.
+struct SimplifiedTerm {
+  LogicExprRef Term;
+  LogicExprRef Result;
+  uint64_t Rewrites = 0;
+};
+using SimplificationMemo = llvm::DenseMap<const LogicExpr *, SimplifiedTerm>;
+
+LogicExprRef simplifyTerm(const LogicExprRef &Expr,
+                          ObligationSimplificationStats &Stats,
+                          SimplificationMemo &Memo);
+
+LogicExprRef simplifyRules(const LogicExprRef &Expr,
+                           ObligationSimplificationStats &Stats,
+                           SimplificationMemo &Memo) {
+  // The node with its children simplified, copied only if one changed.
+  std::unique_ptr<LogicExpr> Copy;
+  for (size_t I = 0; I != Expr->Children.size(); ++I) {
+    LogicExprRef Child = simplifyTerm(Expr->Children[I], Stats, Memo);
+    if (Child == Expr->Children[I])
+      continue;
+    if (!Copy)
+      Copy = cloneLogicExpr(Expr.get());
+    Copy->Children[I] = std::move(Child);
+  }
+  const LogicExprRef Node = Copy ? LogicExprRef(std::move(Copy)) : Expr;
 
-  if ((Expr->K == LogicExpr::Eq || Expr->K == LogicExpr::Ne) &&
-      Expr->Children.size() == 2 &&
-      equalLogicExpr(Expr->Children[0].get(), Expr->Children[1].get())) {
+  if ((Node->K == LogicExpr::Eq || Node->K == LogicExpr::Ne) &&
+      Node->Children.size() == 2 &&
+      equalLogicExpr(Node->Children[0].get(), Node->Children[1].get())) {
     ++Stats.Rewrites;
-    return boolLiteral(Expr->K == LogicExpr::Eq, *Expr);
+    return LogicExprRef(boolLiteral(Node->K == LogicExpr::Eq, *Node));
   }
 
-  if (Expr->K == LogicExpr::Not && Expr->Children.size() == 1) {
+  if (Node->K == LogicExpr::Not && Node->Children.size() == 1) {
     if (std::optional<bool> Value =
-            boolConstant(Expr->Children.front().get())) {
+            boolConstant(Node->Children.front().get())) {
       ++Stats.Rewrites;
-      return boolLiteral(!*Value, *Expr);
+      return LogicExprRef(boolLiteral(!*Value, *Node));
     }
-    LogicExpr *Child = Expr->Children.front().get();
+    const LogicExpr *Child = Node->Children.front().get();
     if (Child && Child->K == LogicExpr::Not && Child->Children.size() == 1 &&
         Child->Children.front() &&
         Child->Children.front()->Sort.Kind == LogicSortKind::Bool) {
       ++Stats.Rewrites;
-      return std::move(Child->Children.front());
+      return Child->Children.front();
     }
   }
 
-  if ((Expr->K == LogicExpr::And || Expr->K == LogicExpr::Or) &&
-      Expr->Children.size() == 2) {
-    std::optional<bool> Left = boolConstant(Expr->Children[0].get());
-    std::optional<bool> Right = boolConstant(Expr->Children[1].get());
+  if ((Node->K == LogicExpr::And || Node->K == LogicExpr::Or) &&
+      Node->Children.size() == 2) {
+    std::optional<bool> Left = boolConstant(Node->Children[0].get());
+    std::optional<bool> Right = boolConstant(Node->Children[1].get());
     if (Left) {
-      const bool SelectRight = Expr->K == LogicExpr::And ? *Left : !*Left;
+      const bool SelectRight = Node->K == LogicExpr::And ? *Left : !*Left;
       ++Stats.Rewrites;
-      return SelectRight ? std::move(Expr->Children[1])
-                         : boolLiteral(*Left, *Expr);
+      return SelectRight ? Node->Children[1]
+                         : LogicExprRef(boolLiteral(*Left, *Node));
     }
     if (Right) {
-      const bool SelectLeft = Expr->K == LogicExpr::And ? *Right : !*Right;
+      const bool SelectLeft = Node->K == LogicExpr::And ? *Right : !*Right;
       ++Stats.Rewrites;
-      return SelectLeft ? std::move(Expr->Children[0])
-                        : boolLiteral(*Right, *Expr);
+      return SelectLeft ? Node->Children[0]
+                        : LogicExprRef(boolLiteral(*Right, *Node));
     }
   }
 
-  if (Expr->K == LogicExpr::Ite && Expr->Children.size() == 3)
-    if (std::optional<bool> Cond = boolConstant(Expr->Children.front().get())) {
+  if (Node->K == LogicExpr::Ite && Node->Children.size() == 3)
+    if (std::optional<bool> Cond = boolConstant(Node->Children.front().get())) {
       ++Stats.Rewrites;
-      return std::move(Expr->Children[*Cond ? 1 : 2]);
+      return Node->Children[*Cond ? 1 : 2];
     }
 
-  return simplifyUnsignedMathToBitVector(std::move(Expr), Stats);
+  return simplifyUnsignedMathToBitVector(Node, Stats);
+}
+
+LogicExprRef simplifyTerm(const LogicExprRef &Expr,
+                          ObligationSimplificationStats &Stats,
+                          SimplificationMemo &Memo) {
+  if (!Expr)
+    return nullptr;
+  if (auto Known = Memo.find(Expr.get()); Known != Memo.end()) {
+    Stats.Rewrites += Known->second.Rewrites;
+    return Known->second.Result;
+  }
+  const uint64_t Before = Stats.Rewrites;
+  LogicExprRef Result = simplifyRules(Expr, Stats, Memo);
+  Memo[Expr.get()] = {Expr, Result, Stats.Rewrites - Before};
+  return Result;
+}
+
+/// \p Expr simplified, as a root its owner may change.
+std::unique_ptr<LogicExpr> simplifyExpr(std::unique_ptr<LogicExpr> Expr,
+                                        ObligationSimplificationStats &Stats,
+                                        SimplificationMemo &Memo) {
+  if (!Expr)
+    return nullptr;
+  LogicExprRef Result =
+      simplifyTerm(LogicExprRef(std::move(Expr)), Stats, Memo);
+  return cloneLogicExpr(Result.get());
 }
 
 std::unique_ptr<LogicExpr> negate(std::unique_ptr<LogicExpr> Expr) {
@@ -297,13 +345,14 @@ bool callsOnlyReachableFunctions(const LogicExpr *Expr,
 }
 
 void simplifyFunctions(ObligationModule &Module,
-                       ObligationSimplificationStats &Stats) {
+                       ObligationSimplificationStats &Stats,
+                       SimplificationMemo &Memo) {
   for (auto &[Identity, Function] : Module.LogicFunctions) {
     (void)Identity;
     Function.StepDefinition =
-        simplifyExpr(std::move(Function.StepDefinition), Stats);
+        simplifyExpr(std::move(Function.StepDefinition), Stats, Memo);
     for (auto &Definition : Function.DefinitionLevels)
-      Definition = simplifyExpr(std::move(Definition), Stats);
+      Definition = simplifyExpr(std::move(Definition), Stats, Memo);
   }
 
   std::set<std::string> Reachable;
@@ -963,16 +1012,17 @@ simplifyObligationModule(ObligationModule Module,
 
   ObligationSimplificationStats Stats;
   Stats.NodesBefore = countModuleNodes(Module);
+  SimplificationMemo Memo;
   for (Obligation &Item : Module.Obligations) {
-    Item.Goal = simplifyExpr(std::move(Item.Goal), Stats);
+    Item.Goal = simplifyExpr(std::move(Item.Goal), Stats, Memo);
     Item.CounterexampleQuery = negate(cloneLogicExpr(Item.Goal.get()));
   }
   // The copies of assumptions stay equal to the assumptions in the goals.
   ObligationSimplificationStats Uncounted;
   for (auto *Copies : {&Module.Theorems, &Module.Preconditions})
     for (auto &Copy : *Copies)
-      Copy = simplifyExpr(std::move(Copy), Uncounted);
-  simplifyFunctions(Module, Stats);
+      Copy = simplifyExpr(std::move(Copy), Uncounted, Memo);
+  simplifyFunctions(Module, Stats, Memo);
   Module.CorrectnessGoal = buildCompleteGoal(Module.Obligations);
   Module.CounterexampleQuery =
       negate(cloneLogicExpr(Module.CorrectnessGoal.get()));

From 76a72e0441f979fa1dee552e5a5d3c8b9a7e7f10 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:28 +0530
Subject: [PATCH 03/14] verify: Build goals and queries from shared subterms
 instead of copies.

---
 clang/lib/Verify/Backend/Obligation.cpp | 89 ++++++++++---------------
 1 file changed, 37 insertions(+), 52 deletions(-)

diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp
index 0e602c1eba..07524b070f 100644
--- a/clang/lib/Verify/Backend/Obligation.cpp
+++ b/clang/lib/Verify/Backend/Obligation.cpp
@@ -401,32 +401,11 @@ static bool containsHeapSelect(const VCExpr *E) {
   return false;
 }
 
-static std::unique_ptr<VCExpr> cloneVCExpr(const VCExpr *E) {
-  if (!E)
-    return nullptr;
-  auto Copy = std::make_unique<VCExpr>(E->K);
-  Copy->Sort = E->Sort;
-  Copy->Loc = E->Loc;
-  Copy->EndLoc = E->EndLoc;
-  Copy->Source = E->Source;
-  Copy->IntVal = E->IntVal;
-  Copy->BoolVal = E->BoolVal;
-  Copy->Name = E->Name;
-  Copy->Binder = E->Binder;
-  Copy->OverflowOp = E->OverflowOp;
-  Copy->CollectionOp = E->CollectionOp;
-  Copy->SpecCallee = E->SpecCallee;
-  Copy->Premise = E->Premise;
-  for (const auto &Child : E->Children)
-    Copy->Children.push_back(cloneVCExpr(Child.get()));
-  for (const auto &Pattern : E->Patterns)
-    Copy->Patterns.push_back(cloneVCExpr(Pattern.get()));
-  return Copy;
-}
-
 static bool equalLogicExpr(const LogicExpr *Left, const LogicExpr *Right) {
+  if (Left == Right)
+    return true;
   if (!Left || !Right)
-    return Left == Right;
+    return false;
   if (Left->K != Right->K || Left->Sort.Kind != Right->Sort.Kind ||
       Left->Sort.BitWidth != Right->Sort.BitWidth ||
       Left->Sort.Signedness != Right->Sort.Signedness ||
@@ -447,10 +426,10 @@ static std::unique_ptr<VCExpr>
 buildCompleteGoal(const std::vector<Obligation> &Obligations) {
   if (Obligations.empty())
     return vcTrue();
-  auto Complete = cloneVCExpr(Obligations.front().Goal.get());
+  auto Complete = cloneLogicExpr(Obligations.front().Goal.get());
   for (unsigned I = 1; I != Obligations.size(); ++I)
     Complete =
-        vcAnd(std::move(Complete), cloneVCExpr(Obligations[I].Goal.get()));
+        vcAnd(std::move(Complete), cloneLogicExpr(Obligations[I].Goal.get()));
   return Complete;
 }
 
@@ -1235,7 +1214,7 @@ class ObligationBuilder {
     if (isActiveBoundVariable(Expr) || Expr->K == VCExpr::Collection)
       return true;
     return std::any_of(Expr->Children.begin(), Expr->Children.end(),
-                       [&](const std::unique_ptr<VCExpr> &Child) {
+                       [&](const LogicExprRef &Child) {
                          return liftsComparison(Child.get());
                        });
   }
@@ -1269,7 +1248,7 @@ class ObligationBuilder {
       return E;
     if (E->K == VCExpr::BvToInt && E->Children.size() == 1 && E->Children[0] &&
         E->Children[0]->Sort.Kind == LogicSortKind::BitVector)
-      E = std::move(E->Children[0]);
+      E = cloneLogicExpr(E->Children[0].get());
     if (E->Sort.Kind == LogicSortKind::BitVector) {
       if (E->Sort.BitWidth == TargetSort.BitWidth &&
           E->Sort.Signedness == TargetSort.Signedness)
@@ -1307,21 +1286,26 @@ class ObligationBuilder {
     case VCExpr::Mul:
       if (!Mathematical)
         break;
-      E->Children[0] = mathToMachine(std::move(E->Children[0]), TargetSort);
-      E->Children[1] = mathToMachine(std::move(E->Children[1]), TargetSort);
+      E->Children[0] =
+          mathToMachine(cloneLogicExpr(E->Children[0].get()), TargetSort);
+      E->Children[1] =
+          mathToMachine(cloneLogicExpr(E->Children[1].get()), TargetSort);
       E->Sort = TargetSort;
       return E;
     case VCExpr::Neg:
       if (!Mathematical)
         break;
-      E->Children[0] = mathToMachine(std::move(E->Children[0]), TargetSort);
+      E->Children[0] =
+          mathToMachine(cloneLogicExpr(E->Children[0].get()), TargetSort);
       E->Sort = TargetSort;
       return E;
     case VCExpr::Ite:
       if (!Mathematical)
         break;
-      E->Children[1] = mathToMachine(std::move(E->Children[1]), TargetSort);
-      E->Children[2] = mathToMachine(std::move(E->Children[2]), TargetSort);
+      E->Children[1] =
+          mathToMachine(cloneLogicExpr(E->Children[1].get()), TargetSort);
+      E->Children[2] =
+          mathToMachine(cloneLogicExpr(E->Children[2].get()), TargetSort);
       E->Sort = TargetSort;
       return E;
     default:
@@ -1339,7 +1323,7 @@ class ObligationBuilder {
       return E;
     if (Target == VIntMode::Math && E->K == VCExpr::IntToBv &&
         E->Children.size() == 1 && isActiveBoundVariable(E->Children[0].get()))
-      return std::move(E->Children[0]);
+      return cloneLogicExpr(E->Children[0].get());
     if (Target == VIntMode::Machine) {
       const LogicSort TargetSort =
           LogicSort::bitVector(E->Sort.BitWidth ? E->Sort.BitWidth : 32,
@@ -1373,9 +1357,9 @@ class ObligationBuilder {
                          std::unique_ptr<VCExpr> Math) {
     const unsigned BitWidth = Machine->Sort.BitWidth;
     const bool IsSigned = Machine->Sort.Signedness == LogicSignedness::Signed;
-    auto InRange = vcAnd(vcBinary(VCExpr::Ge, cloneVCExpr(Math.get()),
+    auto InRange = vcAnd(vcBinary(VCExpr::Ge, cloneLogicExpr(Math.get()),
                                   mathLimit(BitWidth, IsSigned, true)),
-                         vcBinary(VCExpr::Le, cloneVCExpr(Math.get()),
+                         vcBinary(VCExpr::Le, cloneLogicExpr(Math.get()),
                                   mathLimit(BitWidth, IsSigned, false)));
 
     const LogicSort MachineSort = Machine->Sort;
@@ -1397,13 +1381,13 @@ class ObligationBuilder {
     const unsigned BitWidth = Machine->Sort.BitWidth;
     const bool IsSigned = Machine->Sort.Signedness == LogicSignedness::Signed;
     const bool BelowMax = Kind == VCExpr::Lt || Kind == VCExpr::Le;
-    auto Outside = BelowMax ? vcBinary(VCExpr::Gt, cloneVCExpr(Math.get()),
+    auto Outside = BelowMax ? vcBinary(VCExpr::Gt, cloneLogicExpr(Math.get()),
                                        mathLimit(BitWidth, IsSigned, false))
-                            : vcBinary(VCExpr::Lt, cloneVCExpr(Math.get()),
+                            : vcBinary(VCExpr::Lt, cloneLogicExpr(Math.get()),
                                        mathLimit(BitWidth, IsSigned, true));
-    auto InRange = vcAnd(vcBinary(VCExpr::Ge, cloneVCExpr(Math.get()),
+    auto InRange = vcAnd(vcBinary(VCExpr::Ge, cloneLogicExpr(Math.get()),
                                   mathLimit(BitWidth, IsSigned, true)),
-                         vcBinary(VCExpr::Le, cloneVCExpr(Math.get()),
+                         vcBinary(VCExpr::Le, cloneLogicExpr(Math.get()),
                                   mathLimit(BitWidth, IsSigned, false)));
     const LogicSort MachineSort = Machine->Sort;
     auto Converted = mathToMachine(std::move(Math), MachineSort);
@@ -1610,7 +1594,7 @@ class ObligationBuilder {
     case VOverflowOp::SDiv:
       break;
     }
-    auto AboveMinimum = vcBinary(VCExpr::Ge, cloneVCExpr(Exact.get()),
+    auto AboveMinimum = vcBinary(VCExpr::Ge, cloneLogicExpr(Exact.get()),
                                  mathLimit(Width, true, true));
     auto BelowMaximum =
         vcBinary(VCExpr::Le, std::move(Exact), mathLimit(Width, true, false));
@@ -1671,7 +1655,7 @@ class ObligationBuilder {
       return;
     for (auto It = OpenQuantifiers.rbegin(); It != OpenQuantifiers.rend(); ++It)
       if (mentionsName(&Term, It->Binder)) {
-        It->Patterns.push_back(cloneVCExpr(&Term));
+        It->Patterns.push_back(cloneLogicExpr(&Term));
         return;
       }
   }
@@ -1713,7 +1697,8 @@ class ObligationBuilder {
       OpenQuantifiers.back().Patterns.clear();
       Body = fromVExpr(Q->Body.get());
     }
-    N->Patterns = std::move(OpenQuantifiers.back().Patterns);
+    for (auto &Pattern : OpenQuantifiers.back().Patterns)
+      N->Patterns.push_back(std::move(Pattern));
     OpenQuantifiers.pop_back();
     N->Children.push_back(std::move(Body));
     if (HadPrevious)
@@ -1915,8 +1900,8 @@ class ObligationBuilder {
       };
       if (IsInteger(N->Children[1]->Sort) && IsInteger(N->Children[2]->Sort) &&
           N->Children[1]->Sort.Kind != N->Children[2]->Sort.Kind) {
-        auto Unified =
-            unifyIntModes(std::move(N->Children[1]), std::move(N->Children[2]));
+        auto Unified = unifyIntModes(cloneLogicExpr(N->Children[1].get()),
+                                     cloneLogicExpr(N->Children[2].get()));
         N->Children[1] = std::move(Unified.first);
         N->Children[2] = std::move(Unified.second);
       }
@@ -2256,7 +2241,7 @@ class ObligationBuilder {
     if (!P.ContractConclusions.empty()) {
       auto Contract = std::make_shared<ContractTheorem>();
       for (const auto &Entry : EntryAssumes)
-        Contract->Premises.push_back(cloneVCExpr(Entry.get()));
+        Contract->Premises.push_back(cloneLogicExpr(Entry.get()));
       for (const auto &Conclusion : P.ContractConclusions)
         Contract->Conclusions.push_back(fromVExpr(Conclusion.get()));
       std::set<std::string> Bound;
@@ -2281,13 +2266,13 @@ class ObligationBuilder {
                                                           ? P.EntryOrigins[I]
                                                           : "entry");
     for (size_t I = 0; I < P.PreconditionCount && I < EntryAssumes.size(); ++I)
-      M.Preconditions.push_back(cloneVCExpr(EntryAssumes[I].get()));
+      M.Preconditions.push_back(cloneLogicExpr(EntryAssumes[I].get()));
 
     auto makeGoal = [&](const VCExpr *Condition) -> std::unique_ptr<VCExpr> {
-      std::unique_ptr<VCExpr> ConditionWP = cloneVCExpr(Condition);
+      std::unique_ptr<VCExpr> ConditionWP = cloneLogicExpr(Condition);
       for (auto It = Assumptions.rbegin(); It != Assumptions.rend(); ++It) {
         ConditionWP =
-            vcOr(vcNot(cloneVCExpr(It->first)), std::move(ConditionWP));
+            vcOr(vcNot(cloneLogicExpr(It->first)), std::move(ConditionWP));
         if (ConditionWP->K == VCExpr::Or)
           ConditionWP->Premise = It->second.empty() ? "fact" : It->second;
       }
@@ -2312,7 +2297,7 @@ class ObligationBuilder {
       Item.TraceEventCount = TraceEventCount;
       Item.Id = Identity + "::obligation:" + std::to_string(++ObligationIndex);
       Item.Goal = makeGoal(Condition);
-      Item.CounterexampleQuery = vcNot(cloneVCExpr(Item.Goal.get()));
+      Item.CounterexampleQuery = vcNot(cloneLogicExpr(Item.Goal.get()));
       Item.CounterexampleQuery->Loc = Condition->Loc;
       Item.CounterexampleQuery->EndLoc = Condition->EndLoc;
       M.Obligations.push_back(std::move(Item));
@@ -2322,7 +2307,7 @@ class ObligationBuilder {
       if (Stmt.Kind == PassiveStmt::Assume) {
         Assumptions.emplace_back(Stmt.Cond.get(), Stmt.Origin);
         if (Stmt.Theorem)
-          M.Theorems.push_back(cloneVCExpr(Stmt.Cond.get()));
+          M.Theorems.push_back(cloneLogicExpr(Stmt.Cond.get()));
         continue;
       }
       appendObligation(Stmt.ProofKind, Stmt.Cond.get(), Stmt.TraceEventCount,
@@ -2332,7 +2317,7 @@ class ObligationBuilder {
       appendObligation(Kind, Exit.get(), M.TraceEvents.size(), Note);
 
     M.CorrectnessGoal = buildCompleteGoal(M.Obligations);
-    M.CounterexampleQuery = vcNot(cloneVCExpr(M.CorrectnessGoal.get()));
+    M.CounterexampleQuery = vcNot(cloneLogicExpr(M.CorrectnessGoal.get()));
 
     SpecAxiomContext AxiomContext{P.SpecFunctions, P.SpecFuel, P.HiddenSpecs,
                                   P.RevealedSpecs};

From 475877be6c3fcea1b7f74c3a791aefdd55ea73d8 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:28 +0530
Subject: [PATCH 04/14] verify: Rewrite shared terms copy-on-write in the
 certifier.

---
 clang/lib/Verify/Backend/Certify.cpp | 195 +++++++++++++++++----------
 1 file changed, 122 insertions(+), 73 deletions(-)

diff --git a/clang/lib/Verify/Backend/Certify.cpp b/clang/lib/Verify/Backend/Certify.cpp
index 4a7002032f..55df72c841 100644
--- a/clang/lib/Verify/Backend/Certify.cpp
+++ b/clang/lib/Verify/Backend/Certify.cpp
@@ -922,10 +922,9 @@ class Evaluator {
   static bool mentions(const LogicExpr *E, const std::string &Binder) {
     if (E->K == LogicExpr::Var)
       return E->Name == Binder;
-    return llvm::any_of(E->Children,
-                        [&](const std::unique_ptr<LogicExpr> &Child) {
-                          return mentions(Child.get(), Binder);
-                        });
+    return llvm::any_of(E->Children, [&](const LogicExprRef &Child) {
+      return mentions(Child.get(), Binder);
+    });
   }
 
   /// Built from the binder by exact integer +, -, negation, and scaling.
@@ -1215,10 +1214,9 @@ class Evaluator {
         E->K == LogicExpr::Exists || E->K == LogicExpr::SpecCall ||
         E->K == LogicExpr::Store || E->K == LogicExpr::HeapFrame)
       return false;
-    return llvm::all_of(
-        E->Children, [&](const std::unique_ptr<LogicExpr> &Child) {
-          return binderReads(Child.get(), Binder, Loads, Comparisons);
-        });
+    return llvm::all_of(E->Children, [&](const LogicExprRef &Child) {
+      return binderReads(Child.get(), Binder, Loads, Comparisons);
+    });
   }
 
   /// The binder values in [Low, High) at which some load of the body reads a
@@ -1416,7 +1414,7 @@ class Evaluator {
   bool mentionsSymbolic(const LogicExpr *E) const {
     if (E->K == LogicExpr::Var && symbolicName(E->Name))
       return true;
-    return llvm::any_of(E->Children, [&](const std::unique_ptr<LogicExpr> &C) {
+    return llvm::any_of(E->Children, [&](const LogicExprRef &C) {
       return mentionsSymbolic(C.get());
     });
   }
@@ -1780,7 +1778,7 @@ class Evaluator {
   /// The binder values around which a comparison of \p E's body, affine in
   /// the binder once applications at it are unfolded, changes.
   std::set<CertInt> candidateWitnesses(const LogicExpr *E) {
-    std::vector<std::unique_ptr<LogicExpr>> Unfolded;
+    std::vector<LogicExprRef> Unfolded;
     std::vector<const LogicExpr *> Comparisons;
     std::function<void(const LogicExpr *)> collect = [&](const LogicExpr *C) {
       switch (C->K) {
@@ -2208,41 +2206,73 @@ class Evaluator {
       namesIn(Child.get(), Out);
   }
 
+  /// Calls \p Rewrite with the index and a slot for each child of \p E, or
+  /// each pattern when \p Patterns. E's children are shared with other
+  /// terms, so E is copied, once, only if a slot changes.
+  template <typename Fn>
+  static void rewriteSlots(LogicExprRef &E, bool Patterns, Fn Rewrite) {
+    const std::vector<LogicExprRef> &Slots =
+        Patterns ? E->Patterns : E->Children;
+    std::unique_ptr<LogicExpr> Copy;
+    for (size_t I = 0, N = Slots.size(); I != N; ++I) {
+      LogicExprRef Slot = Slots[I];
+      Rewrite(I, Slot);
+      if (Slot == Slots[I])
+        continue;
+      if (!Copy)
+        Copy = cloneLogicExpr(E.get());
+      (Patterns ? Copy->Patterns : Copy->Children)[I] = std::move(Slot);
+    }
+    if (Copy)
+      E = LogicExprRef(std::move(Copy));
+  }
+
   /// Renames the occurrences of \p From in \p E that are not bound below
   /// it to \p To.
-  static void rename(LogicExpr *E, const std::string &From,
+  static void rename(LogicExprRef &E, const std::string &From,
                      const std::string &To) {
-    if (E->K == LogicExpr::Var && E->Name == From) {
-      E->Name = To;
+    if (E->K == LogicExpr::Var) {
+      if (E->Name == From) {
+        std::unique_ptr<LogicExpr> Copy = cloneLogicExpr(E.get());
+        Copy->Name = To;
+        E = LogicExprRef(std::move(Copy));
+      }
       return;
     }
     const bool Binds =
         (E->K == LogicExpr::Forall || E->K == LogicExpr::Exists) &&
         E->Binder == From;
-    for (size_t I = 0; I != E->Children.size(); ++I)
-      if (!Binds || I + 1 != E->Children.size())
-        rename(E->Children[I].get(), From, To);
+    const size_t Body = E->Children.size() - 1;
+    rewriteSlots(E, false, [&](size_t I, LogicExprRef &Child) {
+      if (!Binds || I != Body)
+        rename(Child, From, To);
+    });
     if (!Binds)
-      for (auto &Pattern : E->Patterns)
-        rename(Pattern.get(), From, To);
+      rewriteSlots(E, true, [&](size_t, LogicExprRef &Pattern) {
+        rename(Pattern, From, To);
+      });
   }
 
   /// Substitutes \p Map in \p E. A binder that a substituted value mentions
   /// is renamed apart first, since the value would be captured otherwise.
-  static void substitute(std::unique_ptr<LogicExpr> &E,
+  static void substitute(LogicExprRef &E,
                          const std::map<std::string, const LogicExpr *> &Map) {
     if (E->K == LogicExpr::Var)
       if (auto It = Map.find(E->Name); It != Map.end()) {
-        E = cloneLogicExpr(It->second);
+        E = LogicExprRef(cloneLogicExpr(It->second));
         return;
       }
+    const size_t Body = E->Children.size() - 1;
     if (E->K != LogicExpr::Forall && E->K != LogicExpr::Exists) {
-      for (auto &Child : E->Children)
+      rewriteSlots(E, false, [&](size_t, LogicExprRef &Child) {
         substitute(Child, Map);
+      });
       return;
     }
-    for (size_t I = 0; I + 1 < E->Children.size(); ++I)
-      substitute(E->Children[I], Map);
+    rewriteSlots(E, false, [&](size_t I, LogicExprRef &Child) {
+      if (I != Body)
+        substitute(Child, Map);
+    });
     std::map<std::string, const LogicExpr *> Inner = Map;
     Inner.erase(E->Binder);
     std::set<std::string> Taken;
@@ -2253,12 +2283,17 @@ class Evaluator {
       std::string Binder = E->Binder;
       for (unsigned N = 1; Taken.count(Binder); ++N)
         Binder = E->Binder + "." + std::to_string(N);
-      rename(E->Children.back().get(), E->Binder, Binder);
-      for (auto &Pattern : E->Patterns)
-        rename(Pattern.get(), E->Binder, Binder);
-      E->Binder = Binder;
-    }
-    substitute(E->Children.back(), Inner);
+      std::unique_ptr<LogicExpr> Copy = cloneLogicExpr(E.get());
+      rename(Copy->Children.back(), E->Binder, Binder);
+      for (auto &Pattern : Copy->Patterns)
+        rename(Pattern, E->Binder, Binder);
+      Copy->Binder = Binder;
+      E = LogicExprRef(std::move(Copy));
+    }
+    rewriteSlots(E, false, [&](size_t I, LogicExprRef &Child) {
+      if (I == Body)
+        substitute(Child, Inner);
+    });
   }
 
   static std::unique_ptr<LogicExpr> falseTerm() {
@@ -2271,7 +2306,7 @@ class Evaluator {
   static bool appliesAt(const LogicExpr *E, const std::string &Binder) {
     if (E->K == LogicExpr::SpecCall && mentions(E, Binder))
       return true;
-    return llvm::any_of(E->Children, [&](const std::unique_ptr<LogicExpr> &C) {
+    return llvm::any_of(E->Children, [&](const LogicExprRef &C) {
       return appliesAt(C.get(), Binder);
     });
   }
@@ -2280,8 +2315,8 @@ class Evaluator {
   /// definition, an equation: \p Depth levels deep, of which \p Recursive
   /// may unfold recursive functions, while the term stays within \p Budget
   /// nodes.
-  void inlineAt(std::unique_ptr<LogicExpr> &E, const std::string &Binder,
-                unsigned Depth, unsigned Recursive, uint64_t &Budget) {
+  void inlineAt(LogicExprRef &E, const std::string &Binder, unsigned Depth,
+                unsigned Recursive, uint64_t &Budget) {
     if (E->K == LogicExpr::SpecCall && Depth && mentions(E.get(), Binder))
       if (const LogicFunctionDecl *Function = function(E->SpecCallee);
           Function && Function->StepDefinition && !Function->Choice &&
@@ -2291,8 +2326,7 @@ class Evaluator {
         Budget -= countTerms(Function->StepDefinition.get());
         if (!nonRecursive().count(Function->Identity))
           --Recursive;
-        std::unique_ptr<LogicExpr> Body =
-            cloneLogicExpr(Function->StepDefinition.get());
+        LogicExprRef Body(cloneLogicExpr(Function->StepDefinition.get()));
         std::map<std::string, const LogicExpr *> Map;
         for (size_t I = 0; I != E->Children.size(); ++I)
           Map[Function->Parameters[I].Name] = E->Children[I].get();
@@ -2301,8 +2335,9 @@ class Evaluator {
         inlineAt(E, Binder, Depth - 1, Recursive, Budget);
         return;
       }
-    for (auto &Child : E->Children)
+    rewriteSlots(E, false, [&](size_t, LogicExprRef &Child) {
       inlineAt(Child, Binder, Depth, Recursive, Budget);
+    });
   }
 
   const std::set<std::string> &nonRecursive() {
@@ -2322,7 +2357,7 @@ class Evaluator {
   /// where \p E is monotone in it (\p Positive) and false where antitone,
   /// so that E implies the result. False when one occurs where E is
   /// neither.
-  static bool approximate(std::unique_ptr<LogicExpr> &E, bool Positive,
+  static bool approximate(LogicExprRef &E, bool Positive,
                           const std::string &Binder) {
     if (!appliesAt(E.get(), Binder))
       return true;
@@ -2330,26 +2365,35 @@ class Evaluator {
     case LogicExpr::SpecCall:
       if (E->Sort.Kind != LogicSortKind::Bool)
         return false;
-      E = Positive ? trueTerm() : falseTerm();
+      E = LogicExprRef(Positive ? trueTerm() : falseTerm());
       return true;
     case LogicExpr::Not:
-      return approximate(E->Children[0], !Positive, Binder);
     case LogicExpr::And:
-    case LogicExpr::Or:
-      return llvm::all_of(E->Children, [&](std::unique_ptr<LogicExpr> &C) {
-        return approximate(C, Positive, Binder);
+    case LogicExpr::Or: {
+      const bool Inner = E->K == LogicExpr::Not ? !Positive : Positive;
+      bool Approximated = true;
+      rewriteSlots(E, false, [&](size_t, LogicExprRef &C) {
+        Approximated = Approximated && approximate(C, Inner, Binder);
       });
-    case LogicExpr::Ite:
-      return E->Sort.Kind == LogicSortKind::Bool &&
-             !appliesAt(E->Children[0].get(), Binder) &&
-             approximate(E->Children[1], Positive, Binder) &&
-             approximate(E->Children[2], Positive, Binder);
+      return Approximated;
+    }
+    case LogicExpr::Ite: {
+      if (E->Sort.Kind != LogicSortKind::Bool ||
+          appliesAt(E->Children[0].get(), Binder))
+        return false;
+      bool Approximated = true;
+      rewriteSlots(E, false, [&](size_t I, LogicExprRef &C) {
+        Approximated =
+            Approximated && (I == 0 || approximate(C, Positive, Binder));
+      });
+      return Approximated;
+    }
     case LogicExpr::Forall:
     case LogicExpr::Exists:
       // A condition in a monotone position may become true, in an antitone
       // one false: a quantifier over the binder is one the analysis below
       // cannot read.
-      E = Positive ? trueTerm() : falseTerm();
+      E = LogicExprRef(Positive ? trueTerm() : falseTerm());
       return true;
     default:
       return false;
@@ -2358,7 +2402,7 @@ class Evaluator {
 
   /// Replaces each condition of \p E that does not mention \p Binder by its
   /// value, and simplifies the connectives over them.
-  void fold(std::unique_ptr<LogicExpr> &E, const std::string &Binder) {
+  void fold(LogicExprRef &E, const std::string &Binder) {
     if (E->Sort.Kind != LogicSortKind::Bool)
       return;
     if (!mentions(E.get(), Binder)) {
@@ -2373,38 +2417,40 @@ class Evaluator {
         }
         return;
       }
-      E = *Holds ? trueTerm() : falseTerm();
+      E = LogicExprRef(*Holds ? trueTerm() : falseTerm());
       return;
     }
     switch (E->K) {
     case LogicExpr::Not:
-      fold(E->Children[0], Binder);
+      rewriteSlots(E, false,
+                   [&](size_t, LogicExprRef &Child) { fold(Child, Binder); });
       if (E->Children[0]->K == LogicExpr::True)
-        E = falseTerm();
+        E = LogicExprRef(falseTerm());
       else if (E->Children[0]->K == LogicExpr::False)
-        E = trueTerm();
+        E = LogicExprRef(trueTerm());
       return;
     case LogicExpr::And:
     case LogicExpr::Or: {
       const bool And = E->K == LogicExpr::And;
-      for (auto &Child : E->Children) {
-        fold(Child, Binder);
-        if (Child->K == (And ? LogicExpr::False : LogicExpr::True)) {
-          E = And ? falseTerm() : trueTerm();
+      bool Decided = false;
+      rewriteSlots(E, false, [&](size_t, LogicExprRef &Child) {
+        if (Decided)
           return;
-        }
-      }
+        fold(Child, Binder);
+        Decided = Child->K == (And ? LogicExpr::False : LogicExpr::True);
+      });
+      if (Decided)
+        E = LogicExprRef(And ? falseTerm() : trueTerm());
       return;
     }
     case LogicExpr::Ite:
-      fold(E->Children[0], Binder);
-      fold(E->Children[1], Binder);
-      fold(E->Children[2], Binder);
+      rewriteSlots(E, false,
+                   [&](size_t, LogicExprRef &Child) { fold(Child, Binder); });
       if (E->Children[0]->K == LogicExpr::True) {
-        std::unique_ptr<LogicExpr> Then = std::move(E->Children[1]);
+        LogicExprRef Then = E->Children[1];
         E = std::move(Then);
       } else if (E->Children[0]->K == LogicExpr::False) {
-        std::unique_ptr<LogicExpr> Else = std::move(E->Children[2]);
+        LogicExprRef Else = E->Children[2];
         E = std::move(Else);
       }
       return;
@@ -2436,7 +2482,7 @@ class Evaluator {
     if (!Failure.empty())
       return std::nullopt;
     std::unique_ptr<LogicExpr> Probe = cloneLogicExpr(Q);
-    std::unique_ptr<LogicExpr> &Body = Probe->Children.back();
+    LogicExprRef &Body = Probe->Children.back();
     if (Negated) {
       auto Not = std::make_unique<LogicExpr>(LogicExpr::Not);
       Not->Sort = LogicSort::boolSort();
@@ -2518,7 +2564,7 @@ class Evaluator {
       return false;
     if (E->K == LogicExpr::SpecCall && Group.count(E->SpecCallee))
       return true;
-    return llvm::any_of(E->Children, [&](const std::unique_ptr<LogicExpr> &C) {
+    return llvm::any_of(E->Children, [&](const LogicExprRef &C) {
       return appliesAny(C.get(), Group);
     });
   }
@@ -3604,16 +3650,19 @@ class Evaluator {
     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);
+    std::function<void(LogicExprRef &)> rename = [&](LogicExprRef &E) {
+      if (E->K == LogicExpr::Var && Names.count(E->Name)) {
+        std::unique_ptr<LogicExpr> Copy = cloneLogicExpr(E.get());
+        Copy->Name += Suffix;
+        E = LogicExprRef(std::move(Copy));
+      }
+      rewriteSlots(E, false,
+                   [&](size_t, LogicExprRef &Child) { rename(Child); });
     };
     auto second = [&](const LogicExpr &E) {
-      std::unique_ptr<LogicExpr> Copy = cloneLogicExpr(&E);
-      rename(*Copy);
-      return Copy;
+      LogicExprRef Renamed(cloneLogicExpr(&E));
+      rename(Renamed);
+      return cloneLogicExpr(Renamed.get());
     };
     // The choice's own quantifier: its bounds, then its body at every value
     // in range.

From f37977171236b71abaf089bbc3e07b0e8f5bc7e8 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:29 +0530
Subject: [PATCH 05/14] verify: Take a shared subterm as a root of its own in
 the Z3 adapter.

---
 clang/lib/Verify/Backend/Z3Encode.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp
index 979c920828..d1c13b6fc1 100644
--- a/clang/lib/Verify/Backend/Z3Encode.cpp
+++ b/clang/lib/Verify/Backend/Z3Encode.cpp
@@ -82,7 +82,7 @@ bool containsQuantifier(const VCExpr *E) {
       E->K == VCExpr::HeapFrame)
     return true;
   return std::any_of(E->Children.begin(), E->Children.end(),
-                     [](const std::unique_ptr<VCExpr> &Child) {
+                     [](const LogicExprRef &Child) {
                        return containsQuantifier(Child.get());
                      });
 }
@@ -2600,7 +2600,7 @@ bool appliesDefined(const LogicExpr *E,
   if (!IntoQuantifiers &&
       (E->K == LogicExpr::Forall || E->K == LogicExpr::Exists))
     return false;
-  return llvm::any_of(E->Children, [&](const std::unique_ptr<LogicExpr> &C) {
+  return llvm::any_of(E->Children, [&](const LogicExprRef &C) {
     return appliesDefined(C.get(), Defined, IntoQuantifiers);
   });
 }
@@ -2636,8 +2636,9 @@ guardRecursion(const LogicExpr *E,
     Tail->Sort = E->Sort;
     for (size_t I = From; I != E->Children.size(); ++I)
       Tail->Children.push_back(cloneLogicExpr(E->Children[I].get()));
-    return Tail->Children.size() == 1 ? std::move(Tail->Children.front())
-                                      : std::move(Tail);
+    if (Tail->Children.size() == 1)
+      return cloneLogicExpr(Tail->Children.front().get());
+    return Tail;
   };
   switch (E->K) {
   case LogicExpr::And:
@@ -2685,7 +2686,7 @@ bool recursionGuarded(const LogicExpr *E, bool InBranch,
     return InBranch || !appliesDefined(E, Defined);
   if (E->K == LogicExpr::SpecCall && Defined(E->SpecCallee) && !InBranch)
     return false;
-  return llvm::all_of(E->Children, [&](const std::unique_ptr<LogicExpr> &C) {
+  return llvm::all_of(E->Children, [&](const LogicExprRef &C) {
     return recursionGuarded(C.get(), InBranch, Defined);
   });
 }

From 8fbc97e7c57a23f61f6bf492d100ef46fa4a97ed Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:29 +0530
Subject: [PATCH 06/14] verify: Name a subterm a Lean statement shares once.

---
 clang/lib/Verify/Backend/LeanBackend.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp
index f594870e97..98eda10f5b 100644
--- a/clang/lib/Verify/Backend/LeanBackend.cpp
+++ b/clang/lib/Verify/Backend/LeanBackend.cpp
@@ -687,7 +687,9 @@ static unsigned collectLeanTemporaries(const LogicExpr *Expression,
     for (const auto &Child : Expression->Children)
       Size += collectLeanTemporaries(Child.get(), Nodes);
   if (!IsRoot && Size >= 128) {
-    Nodes.push_back(Expression);
+    // A subterm shared by several places is named once.
+    if (!llvm::is_contained(Nodes, Expression))
+      Nodes.push_back(Expression);
     return 1;
   }
   return Size;

From fe0b958641508221e7385844e969a28896457b36 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:29 +0530
Subject: [PATCH 07/14] verify: Annotate each shared node once, writing only a
 source that differs.

---
 clang/lib/Verify/Driver/Verifier.cpp | 40 ++++++++++++++++++----------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index 2a046c752f..f317e60815 100644
--- a/clang/lib/Verify/Driver/Verifier.cpp
+++ b/clang/lib/Verify/Driver/Verifier.cpp
@@ -28,6 +28,7 @@
 #include "clang/AST/ASTContext.h"
 #include "clang/Basic/SourceManager.h"
 #include "clang/Frontend/TextDiagnostic.h"
+#include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/ScopeExit.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/SmallVector.h"
@@ -1546,30 +1547,41 @@ class Verifier {
       PresumedLoc Location = SourceMgr.getPresumedLoc(Loc);
       if (!Location.isValid())
         return;
-      Source.File = Location.getFilename();
-      Source.Line = Location.getLine();
-      Source.Column = Location.getColumn();
+      ObligationSource Found;
+      Found.File = Location.getFilename();
+      Found.Line = Location.getLine();
+      Found.Column = Location.getColumn();
       PresumedLoc End =
           SourceMgr.getPresumedLoc(EndLoc.isValid() ? EndLoc : Loc);
-      if (End.isValid() && Source.File == End.getFilename() &&
-          (End.getLine() > Source.Line || (End.getLine() == Source.Line &&
-                                           End.getColumn() >= Source.Column))) {
-        Source.EndLine = End.getLine();
-        Source.EndColumn = End.getColumn();
+      if (End.isValid() && Found.File == End.getFilename() &&
+          (End.getLine() > Found.Line ||
+           (End.getLine() == Found.Line && End.getColumn() >= Found.Column))) {
+        Found.EndLine = End.getLine();
+        Found.EndColumn = End.getColumn();
       } else {
-        Source.EndLine = Source.Line;
-        Source.EndColumn = Source.Column;
+        Found.EndLine = Found.Line;
+        Found.EndColumn = Found.Column;
       }
+      // A term shared with a module annotated before, which other threads
+      // may be reading, is read and not written.
+      if (Source.File != Found.File || Source.Line != Found.Line ||
+          Source.Column != Found.Column || Source.EndLine != Found.EndLine ||
+          Source.EndColumn != Found.EndColumn)
+        Source = std::move(Found);
     };
-    auto annotateExpr = [&](LogicExpr *Root) {
+    // Terms share subterms: each node once.
+    llvm::DenseSet<const LogicExpr *> Annotated;
+    auto annotateExpr = [&](const LogicExpr *Root) {
       if (!Root)
         return;
-      std::vector<LogicExpr *> Pending = {Root};
+      std::vector<const LogicExpr *> Pending = {Root};
       while (!Pending.empty()) {
-        LogicExpr *Expr = Pending.back();
+        const LogicExpr *Expr = Pending.back();
         Pending.pop_back();
+        if (!Annotated.insert(Expr).second)
+          continue;
         annotateSource(Expr->Loc, Expr->EndLoc, Expr->Source);
-        for (auto &Child : Expr->Children)
+        for (const auto &Child : Expr->Children)
           if (Child)
             Pending.push_back(Child.get());
       }

From ade24192aa43a844dd9c5db8c67234091dd21f9a Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:30 +0530
Subject: [PATCH 08/14] test: Build shared children in the certifier unit
 tests.

---
 clang/unittests/Verify/CertifyTest.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/clang/unittests/Verify/CertifyTest.cpp b/clang/unittests/Verify/CertifyTest.cpp
index 47e19463d3..5a076f1329 100644
--- a/clang/unittests/Verify/CertifyTest.cpp
+++ b/clang/unittests/Verify/CertifyTest.cpp
@@ -73,7 +73,8 @@ Expr variable(llvm::StringRef Name, LogicSort Sort) {
 
 Expr node(LogicExpr::Kind Kind, LogicSort Sort, std::vector<Expr> Children) {
   Expr E = leaf(Kind, Sort);
-  E->Children = std::move(Children);
+  for (Expr &Child : Children)
+    E->Children.push_back(std::move(Child));
   return E;
 }
 

From a08ebb1891bd19996909ed6e5b4b218204ce9024 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:30 +0530
Subject: [PATCH 09/14] test: Build shared children in the encoding unit tests.

---
 clang/unittests/Verify/MachineIntegerEncodingTest.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/clang/unittests/Verify/MachineIntegerEncodingTest.cpp b/clang/unittests/Verify/MachineIntegerEncodingTest.cpp
index f18f0bb565..f3dae6a0fa 100644
--- a/clang/unittests/Verify/MachineIntegerEncodingTest.cpp
+++ b/clang/unittests/Verify/MachineIntegerEncodingTest.cpp
@@ -60,7 +60,8 @@ Expr variable(llvm::StringRef Name, LogicSort Sort) {
 
 Expr node(LogicExpr::Kind Kind, LogicSort Sort, std::vector<Expr> Children) {
   Expr E = leaf(Kind, Sort);
-  E->Children = std::move(Children);
+  for (Expr &Child : Children)
+    E->Children.push_back(std::move(Child));
   return E;
 }
 

From cd40566da5f5fa51eaa90b646d59e46f23b11b89 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:31 +0530
Subject: [PATCH 10/14] test: Add a check that a Lean statement binds each let
 name once.

---
 .../Verify/suite/Inputs/lean_let_names.py     | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 clang/test/Verify/suite/Inputs/lean_let_names.py

diff --git a/clang/test/Verify/suite/Inputs/lean_let_names.py b/clang/test/Verify/suite/Inputs/lean_let_names.py
new file mode 100644
index 0000000000..87ef6ac3d7
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/lean_let_names.py
@@ -0,0 +1,20 @@
+"""Prints how many theorems of a Lean export bind one name twice in the lets
+their statement starts with: a subterm shared by several places of a
+statement is named once."""
+import re
+import sys
+
+twice = 0
+for theorem in re.split(r"(?m)^(?=theorem )", open(sys.argv[1]).read()):
+    lines = theorem.splitlines()
+    start = next((i for i, l in enumerate(lines) if "(let __cppverify_term_" in l), None)
+    if start is None:
+        continue
+    names = re.findall(r"\(let (__cppverify_term_\d+) :", lines[start])[:1]
+    for line in lines[start + 1:]:
+        bound = re.match(r"  let (__cppverify_term_\d+) :", line)
+        if not bound:
+            break
+        names.append(bound.group(1))
+    twice += len(names) != len(set(names))
+print(f"statements that bind a let name twice: {twice}")

From 9f45057e6922659ca76d48664df2d22e5451df26 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:31 +0530
Subject: [PATCH 11/14] test: Check that the case studies lower within 2 GB of
 address space.

---
 .../test/Verify/suite/shared_logic_terms.test | 35 +++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 clang/test/Verify/suite/shared_logic_terms.test

diff --git a/clang/test/Verify/suite/shared_logic_terms.test b/clang/test/Verify/suite/shared_logic_terms.test
new file mode 100644
index 0000000000..53b963ce24
--- /dev/null
+++ b/clang/test/Verify/suite/shared_logic_terms.test
@@ -0,0 +1,35 @@
+# REQUIRES: system-linux
+# UNSUPPORTED: msan, asan, hwasan
+#
+# Each check of a function states every assumption before it, and its query,
+# the function's complete goal, and that goal's query state the checks again.
+# Terms share these subterms rather than copying them, so a module grows with
+# what it says, not with how often its checks repeat it: lowering the ULEB128
+# case study took 12.8 GB of address space when each was a copy, and
+# safe_fib.cpp 4.7 GB. Both now lower within 2 GB.
+# RUN: ulimit -v 2000000
+# RUN: %cpp-verify --lower-only --jobs=1 %S/llvm_uleb128.cpp -- 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=ULEB
+# RUN: %cpp-verify --lower-only --jobs=1 %S/safe_fib.cpp -- 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=FIB
+#
+# A subterm that several goals share is simplified once; its rewrites still
+# count once for each place, as when each was a copy (main printed 265 here).
+# RUN: %cpp-verify --lower-only --jobs=1 --dump-ir=3 \
+# RUN:   %S/backend_counterexample_trace.cpp -- 2>&1 | FileCheck %s --check-prefix=REWRITES
+#
+# The Lean printer names each large subterm of a statement with a let; one
+# that several places share is named once, rather than once per place.
+# RUN: %cpp-verify --backend=lean --lean-out=%t.lean %S/llvm_uleb128.cpp --
+# RUN: %python %S/Inputs/lean_let_names.py %t.lean | FileCheck %s --check-prefix=LETS
+
+ULEB: Lowered: encode_uleb128
+ULEB: Lowered: decode_uleb128_canonical
+ULEB: Lowered: roundtrip_uleb128
+
+FIB: Lowered: iterative_fibonacci
+
+REWRITES: vc set_value
+REWRITES: simplification nodes 3632 -> 1252, rewrites 265, functions-removed 0
+
+LETS: statements that bind a let name twice: 0

From 6f82cfafdcaa02e6e170c7c76718992070094a21 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:31 +0530
Subject: [PATCH 12/14] docs: Describe shared logic subterms in the
 architecture.

---
 docs/ARCHITECTURE.md | 41 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 40 insertions(+), 1 deletion(-)

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index a4b444b589..e2ed48978b 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -539,7 +539,8 @@ memory checks where they are checked.
 `buildObligationModule` is the only passive-to-logic lowering path. It folds the
 ordered `PassiveProgram` once and publishes:
 
-- a typed `LogicExpr` tree with explicit `Bool`, mathematical integer,
+- typed `LogicExpr` terms, whose subterms are shared (below), with explicit
+  `Bool`, mathematical integer,
   width-indexed bit-vector, pointer, heap-array, and collection (`seq`, `set`,
   `multiset`, `map`) sorts; integer sorts retain
   canonical signedness and originating C++ width for explicit mode conversion,
@@ -565,6 +566,44 @@ Construction returns `llvm::Expected`. A null, unhandled, malformed, or
 untyped term prevents publication of the module and is reported as `unknown`;
 it is never replaced by `true`.
 
+**Shared subterms.** A term owns its root and shares its subterms: the
+children and patterns of a `LogicExpr` are `LogicExprRef`s
+(`llvm::IntrusiveRefCntPtr<const LogicExpr>`, the count in the node), and no
+code changes a node once it is a subterm, which the type enforces. A copy
+(`cloneLogicExpr`) copies the root's fields and shares its children. So each
+obligation's goal states every assumption before it, its query negates the
+goal, and the complete goal conjoins the goals, all without copying them, as
+Verus's AIR shares `Arc<ExprX>`, Frama-C's Qed hash-conses its terms, and
+Lean shares `Expr`. A change below a root rebuilds only the path to it. The
+simplifier is copy-on-write and memoizes each subterm per module, so a
+subterm that many goals share is simplified once and stays shared; a reuse
+adds the rewrites its first simplification counted, so the reported
+statistics are those of the tree. The certifier's substitution, renaming,
+and witness analysis rewrite children the same way (`rewriteSlots`), copying
+a node only when a child changes. The one field written after a term is
+shared is a node's `Source`, a function of its `Loc` alone: annotation visits
+each node once and writes only a value that differs, so it never writes a
+node that an earlier, annotated module shares, which other threads may be
+reading. The caches keyed by a node's address hold what depends on the node
+alone, so sharing cannot make them answer for another place: the Z3
+encoding (a variable is encoded by its name, and the traversal keeps no
+scope), the certifier's cost estimate, and the Lean printer's `let`s, which
+name a shared subterm of a statement once. Every hash, archive, and Layer 3
+and 4 dump is what it was with copies (checked on every Verify source), and
+the Lean exports state definitionally equal goals.
+
+Before 0.2 every copy copied the whole term. Each obligation's goal repeated
+its assumptions, and its query, the complete goal, and the complete query
+repeated those, so memory grew with the number of obligations times what
+came before them: lowering the ULEB128 case study took 12.8 GB of address
+space and 53 s, verifying it 14.9 GB with eight jobs (`--jobs=8`, more than
+a 16 GB CI runner holds beside the tests running with it), and lowering
+`safe_fib.cpp` 4.7 GB and 16 s. They now take 0.43 GB and 10 s, 0.9 GB, and
+0.35 GB and 7 s. The goals still repeat their assumptions as trees, so a
+traversal that does not memoize (validation, hashing, serialization) still
+takes time quadratic in a function's length; hash-consing the terms and
+memoizing those traversals would make it linear.
+
 Every source-built or replayed module then passes through one fail-closed
 canonicalization step before hashing or backend dispatch. The pass folds only
 sort-preserving Boolean constants, double negation, constant conditionals, and

From b927c3df849650ba3f67961bea24c695e33f410e Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:32 +0530
Subject: [PATCH 13/14] docs: State that logic terms share their subterms in
 the design.

---
 docs/DESIGN.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index cf30c31656..2e47c14254 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -1752,6 +1752,13 @@ signedness and the originating C++ width needed by explicit
 machine/mathematical conversions; backend adapters derive all representation
 choices from those sorts.
 
+Terms share their subterms, and no code changes a subterm: an obligation's
+goal states every assumption before it, its query negates the goal, and the
+complete goal conjoins the goals, none of them by copying. A module's memory
+therefore grows with what its terms say rather than with how often its
+obligations repeat it; with copies, verifying the ULEB128 case study took
+14.9 GB, and now takes 0.9 GB.
+
 Module construction is fail-closed. Null, unsupported, malformed, or untyped
 terms return an error before backend dispatch. Every free symbol, including
 diagnostic model and trace expressions, has one module-wide logic sort.

From 244286ef5340e309b94d9d10abd1f290d6a2f5cc Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Sat, 24 Oct 2026 03:58:32 +0530
Subject: [PATCH 14/14] docs: Note the memory large functions take in the
 release notes.

---
 website/source/release-notes.rst | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index 89e6c5332f..42ebaaa422 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -292,6 +292,16 @@ quadratic (a 250-term sum lowers in about 5 s instead of 120 s), and an
 expression nested more than 256 operations deep is reported where it is
 (:doc:`language/limitations`).
 
+**Large functions take far less memory.** Each check of a function restated
+every assumption before it as a copy, and the check's query, the function's
+complete goal, and that goal's query copied them again, so memory grew with
+the number of checks times the length of what came before them: verifying the
+ULEB128 case study took 14.9 GB, and lowering it 53 s. Terms now share what
+they repeat: the case study verifies within 0.9 GB and lowers in 10 s, and
+``safe_fib.cpp`` lowers in 7 s within 0.35 GB instead of 16 s and 4.7 GB.
+Verdicts, archives, hashes, and IR dumps are unchanged; a Lean export names a
+large subterm that one statement repeats once (:doc:`case-studies/llvm-uleb128`).
+
 **Errors point at the code.** An error about a construct the verifier does not
 represent named only the function, as in ``error: pick: unsupported statement:
 SwitchStmt``. It now gives the file, line, and column, and shows the line with