diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -16,12 +16,10 @@
 namespace clang::dataflow {
 
 /// The Arena owns the objects that model data within an analysis.
-/// For example, `Value` and `StorageLocation`.
+/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
 class Arena {
 public:
-  Arena()
-      : TrueVal(create<AtomicBoolValue>()),
-        FalseVal(create<AtomicBoolValue>()) {}
+  Arena() : True(makeAtom()), False(makeAtom()) {}
   Arena(const Arena &) = delete;
   Arena &operator=(const Arena &) = delete;
 
@@ -57,33 +55,26 @@
             .get());
   }
 
-  /// Returns a boolean value that represents the conjunction of `LHS` and
-  /// `RHS`. Subsequent calls with the same arguments, regardless of their
-  /// order, will return the same result. If the given boolean values represent
-  /// the same value, the result will be the value itself.
-  BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS);
-
-  /// Returns a boolean value that represents the disjunction of `LHS` and
-  /// `RHS`. Subsequent calls with the same arguments, regardless of their
-  /// order, will return the same result. If the given boolean values represent
-  /// the same value, the result will be the value itself.
-  BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS);
-
-  /// Returns a boolean value that represents the negation of `Val`. Subsequent
-  /// calls with the same argument will return the same result.
-  BoolValue &makeNot(BoolValue &Val);
-
-  /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls
-  /// with the same arguments, will return the same result. If the given boolean
-  /// values represent the same value, the result will be a value that
-  /// represents the true boolean literal.
-  BoolValue &makeImplies(BoolValue &LHS, BoolValue &RHS);
-
-  /// Returns a boolean value that represents `LHS <=> RHS`. Subsequent calls
-  /// with the same arguments, regardless of their order, will return the same
-  /// result. If the given boolean values represent the same value, the result
-  /// will be a value that represents the true boolean literal.
-  BoolValue &makeEquals(BoolValue &LHS, BoolValue &RHS);
+  /// Creates a BoolValue wrapping a particular formula.
+  ///
+  /// Passing in the same formula will result in the same BoolValue.
+  /// FIXME: This canonicalization isn't sound e.g. if we create two BoolValues
+  ///        with the same formula but attach different properties.
+  ///        Stop relying on pointer identity of BoolValues and remove it.
+  BoolValue &makeBoolValue(const Formula &);
+
+  /// Creates a fresh atom and wraps in in an AtomicBoolValue.
+  /// FIXME: For now, identical-address AtomicBoolValue <=> identical atom.
+  ///        Stop relying on pointer identity and remove this guarantee.
+  AtomicBoolValue &makeAtomValue() {
+    return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom())));
+  }
+
+  /// Creates a fresh Top boolean value.
+  TopBoolValue &makeTopValue() {
+    // No need for deduplicating: there's no way to create aliasing Tops.
+    return create<TopBoolValue>(makeAtomRef(makeAtom()));
+  }
 
   /// Returns a symbolic integer value that models an integer literal equal to
   /// `Value`. These literals are the same every time.
@@ -91,27 +82,42 @@
   /// an integer literal is associated with.
   IntegerValue &makeIntLiteral(llvm::APInt Value);
 
-  /// Returns a symbolic boolean value that models a boolean literal equal to
-  /// `Value`. These literals are the same every time.
-  AtomicBoolValue &makeLiteral(bool Value) const {
-    return Value ? TrueVal : FalseVal;
+  // Factories for boolean formulas.
+  // Formulas are interned: passing the same arguments return the same result.
+  // For commutative operations like And/Or, interning ignores order.
+  // Simplifications are applied: makeOr(X, X) => X, etc.
+
+  /// Returns a formula for the conjunction of `LHS` and `RHS`.
+  const Formula &makeAnd(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for the disjunction of `LHS` and `RHS`.
+  const Formula &makeOr(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for the negation of `Val`.
+  const Formula &makeNot(const Formula &Val);
+
+  /// Returns a formula for `LHS => RHS`.
+  const Formula &makeImplies(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for `LHS <=> RHS`.
+  const Formula &makeEquals(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for the variable A.
+  const Formula &makeAtomRef(Atom A);
+
+  /// Returns a formula for a literal true/false.
+  const Formula &makeLiteral(bool Value) {
+    return makeAtomRef(Value ? True : False);
   }
 
+  /// Returns a new atomic boolean variable, distinct from any other.
+  Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
   /// Creates a fresh flow condition and returns a token that identifies it. The
   /// token can be used to perform various operations on the flow condition such
   /// as adding constraints to it, forking it, joining it with another flow
   /// condition, or checking implications.
-  AtomicBoolValue &makeFlowConditionToken() {
-    return create<AtomicBoolValue>();
-  }
-
-  /// Gets the boolean formula equivalent of a BoolValue.
-  /// Each unique Top values is translated to an Atom.
-  /// TODO: migrate to storing Formula directly in Values instead.
-  const Formula &getFormula(const BoolValue &);
-
-  /// Returns a new atomic boolean variable, distinct from any other.
-  Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+  Atom makeFlowConditionToken() { return makeAtom(); }
 
 private:
   llvm::BumpPtrAllocator Alloc;
@@ -123,21 +129,18 @@
   // Indices that are used to avoid recreating the same integer literals and
   // composite boolean values.
   llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
-      ConjunctionVals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
-      DisjunctionVals;
-  llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
-      ImplicationVals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
-      BiconditionalVals;
-
-  llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+  using FormulaPair = std::pair<const Formula *, const Formula *>;
+  llvm::DenseMap<FormulaPair, const Formula *> Ands;
+  llvm::DenseMap<FormulaPair, const Formula *> Ors;
+  llvm::DenseMap<const Formula *, const Formula *> Nots;
+  llvm::DenseMap<FormulaPair, const Formula *> Implies;
+  llvm::DenseMap<FormulaPair, const Formula *> Equals;
+  llvm::DenseMap<Atom, const Formula *> AtomRefs;
+
+  llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
   unsigned NextAtom = 0;
 
-  AtomicBoolValue &TrueVal;
-  AtomicBoolValue &FalseVal;
+  Atom True, False;
 };
 
 } // namespace clang::dataflow
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -137,33 +137,31 @@
   PointerValue &getOrCreateNullPointerValue(QualType PointeeType);
 
   /// Adds `Constraint` to the flow condition identified by `Token`.
-  void addFlowConditionConstraint(AtomicBoolValue &Token,
-                                  BoolValue &Constraint);
+  void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
 
   /// Creates a new flow condition with the same constraints as the flow
   /// condition identified by `Token` and returns its token.
-  AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
+  Atom forkFlowCondition(Atom Token);
 
   /// Creates a new flow condition that represents the disjunction of the flow
   /// conditions identified by `FirstToken` and `SecondToken`, and returns its
   /// token.
-  AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
-                                      AtomicBoolValue &SecondToken);
+  Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
 
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` imply that `Val` is true.
-  bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
+  bool flowConditionImplies(Atom Token, const Formula &);
 
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` are always true.
-  bool flowConditionIsTautology(AtomicBoolValue &Token);
+  bool flowConditionIsTautology(Atom Token);
 
   /// Returns true if `Val1` is equivalent to `Val2`.
   /// Note: This function doesn't take into account constraints on `Val1` and
   /// `Val2` imposed by the flow condition.
-  bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
+  bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
 
-  LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
+  LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
                                           llvm::raw_ostream &OS = llvm::dbgs());
 
   /// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
@@ -200,19 +198,19 @@
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
-      AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
-      llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+      Atom Token, llvm::DenseSet<const Formula *> &Constraints,
+      llvm::DenseSet<Atom> &VisitedTokens);
 
   /// Returns the outcome of satisfiability checking on `Constraints`.
   /// Possible outcomes are:
   /// - `Satisfiable`: A satisfying assignment exists and is returned.
   /// - `Unsatisfiable`: A satisfying assignment does not exist.
   /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+  Solver::Result querySolver(llvm::DenseSet<const Formula *> Constraints);
 
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
-  bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
+  bool isUnsatisfiable(llvm::DenseSet<const Formula *> Constraints) {
     return querySolver(std::move(Constraints)).getStatus() ==
            Solver::Result::Status::Unsatisfiable;
   }
@@ -251,9 +249,8 @@
   // Flow conditions depend on other flow conditions if they are created using
   // `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
   // dependencies is stored in the `FlowConditionDeps` map.
-  llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
-      FlowConditionDeps;
-  llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
+  llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
+  llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
 
   llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts;
 
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -445,29 +445,30 @@
   template <typename T, typename... Args>
   std::enable_if_t<std::is_base_of<Value, T>::value, T &>
   create(Args &&...args) {
-    return DACtx->arena().create<T>(std::forward<Args>(args)...);
+    return arena().create<T>(std::forward<Args>(args)...);
   }
 
   /// Returns a symbolic integer value that models an integer literal equal to
   /// `Value`
   IntegerValue &getIntLiteralValue(llvm::APInt Value) const {
-    return DACtx->arena().makeIntLiteral(Value);
+    return arena().makeIntLiteral(Value);
   }
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`
   AtomicBoolValue &getBoolLiteralValue(bool Value) const {
-    return DACtx->arena().makeLiteral(Value);
+    return cast<AtomicBoolValue>(
+        arena().makeBoolValue(arena().makeLiteral(Value)));
   }
 
   /// Returns an atomic boolean value.
   BoolValue &makeAtomicBoolValue() const {
-    return DACtx->arena().create<AtomicBoolValue>();
+    return arena().makeAtomValue();
   }
 
   /// Returns a unique instance of boolean Top.
   BoolValue &makeTopBoolValue() const {
-    return DACtx->arena().create<TopBoolValue>();
+    return arena().makeTopValue();
   }
 
   /// Returns a boolean value that represents the conjunction of `LHS` and
@@ -475,7 +476,8 @@
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
   BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->arena().makeAnd(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeAnd(LHS.formula(), RHS.formula()));
   }
 
   /// Returns a boolean value that represents the disjunction of `LHS` and
@@ -483,13 +485,14 @@
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
   BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->arena().makeOr(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeOr(LHS.formula(), RHS.formula()));
   }
 
   /// Returns a boolean value that represents the negation of `Val`. Subsequent
   /// calls with the same argument will return the same result.
   BoolValue &makeNot(BoolValue &Val) const {
-    return DACtx->arena().makeNot(Val);
+    return arena().makeBoolValue(arena().makeNot(Val.formula()));
   }
 
   /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
@@ -497,7 +500,8 @@
   /// values represent the same value, the result will be a value that
   /// represents the true boolean literal.
   BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->arena().makeImplies(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeImplies(LHS.formula(), RHS.formula()));
   }
 
   /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
@@ -505,17 +509,22 @@
   /// result. If the given boolean values represent the same value, the result
   /// will be a value that represents the true boolean literal.
   BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->arena().makeEquals(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeEquals(LHS.formula(), RHS.formula()));
   }
 
   /// Returns the token that identifies the flow condition of the environment.
-  AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
+  Atom getFlowConditionToken() const { return FlowConditionToken; }
 
   /// Adds `Val` to the set of clauses that constitute the flow condition.
+  void addToFlowCondition(const Formula &);
+  LLVM_DEPRECATED("Use Formula version instead", "")
   void addToFlowCondition(BoolValue &Val);
 
   /// Returns true if and only if the clauses that constitute the flow condition
   /// imply that `Val` is true.
+  bool flowConditionImplies(const Formula &) const;
+  LLVM_DEPRECATED("Use Formula version instead", "")
   bool flowConditionImplies(BoolValue &Val) const;
 
   /// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
@@ -536,6 +545,8 @@
   /// Returns the `DataflowAnalysisContext` used by the environment.
   DataflowAnalysisContext &getDataflowAnalysisContext() const { return *DACtx; }
 
+  Arena &arena() const { return DACtx->arena(); }
+
   LLVM_DUMP_METHOD void dump() const;
   LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;
 
@@ -603,7 +614,7 @@
                  std::pair<StructValue *, const ValueDecl *>>
       MemberLocToStruct;
 
-  AtomicBoolValue *FlowConditionToken;
+  Atom FlowConditionToken;
 };
 
 /// Returns the storage location for the implicit object of a
diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h
--- a/clang/include/clang/Analysis/FlowSensitive/Value.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Value.h
@@ -15,11 +15,11 @@
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H
 
 #include "clang/AST/Decl.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringMap.h"
 #include "llvm/ADT/StringRef.h"
-#include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <utility>
 
@@ -38,14 +38,10 @@
     Pointer,
     Struct,
 
-    // Synthetic boolean values are either atomic values or logical connectives.
+    // TODO: Top values should not be need to be type-specific.
     TopBool,
     AtomicBool,
-    Conjunction,
-    Disjunction,
-    Negation,
-    Implication,
-    Biconditional,
+    FormulaBool,
   };
 
   explicit Value(Kind ValKind) : ValKind(ValKind) {}
@@ -95,151 +91,68 @@
 
 /// Models a boolean.
 class BoolValue : public Value {
+  const Formula *F;
+
 public:
-  explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
+  explicit BoolValue(Kind ValueKind, const Formula &F)
+      : Value(ValueKind), F(&F) {}
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::TopBool ||
            Val->getKind() == Kind::AtomicBool ||
-           Val->getKind() == Kind::Conjunction ||
-           Val->getKind() == Kind::Disjunction ||
-           Val->getKind() == Kind::Negation ||
-           Val->getKind() == Kind::Implication ||
-           Val->getKind() == Kind::Biconditional;
+           Val->getKind() == Kind::FormulaBool;
   }
+
+  const Formula &formula() const { return *F; }
 };
 
-/// Models the trivially true formula, which is Top in the lattice of boolean
-/// formulas.
+/// A TopBoolValue represents a boolean that is explicitly unconstrained.
+///
+/// This is equivalent to an AtomicBoolValue that does not appear anywhere
+/// else in a system of formula.
+/// Knowing the value is unconstrained is useful when e.g. reasoning about
+/// convergence.
 class TopBoolValue final : public BoolValue {
 public:
-  TopBoolValue() : BoolValue(Kind::TopBool) {}
+  TopBoolValue(const Formula &F) : BoolValue(Kind::TopBool, F) {
+    assert(F.kind() == Formula::AtomRef);
+  }
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::TopBool;
   }
+
+  Atom atom() const { return formula().atom(); }
 };
 
 /// Models an atomic boolean.
+///
+/// FIXME: Merge this class into FormulaBoolValue.
+///        When we want to specify atom identity, use Atom.
 class AtomicBoolValue : public BoolValue {
 public:
-  explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::AtomicBool;
-  }
-};
-
-/// Models a boolean conjunction.
-// FIXME: Consider representing binary and unary boolean operations similar
-// to how they are represented in the AST. This might become more pressing
-// when such operations need to be added for other data types.
-class ConjunctionValue : public BoolValue {
-public:
-  explicit ConjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Conjunction), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Conjunction;
-  }
-
-  /// Returns the left sub-value of the conjunction.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the conjunction.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
-};
-
-/// Models a boolean disjunction.
-class DisjunctionValue : public BoolValue {
-public:
-  explicit DisjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Disjunction), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Disjunction;
+  explicit AtomicBoolValue(const Formula &F) : BoolValue(Kind::AtomicBool, F) {
+    assert(F.kind() == Formula::AtomRef);
   }
 
-  /// Returns the left sub-value of the disjunction.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the disjunction.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
-};
-
-/// Models a boolean negation.
-class NegationValue : public BoolValue {
-public:
-  explicit NegationValue(BoolValue &SubVal)
-      : BoolValue(Kind::Negation), SubVal(SubVal) {}
-
   static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Negation;
+    return Val->getKind() == Kind::AtomicBool;
   }
 
-  /// Returns the sub-value of the negation.
-  BoolValue &getSubVal() const { return SubVal; }
-
-private:
-  BoolValue &SubVal;
+  Atom atom() const { return formula().atom(); }
 };
 
-/// Models a boolean implication.
-///
-/// Equivalent to `!LHS v RHS`.
-class ImplicationValue : public BoolValue {
+/// Models a compound boolean formula.
+class FormulaBoolValue : public BoolValue {
 public:
-  explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Implication;
+  explicit FormulaBoolValue(const Formula &F)
+      : BoolValue(Kind::FormulaBool, F) {
+    assert(F.kind() != Formula::AtomRef && "For now, use AtomicBoolValue");
   }
 
-  /// Returns the left sub-value of the implication.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the implication.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
-};
-
-/// Models a boolean biconditional.
-///
-/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`.
-class BiconditionalValue : public BoolValue {
-public:
-  explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
   static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Biconditional;
+    return Val->getKind() == Kind::FormulaBool;
   }
-
-  /// Returns the left sub-value of the biconditional.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the biconditional.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
 };
 
 /// Models an integer.
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -7,65 +7,75 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
 
 namespace clang::dataflow {
 
-static std::pair<BoolValue *, BoolValue *>
-makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+static std::pair<const Formula *, const Formula *>
+canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
-  if (&RHS < &LHS)
+  if (&RHS < &LHS) // FIXME: use a deterministic order instead
     std::swap(Res.first, Res.second);
   return Res;
 }
 
-BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeAtomRef(Atom A) {
+  auto [It, Inserted] = AtomRefs.try_emplace(A);
+  if (Inserted)
+    It->second =
+        &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+  return *It->second;
+}
+
+const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
   if (&LHS == &RHS)
     return LHS;
 
-  auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
-                                         nullptr);
-  if (Res.second)
-    Res.first->second = &create<ConjunctionValue>(LHS, RHS);
-  return *Res.first->second;
+  auto [It, Inserted] =
+      Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+  return *It->second;
 }
 
-BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
   if (&LHS == &RHS)
     return LHS;
 
-  auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
-                                         nullptr);
-  if (Res.second)
-    Res.first->second = &create<DisjunctionValue>(LHS, RHS);
-  return *Res.first->second;
+  auto [It, Inserted] =
+      Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+  return *It->second;
 }
 
-BoolValue &Arena::makeNot(BoolValue &Val) {
-  auto Res = NegationVals.try_emplace(&Val, nullptr);
-  if (Res.second)
-    Res.first->second = &create<NegationValue>(Val);
-  return *Res.first->second;
+const Formula &Arena::makeNot(const Formula &Val) {
+  auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::Not, {&Val});
+  return *It->second;
 }
 
-BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
   if (&LHS == &RHS)
     return makeLiteral(true);
 
-  auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
-  if (Res.second)
-    Res.first->second = &create<ImplicationValue>(LHS, RHS);
-  return *Res.first->second;
+  auto [It, Inserted] =
+      Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
+  return *It->second;
 }
 
-BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
   if (&LHS == &RHS)
     return makeLiteral(true);
 
-  auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
-                                           nullptr);
-  if (Res.second)
-    Res.first->second = &create<BiconditionalValue>(LHS, RHS);
-  return *Res.first->second;
+  auto [It, Inserted] =
+      Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+  return *It->second;
 }
 
 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
@@ -76,50 +86,13 @@
   return *It->second;
 }
 
-const Formula &Arena::getFormula(const BoolValue &B) {
-  auto It = ValToFormula.find(&B);
-  if (It != ValToFormula.end())
-    return *It->second;
-  Formula &F = [&]() -> Formula & {
-    switch (B.getKind()) {
-    case Value::Kind::Integer:
-    case Value::Kind::Reference:
-    case Value::Kind::Pointer:
-    case Value::Kind::Struct:
-      llvm_unreachable("not a boolean");
-    case Value::Kind::TopBool:
-    case Value::Kind::AtomicBool:
-      // TODO: assign atom numbers on creation rather than in getFormula(), so
-      // they will be deterministic and maybe even meaningful.
-      return Formula::create(Alloc, Formula::AtomRef, {},
-                             static_cast<unsigned>(makeAtom()));
-    case Value::Kind::Conjunction:
-      return Formula::create(
-          Alloc, Formula::And,
-          {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
-           &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
-    case Value::Kind::Disjunction:
-      return Formula::create(
-          Alloc, Formula::Or,
-          {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
-           &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
-    case Value::Kind::Negation:
-      return Formula::create(Alloc, Formula::Not,
-                             {&getFormula(cast<NegationValue>(B).getSubVal())});
-    case Value::Kind::Implication:
-      return Formula::create(
-          Alloc, Formula::Implies,
-          {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
-           &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
-    case Value::Kind::Biconditional:
-      return Formula::create(
-          Alloc, Formula::Equal,
-          {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
-           &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
-    }
-  }();
-  ValToFormula.try_emplace(&B, &F);
-  return F;
+BoolValue &Arena::makeBoolValue(const Formula &F) {
+  auto [It, Inserted] = FormulaValues.try_emplace(&F);
+  if (Inserted)
+    It->second = (F.kind() == Formula::AtomRef)
+                     ? (BoolValue *)&create<AtomicBoolValue>(F)
+                     : &create<FormulaBoolValue>(F);
+  return *It->second;
 }
 
 } // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -98,110 +98,106 @@
 }
 
 void DataflowAnalysisContext::addFlowConditionConstraint(
-    AtomicBoolValue &Token, BoolValue &Constraint) {
-  auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
+    Atom Token, const Formula &Constraint) {
+  auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
   if (!Res.second) {
     Res.first->second =
         &arena().makeAnd(*Res.first->second, Constraint);
   }
 }
 
-AtomicBoolValue &
-DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
-  auto &ForkToken = arena().makeFlowConditionToken();
-  FlowConditionDeps[&ForkToken].insert(&Token);
-  addFlowConditionConstraint(ForkToken, Token);
+Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) {
+  Atom ForkToken = arena().makeFlowConditionToken();
+  FlowConditionDeps[ForkToken].insert(Token);
+  addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
   return ForkToken;
 }
 
-AtomicBoolValue &
-DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
-                                            AtomicBoolValue &SecondToken) {
-  auto &Token = arena().makeFlowConditionToken();
-  FlowConditionDeps[&Token].insert(&FirstToken);
-  FlowConditionDeps[&Token].insert(&SecondToken);
-  addFlowConditionConstraint(
-      Token, arena().makeOr(FirstToken, SecondToken));
+Atom 
+DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
+                                            Atom SecondToken) {
+  Atom Token = arena().makeFlowConditionToken();
+  FlowConditionDeps[Token].insert(FirstToken);
+  FlowConditionDeps[Token].insert(SecondToken);
+  addFlowConditionConstraint(Token,
+                             arena().makeOr(arena().makeAtomRef(FirstToken),
+                                            arena().makeAtomRef(SecondToken)));
   return Token;
 }
 
-Solver::Result
-DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
+Solver::Result DataflowAnalysisContext::querySolver(
+    llvm::DenseSet<const Formula *> Constraints) {
   Constraints.insert(&arena().makeLiteral(true));
-  Constraints.insert(
-      &arena().makeNot(arena().makeLiteral(false)));
-  llvm::DenseSet<const Formula *> Formulas;
-  for (const BoolValue * Constraint : Constraints)
-    Formulas.insert(&arena().getFormula(*Constraint));
-  return S->solve(Formulas);
+  Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
+  return S->solve(Constraints);
 }
 
-bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
-                                                   BoolValue &Val) {
+bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
+                                                   const Formula &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
-  llvm::DenseSet<BoolValue *> Constraints = {&Token,
-                                             &arena().makeNot(Val)};
-  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  llvm::DenseSet<const Formula *> Constraints = {&arena().makeAtomRef(Token),
+                                                 &arena().makeNot(Val)};
+  llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
+bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
-  llvm::DenseSet<BoolValue *> Constraints = {
-      &arena().makeNot(Token)};
-  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  llvm::DenseSet<const Formula *> Constraints = {
+      &arena().makeNot(arena().makeAtomRef(Token))};
+  llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
-                                                   BoolValue &Val2) {
-  llvm::DenseSet<BoolValue *> Constraints = {
+bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
+                                                 const Formula &Val2) {
+  llvm::DenseSet<const Formula *> Constraints = {
       &arena().makeNot(arena().makeEquals(Val1, Val2))};
-  return isUnsatisfiable(Constraints);
+  return isUnsatisfiable(std::move(Constraints));
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
-    AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
-    llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
-  auto Res = VisitedTokens.insert(&Token);
+    Atom Token, llvm::DenseSet<const Formula *> &Constraints,
+    llvm::DenseSet<Atom> &VisitedTokens) {
+  auto Res = VisitedTokens.insert(Token);
   if (!Res.second)
     return;
 
-  auto ConstraintsIt = FlowConditionConstraints.find(&Token);
+  auto ConstraintsIt = FlowConditionConstraints.find(Token);
   if (ConstraintsIt == FlowConditionConstraints.end()) {
-    Constraints.insert(&Token);
+    Constraints.insert(&arena().makeAtomRef(Token));
   } else {
     // Bind flow condition token via `iff` to its set of constraints:
     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
-    Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
+    Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
+                                           *ConstraintsIt->second));
   }
 
-  auto DepsIt = FlowConditionDeps.find(&Token);
+  auto DepsIt = FlowConditionDeps.find(Token);
   if (DepsIt != FlowConditionDeps.end()) {
-    for (AtomicBoolValue *DepToken : DepsIt->second) {
-      addTransitiveFlowConditionConstraints(*DepToken, Constraints,
+    for (Atom DepToken : DepsIt->second) {
+      addTransitiveFlowConditionConstraints(DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
-void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
+void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
                                                 llvm::raw_ostream &OS) {
-  // TODO: accumulate formulas directly instead
-  llvm::DenseSet<BoolValue *> Constraints = {&Token};
-  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  llvm::DenseSet<const Formula *> Constraints = {&arena().makeAtomRef(Token)};
+  llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
   // TODO: have formulas know about true/false directly instead
-  auto &True = arena().getFormula(arena().makeLiteral(true));
-  auto &False = arena().getFormula(arena().makeLiteral(false));
+  auto &True = arena().makeLiteral(true);
+  auto &False = arena().makeLiteral(false);
   auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
     if (&F == &True) {
       OS << "True";
@@ -218,7 +214,7 @@
   for (const auto *Constraint : Constraints) {
     Lines.emplace_back();
     llvm::raw_string_ostream LineOS(Lines.back());
-    arena().getFormula(*Constraint).print(LineOS, Delegate);
+    Constraint->print(LineOS, Delegate);
   }
   llvm::sort(Lines);
   for (const auto &Line : Lines)
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -107,15 +107,16 @@
     // if (o.has_value())
     //   x = o.value();
     // ```
-    auto *Expr1 = cast<BoolValue>(&Val1);
-    auto *Expr2 = cast<BoolValue>(&Val2);
-    auto &MergedVal = MergedEnv.makeAtomicBoolValue();
-    MergedEnv.addToFlowCondition(MergedEnv.makeOr(
-        MergedEnv.makeAnd(Env1.getFlowConditionToken(),
-                          MergedEnv.makeIff(MergedVal, *Expr1)),
-        MergedEnv.makeAnd(Env2.getFlowConditionToken(),
-                          MergedEnv.makeIff(MergedVal, *Expr2))));
-    return &MergedVal;
+    auto &Expr1 = cast<BoolValue>(Val1).formula();
+    auto &Expr2 = cast<BoolValue>(Val2).formula();
+    auto &A = MergedEnv.arena();
+    auto &MergedVal = A.makeAtomRef(A.makeAtom());
+    MergedEnv.addToFlowCondition(
+        A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
+                           A.makeEquals(MergedVal, Expr1)),
+                 A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
+                           A.makeEquals(MergedVal, Expr2))));
+    return &A.makeBoolValue(MergedVal);
   }
 
   // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
@@ -263,7 +264,7 @@
 
 Environment::Environment(DataflowAnalysisContext &DACtx)
     : DACtx(&DACtx),
-      FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
+      FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
 
 Environment::Environment(const Environment &Other)
     : DACtx(Other.DACtx), CallStack(Other.CallStack),
@@ -271,8 +272,7 @@
       ThisPointeeLoc(Other.ThisPointeeLoc), DeclToLoc(Other.DeclToLoc),
       ExprToLoc(Other.ExprToLoc), LocToVal(Other.LocToVal),
       MemberLocToStruct(Other.MemberLocToStruct),
-      FlowConditionToken(&DACtx->forkFlowCondition(*Other.FlowConditionToken)) {
-}
+      FlowConditionToken(DACtx->forkFlowCondition(Other.FlowConditionToken)) {}
 
 Environment &Environment::operator=(const Environment &Other) {
   Environment Copy(Other);
@@ -598,8 +598,8 @@
   // FIXME: set `Effect` as needed.
   // FIXME: update join to detect backedges and simplify the flow condition
   // accordingly.
-  JoinedEnv.FlowConditionToken = &DACtx->joinFlowConditions(
-      *FlowConditionToken, *Other.FlowConditionToken);
+  JoinedEnv.FlowConditionToken =
+      DACtx->joinFlowConditions(FlowConditionToken, Other.FlowConditionToken);
 
   for (auto &Entry : LocToVal) {
     const StorageLocation *Loc = Entry.first;
@@ -819,7 +819,7 @@
     // with integers, and so distinguishing them serves no purpose, but could
     // prevent convergence.
     CreatedValuesCount++;
-    return &DACtx->arena().create<IntegerValue>();
+    return &arena().create<IntegerValue>();
   }
 
   if (Type->isReferenceType() || Type->isPointerType()) {
@@ -837,9 +837,9 @@
     }
 
     if (Type->isReferenceType())
-      return &DACtx->arena().create<ReferenceValue>(PointeeLoc);
+      return &arena().create<ReferenceValue>(PointeeLoc);
     else
-      return &DACtx->arena().create<PointerValue>(PointeeLoc);
+      return &arena().create<PointerValue>(PointeeLoc);
   }
 
   if (Type->isRecordType()) {
@@ -859,7 +859,7 @@
       Visited.erase(FieldType.getCanonicalType());
     }
 
-    return &DACtx->arena().create<StructValue>(std::move(FieldValues));
+    return &arena().create<StructValue>(std::move(FieldValues));
   }
 
   return nullptr;
@@ -884,12 +884,18 @@
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
+void Environment::addToFlowCondition(const Formula &Val) {
+  DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
+}
 void Environment::addToFlowCondition(BoolValue &Val) {
-  DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
+  addToFlowCondition(Val.formula());
 }
 
+bool Environment::flowConditionImplies(const Formula &Val) const {
+  return DACtx->flowConditionImplies(FlowConditionToken, Val);
+}
 bool Environment::flowConditionImplies(BoolValue &Val) const {
-  return DACtx->flowConditionImplies(*FlowConditionToken, Val);
+  return flowConditionImplies(Val.formula());
 }
 
 void Environment::dump(raw_ostream &OS) const {
@@ -909,7 +915,7 @@
   }
 
   OS << "FlowConditionToken:\n";
-  DACtx->dumpFlowCondition(*FlowConditionToken, OS);
+  DACtx->dumpFlowCondition(FlowConditionToken, OS);
 }
 
 void Environment::dump() const {
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -36,16 +36,8 @@
     return "AtomicBool";
   case Value::Kind::TopBool:
     return "TopBool";
-  case Value::Kind::Conjunction:
-    return "Conjunction";
-  case Value::Kind::Disjunction:
-    return "Disjunction";
-  case Value::Kind::Negation:
-    return "Negation";
-  case Value::Kind::Implication:
-    return "Implication";
-  case Value::Kind::Biconditional:
-    return "Biconditional";
+  case Value::Kind::FormulaBool:
+    return "FormulaBool";
   }
   llvm_unreachable("Unhandled value kind");
 }
diff --git a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
--- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -111,33 +111,9 @@
         JOS.attributeObject("f:" + Child.first->getNameAsString(),
                             [&] { dump(*Child.second); });
       break;
-    case Value::Kind::Disjunction: {
-      auto &VV = cast<DisjunctionValue>(V);
-      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
-      break;
-    }
-    case Value::Kind::Conjunction: {
-      auto &VV = cast<ConjunctionValue>(V);
-      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
-      break;
-    }
-    case Value::Kind::Negation: {
-      auto &VV = cast<NegationValue>(V);
-      JOS.attributeObject("not", [&] { dump(VV.getSubVal()); });
-      break;
-    }
-    case Value::Kind::Implication: {
-      auto &VV = cast<ImplicationValue>(V);
-      JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); });
-      break;
-    }
-    case Value::Kind::Biconditional: {
-      auto &VV = cast<BiconditionalValue>(V);
-      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+    case Value::Kind::FormulaBool: {
+      auto &VV = cast<FormulaBoolValue>(V);
+      JOS.attribute("formula", llvm::to_string(VV.formula()));
       break;
     }
     }
@@ -149,10 +125,11 @@
     // Running the SAT solver is expensive, but knowing which booleans are
     // guaranteed true/false here is valuable and hard to determine by hand.
     if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
-      JOS.attribute("truth", Env.flowConditionImplies(*B) ? "true"
-                             : Env.flowConditionImplies(Env.makeNot(*B))
-                                 ? "false"
-                                 : "unknown");
+      JOS.attribute(
+          "truth", Env.flowConditionImplies(B->formula()) ? "true"
+                   : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
+                       ? "false"
+                       : "unknown");
     }
   }
   void dump(const StorageLocation &L) {
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -61,64 +61,12 @@
   return Env.makeAtomicBoolValue();
 }
 
-// Functionally updates `V` such that any instances of `TopBool` are replaced
-// with fresh atomic bools. Note: This implementation assumes that `B` is a
-// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
-// present in the original .
-static BoolValue &unpackValue(BoolValue &V, Environment &Env);
-
-template <typename Derived, typename M>
-BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
-  auto &V = *cast<Derived>(&B);
-  BoolValue &Left = V.getLeftSubValue();
-  BoolValue &Right = V.getRightSubValue();
-  BoolValue &ULeft = unpackValue(Left, Env);
-  BoolValue &URight = unpackValue(Right, Env);
-
-  if (&ULeft == &Left && &URight == &Right)
-    return V;
-
-  return (Env.*build)(ULeft, URight);
-}
-
 static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
-  switch (V.getKind()) {
-  case Value::Kind::Integer:
-  case Value::Kind::Reference:
-  case Value::Kind::Pointer:
-  case Value::Kind::Struct:
-    llvm_unreachable("BoolValue cannot have any of these kinds.");
-
-  case Value::Kind::AtomicBool:
-    return V;
-
-  case Value::Kind::TopBool:
-    // Unpack `TopBool` into a fresh atomic bool.
-    return Env.makeAtomicBoolValue();
-
-  case Value::Kind::Negation: {
-    auto &N = *cast<NegationValue>(&V);
-    BoolValue &Sub = N.getSubVal();
-    BoolValue &USub = unpackValue(Sub, Env);
-
-    if (&USub == &Sub)
-      return V;
-    return Env.makeNot(USub);
-  }
-  case Value::Kind::Conjunction:
-    return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
-                                                   &Environment::makeAnd);
-  case Value::Kind::Disjunction:
-    return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
-                                                   &Environment::makeOr);
-  case Value::Kind::Implication:
-    return unpackBinaryBoolValue<ImplicationValue>(
-        Env, V, &Environment::makeImplication);
-  case Value::Kind::Biconditional:
-    return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
-                                                     &Environment::makeIff);
+  if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
+    auto &A = Env.getDataflowAnalysisContext().arena();
+    return A.makeBoolValue(A.makeAtomRef(Top->atom()));
   }
-  llvm_unreachable("All reachable cases in switch return");
+  return V;
 }
 
 // Unpacks the value (if any) associated with `E` and updates `E` to the new
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -20,26 +20,26 @@
 };
 
 TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomValue();
+  auto &Y = A.makeAtomValue();
   EXPECT_NE(&X, &Y);
 }
 
 TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
-  auto &X = A.create<TopBoolValue>();
-  auto &Y = A.create<TopBoolValue>();
+  auto &X = A.makeTopValue();
+  auto &Y = A.makeTopValue();
   EXPECT_NE(&X, &Y);
 }
 
 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &XAndX = A.makeAnd(X, X);
   EXPECT_EQ(&XAndX, &X);
 }
 
 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XAndY1 = A.makeAnd(X, Y);
   auto &XAndY2 = A.makeAnd(X, Y);
   EXPECT_EQ(&XAndY1, &XAndY2);
@@ -47,20 +47,20 @@
   auto &YAndX = A.makeAnd(Y, X);
   EXPECT_EQ(&XAndY1, &YAndX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XAndZ = A.makeAnd(X, Z);
   EXPECT_NE(&XAndY1, &XAndZ);
 }
 
 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &XOrX = A.makeOr(X, X);
   EXPECT_EQ(&XOrX, &X);
 }
 
 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XOrY1 = A.makeOr(X, Y);
   auto &XOrY2 = A.makeOr(X, Y);
   EXPECT_EQ(&XOrY1, &XOrY2);
@@ -68,31 +68,30 @@
   auto &YOrX = A.makeOr(Y, X);
   EXPECT_EQ(&XOrY1, &YOrX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XOrZ = A.makeOr(X, Z);
   EXPECT_NE(&XOrY1, &XOrZ);
 }
 
 TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &NotX1 = A.makeNot(X);
   auto &NotX2 = A.makeNot(X);
   EXPECT_EQ(&NotX1, &NotX2);
-
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &NotY = A.makeNot(Y);
   EXPECT_NE(&NotX1, &NotY);
 }
 
 TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &XImpliesX = A.makeImplies(X, X);
   EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
 }
 
 TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XImpliesY1 = A.makeImplies(X, Y);
   auto &XImpliesY2 = A.makeImplies(X, Y);
   EXPECT_EQ(&XImpliesY1, &XImpliesY2);
@@ -100,20 +99,20 @@
   auto &YImpliesX = A.makeImplies(Y, X);
   EXPECT_NE(&XImpliesY1, &YImpliesX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XImpliesZ = A.makeImplies(X, Z);
   EXPECT_NE(&XImpliesY1, &XImpliesZ);
 }
 
 TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &XIffX = A.makeEquals(X, X);
   EXPECT_EQ(&XIffX, &A.makeLiteral(true));
 }
 
 TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XIffY1 = A.makeEquals(X, Y);
   auto &XIffY2 = A.makeEquals(X, Y);
   EXPECT_EQ(&XIffY1, &XIffY2);
@@ -121,30 +120,21 @@
   auto &YIffX = A.makeEquals(Y, X);
   EXPECT_EQ(&XIffY1, &YIffX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XIffZ = A.makeEquals(X, Z);
   EXPECT_NE(&XIffY1, &XIffZ);
 }
 
-TEST_F(ArenaTest, ValueToFormula) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
-  auto &XIffY = A.makeEquals(X, Y);
-  auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
-  auto &Implies = A.makeImplies(XIffY, XOrNotY);
-
-  EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
-            "((V0 = V1) => (V0 | !V1))");
-}
-
-TEST_F(ArenaTest, ValueToFormulaCached) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
-  auto &XIffY = A.makeEquals(X, Y);
-
-  auto &Formula1 = A.getFormula(XIffY);
-  auto &Formula2 = A.getFormula(XIffY);
-  EXPECT_EQ(&Formula1, &Formula2);
+TEST_F(ArenaTest, Interning) {
+  Atom X = A.makeAtom();
+  Atom Y = A.makeAtom();
+  const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));
+  const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
+  EXPECT_EQ(&F1, &F2);
+  BoolValue &B1 = A.makeBoolValue(F1);
+  BoolValue &B2 = A.makeBoolValue(F2);
+  EXPECT_EQ(&B1, &B2);
+  EXPECT_EQ(&B1.formula(), &F1);
 }
 
 } // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -28,56 +28,56 @@
 };
 
 TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
-  auto &X = A.create<TopBoolValue>();
-  auto &Y = A.create<TopBoolValue>();
-  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+  auto &X = A.makeTopValue();
+  auto &Y = A.makeTopValue();
+  EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
 }
 
 TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
-  auto &FC = A.makeFlowConditionToken();
-  auto &C = A.create<AtomicBoolValue>();
+  Atom FC = A.makeFlowConditionToken();
+  auto &C = A.makeAtomRef(A.makeAtom());
   EXPECT_FALSE(Context.flowConditionImplies(FC, C));
 }
 
 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
-  auto &FC = A.makeFlowConditionToken();
-  auto &C = A.create<AtomicBoolValue>();
+  Atom FC = A.makeFlowConditionToken();
+  auto &C = A.makeAtomRef(A.makeAtom());
   Context.addFlowConditionConstraint(FC, C);
   EXPECT_TRUE(Context.flowConditionImplies(FC, C));
 }
 
 TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
-  auto &FC1 = A.makeFlowConditionToken();
-  auto &C1 = A.create<AtomicBoolValue>();
+  Atom FC1 = A.makeFlowConditionToken();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
   Context.addFlowConditionConstraint(FC1, C1);
 
   // Forked flow condition inherits the constraints of its parent flow
   // condition.
-  auto &FC2 = Context.forkFlowCondition(FC1);
+  Atom FC2 = Context.forkFlowCondition(FC1);
   EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
 
   // Adding a new constraint to the forked flow condition does not affect its
   // parent flow condition.
-  auto &C2 = A.create<AtomicBoolValue>();
+  auto &C2 = A.makeAtomRef(A.makeAtom());
   Context.addFlowConditionConstraint(FC2, C2);
   EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
   EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
 }
 
 TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
-  auto &C1 = A.create<AtomicBoolValue>();
-  auto &C2 = A.create<AtomicBoolValue>();
-  auto &C3 = A.create<AtomicBoolValue>();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
+  auto &C2 = A.makeAtomRef(A.makeAtom());
+  auto &C3 = A.makeAtomRef(A.makeAtom());
 
-  auto &FC1 = A.makeFlowConditionToken();
+  Atom FC1 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC1, C1);
   Context.addFlowConditionConstraint(FC1, C3);
 
-  auto &FC2 = A.makeFlowConditionToken();
+  Atom FC2 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, C2);
   Context.addFlowConditionConstraint(FC2, C3);
 
-  auto &FC3 = Context.joinFlowConditions(FC1, FC2);
+  Atom FC3 = Context.joinFlowConditions(FC1, FC2);
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
@@ -85,77 +85,77 @@
 
 TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
   // Fresh flow condition with empty/no constraints is always true.
-  auto &FC1 = A.makeFlowConditionToken();
+  Atom FC1 = A.makeFlowConditionToken();
   EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
 
   // Literal `true` is always true.
-  auto &FC2 = A.makeFlowConditionToken();
+  Atom FC2 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
 
   // Literal `false` is never true.
-  auto &FC3 = A.makeFlowConditionToken();
+  Atom FC3 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC3, A.makeLiteral(false));
   EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
 
   // We can't prove that an arbitrary bool A is always true...
-  auto &C1 = A.create<AtomicBoolValue>();
-  auto &FC4 = A.makeFlowConditionToken();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
+  Atom FC4 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC4, C1);
   EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
 
   // ... but we can prove A || !A is true.
-  auto &FC5 = A.makeFlowConditionToken();
+  Atom FC5 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
 }
 
 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &True = A.makeLiteral(true);
   auto &False = A.makeLiteral(false);
 
   // X == X
-  EXPECT_TRUE(Context.equivalentBoolValues(X, X));
+  EXPECT_TRUE(Context.equivalentFormulas(X, X));
   // X != Y
-  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+  EXPECT_FALSE(Context.equivalentFormulas(X, Y));
 
   // !X != X
-  EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
+  EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
   // !(!X) = X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
 
   // (X || X) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
   // (X || Y) != X
-  EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
+  EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
   // (X || True) == True
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
   // (X || False) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
 
   // (X && X) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
   // (X && Y) != X
-  EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
+  EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
   // (X && True) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
   // (X && False) == False
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
 
   // (X || Y) == (Y || X)
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
   // (X && Y) == (Y && X)
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
 
   // ((X || Y) || Z) == (X || (Y || Z))
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
-                                           A.makeOr(X, A.makeOr(Y, Z))));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
+                                         A.makeOr(X, A.makeOr(Y, Z))));
   // ((X && Y) && Z) == (X && (Y && Z))
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z),
-                                           A.makeAnd(X, A.makeAnd(Y, Z))));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),
+                                         A.makeAnd(X, A.makeAnd(Y, Z))));
 }
 
 } // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -2908,14 +2908,12 @@
           ASSERT_THAT(BazDecl, NotNull());
 
           const auto *BazVal =
-              dyn_cast_or_null<ConjunctionValue>(Env.getValue(*BazDecl));
+              dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
           ASSERT_THAT(BazVal, NotNull());
-          EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal);
-
-          const auto *BazRightSubValVal =
-              cast<DisjunctionValue>(&BazVal->getRightSubValue());
-          EXPECT_EQ(&BazRightSubValVal->getLeftSubValue(), BarVal);
-          EXPECT_EQ(&BazRightSubValVal->getRightSubValue(), QuxVal);
+          auto &A = Env.arena();
+          EXPECT_EQ(&BazVal->formula(),
+                    &A.makeAnd(FooVal->formula(),
+                               A.makeOr(BarVal->formula(), QuxVal->formula())));
         });
   }
 
@@ -2958,15 +2956,12 @@
           ASSERT_THAT(BazDecl, NotNull());
 
           const auto *BazVal =
-              dyn_cast_or_null<DisjunctionValue>(Env.getValue(*BazDecl));
+              dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
           ASSERT_THAT(BazVal, NotNull());
-
-          const auto *BazLeftSubValVal =
-              cast<ConjunctionValue>(&BazVal->getLeftSubValue());
-          EXPECT_EQ(&BazLeftSubValVal->getLeftSubValue(), FooVal);
-          EXPECT_EQ(&BazLeftSubValVal->getRightSubValue(), QuxVal);
-
-          EXPECT_EQ(&BazVal->getRightSubValue(), BarVal);
+          auto &A = Env.arena();
+          EXPECT_EQ(&BazVal->formula(),
+                    &A.makeOr(A.makeAnd(FooVal->formula(), QuxVal->formula()),
+                              BarVal->formula()));
         });
   }
 
@@ -3012,17 +3007,14 @@
           ASSERT_THAT(FooDecl, NotNull());
 
           const auto *FooVal =
-              dyn_cast_or_null<ConjunctionValue>(Env.getValue(*FooDecl));
+              dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
           ASSERT_THAT(FooVal, NotNull());
-
-          const auto &FooLeftSubVal =
-              cast<ConjunctionValue>(FooVal->getLeftSubValue());
-          const auto &FooLeftLeftSubVal =
-              cast<ConjunctionValue>(FooLeftSubVal.getLeftSubValue());
-          EXPECT_EQ(&FooLeftLeftSubVal.getLeftSubValue(), AVal);
-          EXPECT_EQ(&FooLeftLeftSubVal.getRightSubValue(), BVal);
-          EXPECT_EQ(&FooLeftSubVal.getRightSubValue(), CVal);
-          EXPECT_EQ(&FooVal->getRightSubValue(), DVal);
+          auto &A = Env.arena();
+          EXPECT_EQ(
+              &FooVal->formula(),
+              &A.makeAnd(A.makeAnd(A.makeAnd(AVal->formula(), BVal->formula()),
+                                   CVal->formula()),
+                         DVal->formula()));
         });
   }
 }
@@ -3053,10 +3045,10 @@
         ASSERT_THAT(BarDecl, NotNull());
 
         const auto *BarVal =
-            dyn_cast_or_null<NegationValue>(Env.getValue(*BarDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
         ASSERT_THAT(BarVal, NotNull());
-
-        EXPECT_EQ(&BarVal->getSubVal(), FooVal);
+        auto &A = Env.arena();
+        EXPECT_EQ(&BarVal->formula(), &A.makeNot(FooVal->formula()));
       });
 }
 
diff --git a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
@@ -39,17 +40,19 @@
 }
 
 TEST(ValueTest, TopsEquivalent) {
-  TopBoolValue V1;
-  TopBoolValue V2;
+  Arena A;
+  TopBoolValue V1(A.makeAtomRef(Atom(0)));
+  TopBoolValue V2(A.makeAtomRef(Atom(1)));
   EXPECT_TRUE(areEquivalentValues(V1, V2));
   EXPECT_TRUE(areEquivalentValues(V2, V1));
 }
 
 TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
-  TopBoolValue Prop1;
-  TopBoolValue Prop2;
-  TopBoolValue V1;
-  TopBoolValue V2;
+  Arena A;
+  TopBoolValue Prop1(A.makeAtomRef(Atom(0)));
+  TopBoolValue Prop2(A.makeAtomRef(Atom(1)));
+  TopBoolValue V1(A.makeAtomRef(Atom(2)));
+  TopBoolValue V2(A.makeAtomRef(Atom(3)));
   V1.setProperty("foo", Prop1);
   V2.setProperty("bar", Prop2);
   EXPECT_TRUE(areEquivalentValues(V1, V2));
@@ -57,9 +60,10 @@
 }
 
 TEST(ValueTest, DifferentKindsNotEquivalent) {
+  Arena A;
   auto L = ScalarStorageLocation(QualType());
   ReferenceValue V1(L);
-  TopBoolValue V2;
+  TopBoolValue V2(A.makeAtomRef(Atom(0)));
   EXPECT_FALSE(areEquivalentValues(V1, V2));
   EXPECT_FALSE(areEquivalentValues(V2, V1));
 }