diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
index b6c62e7624625..83b4ddeec0256 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,7 +8,6 @@
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
 
-#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include <vector>
@@ -105,17 +104,7 @@ class Arena {
     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++); };
-
 private:
-  llvm::BumpPtrAllocator Alloc;
-
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
@@ -133,9 +122,6 @@ class Arena {
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
       BiconditionalVals;
 
-  llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
-  unsigned NextAtom = 0;
-
   AtomicBoolValue &TrueVal;
   AtomicBoolValue &FalseVal;
 };
diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
index 6b9f3681490af..360786b02729f 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,6 +19,7 @@
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringRef.h"
 
 namespace clang {
@@ -27,9 +28,52 @@ namespace dataflow {
 /// Returns a string representation of a value kind.
 llvm::StringRef debugString(Value::Kind Kind);
 
+/// Returns a string representation of a boolean assignment to true or false.
+llvm::StringRef debugString(Solver::Result::Assignment Assignment);
+
 /// Returns a string representation of the result status of a SAT check.
 llvm::StringRef debugString(Solver::Result::Status Status);
 
+/// Returns a string representation for the boolean value `B`.
+///
+/// Atomic booleans appearing in the boolean value `B` are assigned to labels
+/// either specified in `AtomNames` or created by default rules as B0, B1, ...
+///
+/// Requirements:
+///
+///   Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+    const BoolValue &B,
+    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
+/// Returns a string representation for `Constraints` - a collection of boolean
+/// formulas.
+///
+/// Atomic booleans appearing in the boolean value `Constraints` are assigned to
+/// labels either specified in `AtomNames` or created by default rules as B0,
+/// B1, ...
+///
+/// Requirements:
+///
+///   Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+    const llvm::ArrayRef<BoolValue *> Constraints,
+    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
+/// Returns a string representation for `Constraints` - a collection of boolean
+/// formulas and the `Result` of satisfiability checking.
+///
+/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
+/// labels either specified in `AtomNames` or created by default rules as B0,
+/// B1, ...
+///
+/// Requirements:
+///
+///   Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+    ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
+    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
 } // namespace dataflow
 } // namespace clang
 
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h
deleted file mode 100644
index 0c7b1ecd02b17..0000000000000
--- a/clang/include/clang/Analysis/FlowSensitive/Formula.h
+++ /dev/null
@@ -1,137 +0,0 @@
-//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
-#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
-
-#include "clang/Basic/LLVM.h"
-#include "llvm/ADT/ArrayRef.h"
-#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/DenseMapInfo.h"
-#include "llvm/ADT/STLFunctionalExtras.h"
-#include "llvm/Support/Allocator.h"
-#include "llvm/Support/raw_ostream.h"
-#include <cassert>
-#include <string>
-#include <type_traits>
-
-namespace clang::dataflow {
-
-/// Identifies an atomic boolean variable such as "V1".
-///
-/// This often represents an assertion that is interesting to the analysis but
-/// cannot immediately be proven true or false. For example:
-/// - V1 may mean "the program reaches this point",
-/// - V2 may mean "the parameter was null"
-///
-/// We can use these variables in formulas to describe relationships we know
-/// to be true: "if the parameter was null, the program reaches this point".
-/// We also express hypotheses as formulas, and use a SAT solver to check
-/// whether they are consistent with the known facts.
-enum class Atom : unsigned {};
-
-/// A boolean expression such as "true" or "V1 & !V2".
-/// Expressions may refer to boolean atomic variables. These should take a
-/// consistent true/false value across the set of formulas being considered.
-///
-/// (Formulas are always expressions in terms of boolean variables rather than
-/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
-///
-/// Simple formulas such as "true" and "V1" are self-contained.
-/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
-/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
-/// trailing objects.
-/// For this reason, Formulas are Arena-allocated and over-aligned.
-class Formula;
-class alignas(const Formula *) Formula {
-public:
-  enum Kind : unsigned {
-    /// A reference to an atomic boolean variable.
-    /// We name these e.g. "V3", where 3 == atom identity == Value.
-    AtomRef,
-    // FIXME: add const true/false rather than modeling them as variables
-
-    Not, /// True if its only operand is false
-
-    // These kinds connect two operands LHS and RHS
-    And,     /// True if LHS and RHS are both true
-    Or,      /// True if either LHS or RHS is true
-    Implies, /// True if LHS is false or RHS is true
-    Equal,   /// True if LHS and RHS have the same truth value
-  };
-  Kind kind() const { return FormulaKind; }
-
-  Atom getAtom() const {
-    assert(kind() == AtomRef);
-    return static_cast<Atom>(Value);
-  }
-
-  ArrayRef<const Formula *> operands() const {
-    return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
-                    numOperands(kind()));
-  }
-
-  using AtomNames = llvm::DenseMap<Atom, std::string>;
-  // Produce a stable human-readable representation of this formula.
-  // For example: (V3 | !(V1 & V2))
-  // If AtomNames is provided, these override the default V0, V1... names.
-  void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
-
-  // Allocate Formulas using Arena rather than calling this function directly.
-  static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
-                         ArrayRef<const Formula *> Operands,
-                         unsigned Value = 0);
-
-private:
-  Formula() = default;
-  Formula(const Formula &) = delete;
-  Formula &operator=(const Formula &) = delete;
-
-  static unsigned numOperands(Kind K) {
-    switch (K) {
-    case AtomRef:
-      return 0;
-    case Not:
-      return 1;
-    case And:
-    case Or:
-    case Implies:
-    case Equal:
-      return 2;
-    }
-  }
-
-  Kind FormulaKind;
-  // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
-  unsigned Value;
-};
-
-// The default names of atoms are V0, V1 etc in order of creation.
-inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
-  return OS << 'V' << static_cast<unsigned>(A);
-}
-inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
-  F.print(OS);
-  return OS;
-}
-
-} // namespace clang::dataflow
-namespace llvm {
-template <> struct DenseMapInfo<clang::dataflow::Atom> {
-  using Atom = clang::dataflow::Atom;
-  using Underlying = std::underlying_type_t<Atom>;
-
-  static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
-  static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
-  static unsigned getHashValue(const Atom &Val) {
-    return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
-  }
-  static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
-};
-} // namespace llvm
-#endif
diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h
index 079f6802f241e..10964eab8c34c 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,10 +14,12 @@
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 
-#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Basic/LLVM.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+#include "llvm/Support/Compiler.h"
 #include <optional>
 #include <vector>
 
@@ -47,7 +49,8 @@ class Solver {
 
     /// Constructs a result indicating that the queried boolean formula is
     /// satisfiable. The result will hold a solution found by the solver.
-    static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
+    static Result
+    Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
       return Result(Status::Satisfiable, std::move(Solution));
     }
 
@@ -65,17 +68,19 @@ class Solver {
 
     /// Returns a truth assignment to boolean values that satisfies the queried
     /// boolean formula if available. Otherwise, an empty optional is returned.
-    std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
+    std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
+    getSolution() const {
       return Solution;
     }
 
   private:
-    Result(Status SATCheckStatus,
-           std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
+    Result(
+        enum Status SATCheckStatus,
+        std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
         : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
 
     Status SATCheckStatus;
-    std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
+    std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
   };
 
   virtual ~Solver() = default;
@@ -86,11 +91,13 @@ class Solver {
   /// Requirements:
   ///
   ///  All elements in `Vals` must not be null.
-  virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
-};
+  virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
 
-llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
-llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+  LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
+  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
+    return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
+  }
+};
 
 } // namespace dataflow
 } // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
index a0cdce93c9d47..b69cc01542c55 100644
--- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -14,8 +14,8 @@
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 
-#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/ArrayRef.h"
 #include <limits>
 
@@ -46,7 +46,7 @@ class WatchedLiteralsSolver : public Solver {
   explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
       : MaxIterations(WorkLimit) {}
 
-  Result solve(llvm::ArrayRef<const Formula *> Vals) override;
+  Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
 };
 
 } // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index e576affc6a41b..cff6c45e18542 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -76,50 +76,4 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
   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;
-}
-
 } // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 171884afe8f4b..d59bebf6a5a12 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,7 +3,6 @@ add_clang_library(clangAnalysisFlowSensitive
   ControlFlowContext.cpp
   DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
-  Formula.cpp
   HTMLLogger.cpp
   Logger.cpp
   RecordOps.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 42cc6d4c3d143..37bcc8be95879 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,7 +15,6 @@
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Logger.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/SetOperations.h"
@@ -24,12 +23,9 @@
 #include "llvm/Support/Debug.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/Path.h"
-#include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <memory>
-#include <string>
 #include <utility>
-#include <vector>
 
 static llvm::cl::opt<std::string> DataflowLog(
     "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
@@ -133,10 +129,7 @@ Solver::Result
 DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
   Constraints.insert(&arena().makeLiteral(true));
   Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
-  std::vector<const Formula *> Formulas;
-  for (const BoolValue *Constraint : Constraints)
-    Formulas.push_back(&arena().getFormula(*Constraint));
-  return S->solve(Formulas);
+  return S->solve(Constraints.getArrayRef());
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
@@ -198,21 +191,15 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
 
 void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
                                                 llvm::raw_ostream &OS) {
-  // TODO: accumulate formulas directly instead
   llvm::SetVector<BoolValue *> Constraints;
   Constraints.insert(&Token);
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
-  // TODO: have formulas know about true/false directly instead
-  Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom();
-  Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom();
-  Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
-
-  for (const auto *Constraint : Constraints) {
-    arena().getFormula(*Constraint).print(OS, &Names);
-    OS << "\n";
-  }
+  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
+      {&arena().makeLiteral(false), "False"},
+      {&arena().makeLiteral(true), "True"}};
+  OS << debugString(Constraints.getArrayRef(), AtomNames);
 }
 
 const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index 34e53249ba4d8..25225ed6266fb 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,12 +16,22 @@
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/StringRef.h"
+#include "llvm/ADT/StringSet.h"
 #include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/FormatAdapters.h"
+#include "llvm/Support/FormatCommon.h"
+#include "llvm/Support/FormatVariadic.h"
 
 namespace clang {
 namespace dataflow {
 
+using llvm::AlignStyle;
+using llvm::fmt_pad;
+using llvm::formatv;
+
 llvm::StringRef debugString(Value::Kind Kind) {
   switch (Kind) {
   case Value::Kind::Integer:
@@ -50,13 +60,12 @@ llvm::StringRef debugString(Value::Kind Kind) {
   llvm_unreachable("Unhandled value kind");
 }
 
-llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
-                              Solver::Result::Assignment Assignment) {
+llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
   switch (Assignment) {
   case Solver::Result::Assignment::AssignedFalse:
-    return OS << "False";
+    return "False";
   case Solver::Result::Assignment::AssignedTrue:
-    return OS << "True";
+    return "True";
   }
   llvm_unreachable("Booleans can only be assigned true/false");
 }
@@ -73,16 +82,174 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
   llvm_unreachable("Unhandled SAT check result status");
 }
 
-llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
-  OS << debugString(R.getStatus()) << "\n";
-  if (auto Solution = R.getSolution()) {
-    std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
-        Solution->begin(), Solution->end()};
-    llvm::sort(Sorted);
-    for (const auto &Entry : Sorted)
-      OS << Entry.first << " = " << Entry.second << "\n";
+namespace {
+
+class DebugStringGenerator {
+public:
+  explicit DebugStringGenerator(
+      llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
+      : Counter(0), AtomNames(std::move(AtomNamesArg)) {
+#ifndef NDEBUG
+    llvm::StringSet<> Names;
+    for (auto &N : AtomNames) {
+      assert(Names.insert(N.second).second &&
+             "The same name must not assigned to different atoms");
+    }
+#endif
+  }
+
+  /// Returns a string representation of a boolean value `B`.
+  std::string debugString(const BoolValue &B, size_t Depth = 0) {
+    std::string S;
+    switch (B.getKind()) {
+    case Value::Kind::AtomicBool: {
+      S = getAtomName(&cast<AtomicBoolValue>(B));
+      break;
+    }
+    case Value::Kind::TopBool: {
+      S = "top";
+      break;
+    }
+    case Value::Kind::Conjunction: {
+      auto &C = cast<ConjunctionValue>(B);
+      auto L = debugString(C.getLeftSubValue(), Depth + 1);
+      auto R = debugString(C.getRightSubValue(), Depth + 1);
+      S = formatv("(and\n{0}\n{1})", L, R);
+      break;
+    }
+    case Value::Kind::Disjunction: {
+      auto &D = cast<DisjunctionValue>(B);
+      auto L = debugString(D.getLeftSubValue(), Depth + 1);
+      auto R = debugString(D.getRightSubValue(), Depth + 1);
+      S = formatv("(or\n{0}\n{1})", L, R);
+      break;
+    }
+    case Value::Kind::Negation: {
+      auto &N = cast<NegationValue>(B);
+      S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
+      break;
+    }
+    case Value::Kind::Implication: {
+      auto &IV = cast<ImplicationValue>(B);
+      auto L = debugString(IV.getLeftSubValue(), Depth + 1);
+      auto R = debugString(IV.getRightSubValue(), Depth + 1);
+      S = formatv("(=>\n{0}\n{1})", L, R);
+      break;
+    }
+    case Value::Kind::Biconditional: {
+      auto &BV = cast<BiconditionalValue>(B);
+      auto L = debugString(BV.getLeftSubValue(), Depth + 1);
+      auto R = debugString(BV.getRightSubValue(), Depth + 1);
+      S = formatv("(=\n{0}\n{1})", L, R);
+      break;
+    }
+    default:
+      llvm_unreachable("Unhandled value kind");
+    }
+    auto Indent = Depth * 4;
+    return formatv("{0}", fmt_pad(S, Indent, 0));
+  }
+
+  std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) {
+    std::string Result;
+    for (const BoolValue *S : Constraints) {
+      Result += debugString(*S);
+      Result += '\n';
+    }
+    return Result;
+  }
+
+  /// Returns a string representation of a set of boolean `Constraints` and the
+  /// `Result` of satisfiability checking on the `Constraints`.
+  std::string debugString(ArrayRef<BoolValue *> &Constraints,
+                          const Solver::Result &Result) {
+    auto Template = R"(
+Constraints
+------------
+{0:$[
+
+]}
+------------
+{1}.
+{2}
+)";
+
+    std::vector<std::string> ConstraintsStrings;
+    ConstraintsStrings.reserve(Constraints.size());
+    for (auto &Constraint : Constraints) {
+      ConstraintsStrings.push_back(debugString(*Constraint));
+    }
+
+    auto StatusString = clang::dataflow::debugString(Result.getStatus());
+    auto Solution = Result.getSolution();
+    auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
+
+    return formatv(
+        Template,
+        llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
+        StatusString, SolutionString);
+  }
+
+private:
+  /// Returns a string representation of a truth assignment to atom booleans.
+  std::string debugString(
+      const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
+          &AtomAssignments) {
+    size_t MaxNameLength = 0;
+    for (auto &AtomName : AtomNames) {
+      MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
+    }
+
+    std::vector<std::string> Lines;
+    for (auto &AtomAssignment : AtomAssignments) {
+      auto Line = formatv("{0} = {1}",
+                          fmt_align(getAtomName(AtomAssignment.first),
+                                    AlignStyle::Left, MaxNameLength),
+                          clang::dataflow::debugString(AtomAssignment.second));
+      Lines.push_back(Line);
+    }
+    llvm::sort(Lines);
+
+    return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
   }
-  return OS;
+
+  /// Returns the name assigned to `Atom`, either user-specified or created by
+  /// default rules (B0, B1, ...).
+  std::string getAtomName(const AtomicBoolValue *Atom) {
+    auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
+    if (Entry.second) {
+      Counter++;
+    }
+    return Entry.first->second;
+  }
+
+  // Keep track of number of atoms without a user-specified name, used to assign
+  // non-repeating default names to such atoms.
+  size_t Counter;
+
+  // Keep track of names assigned to atoms.
+  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
+};
+
+} // namespace
+
+std::string
+debugString(const BoolValue &B,
+            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+  return DebugStringGenerator(std::move(AtomNames)).debugString(B);
+}
+
+std::string
+debugString(llvm::ArrayRef<BoolValue *> Constraints,
+            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+  return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
+}
+
+std::string
+debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
+            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+  return DebugStringGenerator(std::move(AtomNames))
+      .debugString(Constraints, Result);
 }
 
 } // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
deleted file mode 100644
index 504ad2fb7938a..0000000000000
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-//===- Formula.cpp ----------------------------------------------*- C++ -*-===//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-
-#include "clang/Analysis/FlowSensitive/Formula.h"
-#include "clang/Basic/LLVM.h"
-#include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/StringRef.h"
-#include "llvm/Support/Allocator.h"
-#include "llvm/Support/ErrorHandling.h"
-#include <cassert>
-
-namespace clang::dataflow {
-
-Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
-                         ArrayRef<const Formula *> Operands, unsigned Value) {
-  assert(Operands.size() == numOperands(K));
-  if (Value != 0) // Currently, formulas have values or operands, not both.
-    assert(numOperands(K) == 0);
-  void *Mem = Alloc.Allocate(sizeof(Formula) +
-                                 Operands.size() * sizeof(Operands.front()),
-                             alignof(Formula));
-  Formula *Result = new (Mem) Formula();
-  Result->FormulaKind = K;
-  Result->Value = Value;
-  // Operands are stored as `const Formula *`s after the formula itself.
-  // We don't need to construct an object as pointers are trivial types.
-  // Formula is alignas(const Formula *), so alignment is satisfied.
-  llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
-  return *Result;
-}
-
-static llvm::StringLiteral sigil(Formula::Kind K) {
-  switch (K) {
-  case Formula::AtomRef:
-    return "";
-  case Formula::Not:
-    return "!";
-  case Formula::And:
-    return " & ";
-  case Formula::Or:
-    return " | ";
-  case Formula::Implies:
-    return " => ";
-  case Formula::Equal:
-    return " = ";
-  }
-  llvm_unreachable("unhandled formula kind");
-}
-
-void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
-  if (Names && kind() == AtomRef)
-    if (auto It = Names->find(getAtom()); It != Names->end()) {
-      OS << It->second;
-      return;
-    }
-
-  switch (numOperands(kind())) {
-  case 0:
-    OS << getAtom();
-    break;
-  case 1:
-    OS << sigil(kind());
-    operands()[0]->print(OS, Names);
-    break;
-  case 2:
-    OS << '(';
-    operands()[0]->print(OS, Names);
-    OS << sigil(kind());
-    operands()[1]->print(OS, Names);
-    OS << ')';
-    break;
-  default:
-    llvm_unreachable("unhandled formula arity");
-  }
-}
-
-} // namespace clang::dataflow
\ No newline at end of file
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index 037886d09c4f7..db2e1d694457b 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -17,8 +17,8 @@
 #include <queue>
 #include <vector>
 
-#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
@@ -79,7 +79,7 @@ using ClauseID = uint32_t;
 static constexpr ClauseID NullClause = 0;
 
 /// A boolean formula in conjunctive normal form.
-struct CNFFormula {
+struct BooleanFormula {
   /// `LargestVar` is equal to the largest positive integer that represents a
   /// variable in the formula.
   const Variable LargestVar;
@@ -121,12 +121,12 @@ struct CNFFormula {
   /// clauses in the formula start from the element at index 1.
   std::vector<ClauseID> NextWatched;
 
-  /// Stores the variable identifier and Atom for atomic booleans in the
-  /// formula.
-  llvm::DenseMap<Variable, Atom> Atomics;
+  /// Stores the variable identifier and value location for atomic booleans in
+  /// the formula.
+  llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
 
-  explicit CNFFormula(Variable LargestVar,
-                      llvm::DenseMap<Variable, Atom> Atomics)
+  explicit BooleanFormula(Variable LargestVar,
+                          llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
       : LargestVar(LargestVar), Atomics(std::move(Atomics)) {
     Clauses.push_back(0);
     ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct CNFFormula {
   ///
   ///  All literals in the input that are not `NullLit` must be distinct.
   void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
-    // The literals are guaranteed to be distinct from properties of Formula
-    // and the construction in `buildCNF`.
+    // The literals are guaranteed to be distinct from properties of BoolValue
+    // and the construction in `buildBooleanFormula`.
     assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
            (L2 != L3 || L2 == NullLit));
 
@@ -178,59 +178,98 @@ struct CNFFormula {
 
 /// Converts the conjunction of `Vals` into a formula in conjunctive normal
 /// form where each clause has at least one and at most three literals.
-CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
   // The general strategy of the algorithm implemented below is to map each
   // of the sub-values in `Vals` to a unique variable and use these variables in
   // the resulting CNF expression to avoid exponential blow up. The number of
   // literals in the resulting formula is guaranteed to be linear in the number
-  // of sub-formulas in `Vals`.
+  // of sub-values in `Vals`.
 
-  // Map each sub-formula in `Vals` to a unique variable.
-  llvm::DenseMap<const Formula *, Variable> SubValsToVar;
-  // Store variable identifiers and Atom of atomic booleans.
-  llvm::DenseMap<Variable, Atom> Atomics;
+  // Map each sub-value in `Vals` to a unique variable.
+  llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
+  // Store variable identifiers and value location of atomic booleans.
+  llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
   Variable NextVar = 1;
   {
-    std::queue<const Formula *> UnprocessedSubVals;
-    for (const Formula *Val : Vals)
+    std::queue<BoolValue *> UnprocessedSubVals;
+    for (BoolValue *Val : Vals)
       UnprocessedSubVals.push(Val);
     while (!UnprocessedSubVals.empty()) {
       Variable Var = NextVar;
-      const Formula *Val = UnprocessedSubVals.front();
+      BoolValue *Val = UnprocessedSubVals.front();
       UnprocessedSubVals.pop();
 
       if (!SubValsToVar.try_emplace(Val, Var).second)
         continue;
       ++NextVar;
 
-      for (const Formula *F : Val->operands())
-        UnprocessedSubVals.push(F);
-      if (Val->kind() == Formula::AtomRef)
-        Atomics[Var] = Val->getAtom();
+      // Visit the sub-values of `Val`.
+      switch (Val->getKind()) {
+      case Value::Kind::Conjunction: {
+        auto *C = cast<ConjunctionValue>(Val);
+        UnprocessedSubVals.push(&C->getLeftSubValue());
+        UnprocessedSubVals.push(&C->getRightSubValue());
+        break;
+      }
+      case Value::Kind::Disjunction: {
+        auto *D = cast<DisjunctionValue>(Val);
+        UnprocessedSubVals.push(&D->getLeftSubValue());
+        UnprocessedSubVals.push(&D->getRightSubValue());
+        break;
+      }
+      case Value::Kind::Negation: {
+        auto *N = cast<NegationValue>(Val);
+        UnprocessedSubVals.push(&N->getSubVal());
+        break;
+      }
+      case Value::Kind::Implication: {
+        auto *I = cast<ImplicationValue>(Val);
+        UnprocessedSubVals.push(&I->getLeftSubValue());
+        UnprocessedSubVals.push(&I->getRightSubValue());
+        break;
+      }
+      case Value::Kind::Biconditional: {
+        auto *B = cast<BiconditionalValue>(Val);
+        UnprocessedSubVals.push(&B->getLeftSubValue());
+        UnprocessedSubVals.push(&B->getRightSubValue());
+        break;
+      }
+      case Value::Kind::TopBool:
+        // Nothing more to do. This `TopBool` instance has already been mapped
+        // to a fresh solver variable (`NextVar`, above) and is thereafter
+        // anonymous. The solver never sees `Top`.
+        break;
+      case Value::Kind::AtomicBool: {
+        Atomics[Var] = cast<AtomicBoolValue>(Val);
+        break;
+      }
+      default:
+        llvm_unreachable("buildBooleanFormula: unhandled value kind");
+      }
     }
   }
 
-  auto GetVar = [&SubValsToVar](const Formula *Val) {
+  auto GetVar = [&SubValsToVar](const BoolValue *Val) {
     auto ValIt = SubValsToVar.find(Val);
     assert(ValIt != SubValsToVar.end());
     return ValIt->second;
   };
 
-  CNFFormula CNF(NextVar - 1, std::move(Atomics));
+  BooleanFormula Formula(NextVar - 1, std::move(Atomics));
   std::vector<bool> ProcessedSubVals(NextVar, false);
 
-  // Add a conjunct for each variable that represents a top-level formula in
-  // `Vals`.
-  for (const Formula *Val : Vals)
-    CNF.addClause(posLit(GetVar(Val)));
+  // Add a conjunct for each variable that represents a top-level conjunction
+  // value in `Vals`.
+  for (BoolValue *Val : Vals)
+    Formula.addClause(posLit(GetVar(Val)));
 
   // Add conjuncts that represent the mapping between newly-created variables
-  // and their corresponding sub-formulas.
-  std::queue<const Formula *> UnprocessedSubVals;
-  for (const Formula *Val : Vals)
+  // and their corresponding sub-values.
+  std::queue<BoolValue *> UnprocessedSubVals;
+  for (BoolValue *Val : Vals)
     UnprocessedSubVals.push(Val);
   while (!UnprocessedSubVals.empty()) {
-    const Formula *Val = UnprocessedSubVals.front();
+    const BoolValue *Val = UnprocessedSubVals.front();
     UnprocessedSubVals.pop();
     const Variable Var = GetVar(Val);
 
@@ -238,107 +277,117 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
       continue;
     ProcessedSubVals[Var] = true;
 
-    switch (Val->kind()) {
-    case Formula::AtomRef:
-      break;
-    case Formula::And: {
-      const Variable LHS = GetVar(Val->operands()[0]);
-      const Variable RHS = GetVar(Val->operands()[1]);
+    if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&C->getRightSubValue());
 
-      if (LHS == RHS) {
+      if (LeftSubVar == RightSubVar) {
         // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
+        Formula.addClause(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
+
+        // Visit a sub-value of `Val` (pick any, they are identical).
+        UnprocessedSubVals.push(&C->getLeftSubValue());
       } else {
         // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
         // which is already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(negLit(Var), posLit(RHS));
-        CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+        Formula.addClause(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(negLit(Var), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&C->getLeftSubValue());
+        UnprocessedSubVals.push(&C->getRightSubValue());
       }
-      break;
-    }
-    case Formula::Or: {
-      const Variable LHS = GetVar(Val->operands()[0]);
-      const Variable RHS = GetVar(Val->operands()[1]);
+    } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&D->getRightSubValue());
 
-      if (LHS == RHS) {
+      if (LeftSubVar == RightSubVar) {
         // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
+        Formula.addClause(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
+
+        // Visit a sub-value of `Val` (pick any, they are identical).
+        UnprocessedSubVals.push(&D->getLeftSubValue());
       } else {
-        // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
-        // !B)` which is already in conjunctive normal form. Below we add each
-        // of the conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
-        CNF.addClause(posLit(Var), negLit(RHS));
+        // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
+        // which is already in conjunctive normal form. Below we add each of the
+        // conjuncts of the latter expression to the result.
+        Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&D->getLeftSubValue());
+        UnprocessedSubVals.push(&D->getRightSubValue());
       }
-      break;
-    }
-    case Formula::Not: {
-      const Variable Operand = GetVar(Val->operands()[0]);
-
-      // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
-      // already in conjunctive normal form. Below we add each of the
-      // conjuncts of the latter expression to the result.
-      CNF.addClause(negLit(Var), negLit(Operand));
-      CNF.addClause(posLit(Var), posLit(Operand));
-      break;
-    }
-    case Formula::Implies: {
-      const Variable LHS = GetVar(Val->operands()[0]);
-      const Variable RHS = GetVar(Val->operands()[1]);
+    } else if (auto *N = dyn_cast<NegationValue>(Val)) {
+      const Variable SubVar = GetVar(&N->getSubVal());
+
+      // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
+      // conjunctive normal form. Below we add each of the conjuncts of the
+      // latter expression to the result.
+      Formula.addClause(negLit(Var), negLit(SubVar));
+      Formula.addClause(posLit(Var), posLit(SubVar));
+
+      // Visit the sub-values of `Val`.
+      UnprocessedSubVals.push(&N->getSubVal());
+    } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&I->getRightSubValue());
 
       // `X <=> (A => B)` is equivalent to
       // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
-      // conjunctive normal form. Below we add each of the conjuncts of
-      // the latter expression to the result.
-      CNF.addClause(posLit(Var), posLit(LHS));
-      CNF.addClause(posLit(Var), negLit(RHS));
-      CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
-      break;
-    }
-    case Formula::Equal: {
-      const Variable LHS = GetVar(Val->operands()[0]);
-      const Variable RHS = GetVar(Val->operands()[1]);
-
-      if (LHS == RHS) {
+      // conjunctive normal form. Below we add each of the conjuncts of the
+      // latter expression to the result.
+      Formula.addClause(posLit(Var), posLit(LeftSubVar));
+      Formula.addClause(posLit(Var), negLit(RightSubVar));
+      Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
+
+      // Visit the sub-values of `Val`.
+      UnprocessedSubVals.push(&I->getLeftSubValue());
+      UnprocessedSubVals.push(&I->getRightSubValue());
+    } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&B->getRightSubValue());
+
+      if (LeftSubVar == RightSubVar) {
         // `X <=> (A <=> A)` is equvalent to `X` which is already in
         // conjunctive normal form. Below we add each of the conjuncts of the
         // latter expression to the result.
-        CNF.addClause(posLit(Var));
+        Formula.addClause(posLit(Var));
 
         // No need to visit the sub-values of `Val`.
-        continue;
+      } else {
+        // `X <=> (A <=> B)` is equivalent to
+        // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
+        // already in conjunctive normal form. Below we add each of the conjuncts
+        // of the latter expression to the result.
+        Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+        Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
+        Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&B->getLeftSubValue());
+        UnprocessedSubVals.push(&B->getRightSubValue());
       }
-      // `X <=> (A <=> B)` is equivalent to
-      // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
-      // is already in conjunctive normal form. Below we add each of the
-      // conjuncts of the latter expression to the result.
-      CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS));
-      CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
-      CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS));
-      CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
-      break;
-    }
     }
-    for (const Formula *Child : Val->operands())
-      UnprocessedSubVals.push(Child);
   }
 
-  return CNF;
+  return Formula;
 }
 
 class WatchedLiteralsSolverImpl {
   /// A boolean formula in conjunctive normal form that the solver will attempt
   /// to prove satisfiable. The formula will be modified in the process.
-  CNFFormula CNF;
+  BooleanFormula Formula;
 
   /// The search for a satisfying assignment of the variables in `Formula` will
   /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -390,10 +439,9 @@ class WatchedLiteralsSolverImpl {
   std::vector<Variable> ActiveVars;
 
 public:
-  explicit WatchedLiteralsSolverImpl(
-      const llvm::ArrayRef<const Formula *> &Vals)
-      : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
-        LevelStates(CNF.LargestVar + 1) {
+  explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
+      : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
+        LevelStates(Formula.LargestVar + 1) {
     assert(!Vals.empty());
 
     // Initialize the state at the root level to a decision so that in
@@ -402,10 +450,10 @@ class WatchedLiteralsSolverImpl {
     LevelStates[0] = State::Decision;
 
     // Initialize all variables as unassigned.
-    VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
+    VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
 
     // Initialize the active variables.
-    for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
+    for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
         ActiveVars.push_back(Var);
     }
@@ -426,7 +474,7 @@ class WatchedLiteralsSolverImpl {
       // 3. Unassigned variables that form watched literals are active.
       // FIXME: Consider replacing these with test cases that fail if the any
       // of the invariants is broken. That might not be easy due to the
-      // transformations performed by `buildCNF`.
+      // transformations performed by `buildBooleanFormula`.
       assert(activeVarsAreUnassigned());
       assert(activeVarsFormWatchedLiterals());
       assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -507,10 +555,12 @@ class WatchedLiteralsSolverImpl {
   }
 
 private:
-  /// Returns a satisfying truth assignment to the atoms in the boolean formula.
-  llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
-    llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
-    for (auto &Atomic : CNF.Atomics) {
+  /// Returns a satisfying truth assignment to the atomic values in the boolean
+  /// formula.
+  llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
+  buildSolution() {
+    llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
+    for (auto &Atomic : Formula.Atomics) {
       // A variable may have a definite true/false assignment, or it may be
       // unassigned indicating its truth value does not affect the result of
       // the formula. Unassigned variables are assigned to true as a default.
@@ -546,24 +596,24 @@ class WatchedLiteralsSolverImpl {
     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
                                  ? negLit(Var)
                                  : posLit(Var);
-    ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
-    CNF.WatchedHead[FalseLit] = NullClause;
+    ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
+    Formula.WatchedHead[FalseLit] = NullClause;
     while (FalseLitWatcher != NullClause) {
-      const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
+      const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
 
       // Pick the first non-false literal as the new watched literal.
-      const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
+      const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
       size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
-      while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
+      while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
         ++NewWatchedLitIdx;
-      const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
+      const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
       const Variable NewWatchedLitVar = var(NewWatchedLit);
 
       // Swap the old watched literal for the new one in `FalseLitWatcher` to
       // maintain the invariant that the watched literal is at the beginning of
       // the clause.
-      CNF.Clauses[NewWatchedLitIdx] = FalseLit;
-      CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+      Formula.Clauses[NewWatchedLitIdx] = FalseLit;
+      Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
 
       // If the new watched literal isn't watched by any other clause and its
       // variable isn't assigned we need to add it to the active variables.
@@ -571,8 +621,8 @@ class WatchedLiteralsSolverImpl {
           VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
         ActiveVars.push_back(NewWatchedLitVar);
 
-      CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
-      CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+      Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
+      Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
 
       // Go to the next clause that watches `FalseLit`.
       FalseLitWatcher = NextFalseLitWatcher;
@@ -582,15 +632,16 @@ class WatchedLiteralsSolverImpl {
   /// Returns true if and only if one of the clauses that watch `Lit` is a unit
   /// clause.
   bool watchedByUnitClause(Literal Lit) const {
-    for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
-         LitWatcher = CNF.NextWatched[LitWatcher]) {
-      llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
+    for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
+         LitWatcher != NullClause;
+         LitWatcher = Formula.NextWatched[LitWatcher]) {
+      llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
 
       // Assert the invariant that the watched literal is always the first one
       // in the clause.
       // FIXME: Consider replacing this with a test case that fails if the
       // invariant is broken by `updateWatchedLiterals`. That might not be easy
-      // due to the transformations performed by `buildCNF`.
+      // due to the transformations performed by `buildBooleanFormula`.
       assert(Clause.front() == Lit);
 
       if (isUnit(Clause))
@@ -614,7 +665,7 @@ class WatchedLiteralsSolverImpl {
 
   /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
   bool isWatched(Literal Lit) const {
-    return CNF.WatchedHead[Lit] != NullClause;
+    return Formula.WatchedHead[Lit] != NullClause;
   }
 
   /// Returns an assignment for an unassigned variable.
@@ -627,8 +678,8 @@ class WatchedLiteralsSolverImpl {
   /// Returns a set of all watched literals.
   llvm::DenseSet<Literal> watchedLiterals() const {
     llvm::DenseSet<Literal> WatchedLiterals;
-    for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
-      if (CNF.WatchedHead[Lit] == NullClause)
+    for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
+      if (Formula.WatchedHead[Lit] == NullClause)
         continue;
       WatchedLiterals.insert(Lit);
     }
@@ -668,8 +719,7 @@ class WatchedLiteralsSolverImpl {
   }
 };
 
-Solver::Result
-WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
+Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
   if (Vals.empty())
     return Solver::Result::Satisfiable({{}});
   auto [Res, Iterations] =
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
index 53131723ff5ce..407abf58529a5 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -7,7 +7,6 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/Arena.h"
-#include "llvm/Support/ScopedPrinter.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
@@ -126,26 +125,5 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
   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);
-}
-
 } // namespace
 } // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index 8ee56ae08b98a..10fcd204c9ab0 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -8,9 +8,8 @@
 
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
-#include "llvm/Support/ScopedPrinter.h"
-#include "llvm/Support/raw_ostream.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
@@ -23,88 +22,429 @@ using test::ConstraintContext;
 using testing::StrEq;
 
 TEST(BoolValueDebugStringTest, AtomicBoolean) {
+  // B0
   ConstraintContext Ctx;
   auto B = Ctx.atom();
 
-  auto Expected = "V0";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"(B0)";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
+}
+
+TEST(BoolValueDebugStringTest, Top) {
+  ConstraintContext Ctx;
+  auto B = Ctx.top();
+
+  auto Expected = R"(top)";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Negation) {
+  // !B0
   ConstraintContext Ctx;
   auto B = Ctx.neg(Ctx.atom());
 
-  auto Expected = "!V0";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((not
+    B0))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Conjunction) {
+  // B0 ^ B1
   ConstraintContext Ctx;
   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
 
-  auto Expected = "(V0 & V1)";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((and
+    B0
+    B1))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Disjunction) {
+  // B0 v B1
   ConstraintContext Ctx;
   auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
 
-  auto Expected = "(V0 | V1)";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((or
+    B0
+    B1))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Implication) {
+  // B0 => B1
   ConstraintContext Ctx;
   auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
 
-  auto Expected = "(V0 => V1)";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((=>
+    B0
+    B1))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Iff) {
+  // B0 <=> B1
   ConstraintContext Ctx;
   auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
 
-  auto Expected = "(V0 = V1)";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((=
+    B0
+    B1))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Xor) {
+  // (B0 ^ !B1) V (!B0 ^ B1)
   ConstraintContext Ctx;
   auto B0 = Ctx.atom();
   auto B1 = Ctx.atom();
   auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
 
-  auto Expected = "((V0 & !V1) | (!V0 & V1))";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((or
+    (and
+        B0
+        (not
+            B1))
+    (and
+        (not
+            B0)
+        B1)))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, NestedBoolean) {
+  // B0 ^ (B1 v (B2 ^ (B3 v B4)))
   ConstraintContext Ctx;
   auto B = Ctx.conj(
       Ctx.atom(),
       Ctx.disj(Ctx.atom(),
                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
 
-  auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
-  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+  auto Expected = R"((and
+    B0
+    (or
+        B1
+        (and
+            B2
+            (or
+                B3
+                B4)))))";
+  EXPECT_THAT(debugString(*B), StrEq(Expected));
+}
+
+TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
+  // True
+  ConstraintContext Ctx;
+  auto True = cast<AtomicBoolValue>(Ctx.atom());
+  auto B = True;
+
+  auto Expected = R"(True)";
+  EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
+}
+
+TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
+  // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
+  ConstraintContext Ctx;
+  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
+  auto Then = cast<AtomicBoolValue>(Ctx.atom());
+  auto Else = cast<AtomicBoolValue>(Ctx.atom());
+  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
+                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
+
+  auto Expected = R"((or
+    (and
+        Cond
+        (and
+            Then
+            (not
+                Else)))
+    (and
+        (not
+            Cond)
+        (and
+            (not
+                Then)
+            Else))))";
+  EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
+              StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
+  // (False && B0) v (True v B1)
   ConstraintContext Ctx;
-  auto True = Ctx.atom();
-  auto False = Ctx.atom();
-  Formula::AtomNames Names;
-  Names[True->getAtom()] = "true";
-  Names[False->getAtom()] = "false";
+  auto True = cast<AtomicBoolValue>(Ctx.atom());
+  auto False = cast<AtomicBoolValue>(Ctx.atom());
   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
 
-  auto Expected = R"(((false & V2) | (true | V3)))";
-  std::string Actual;
-  llvm::raw_string_ostream OS(Actual);
-  B->print(OS, &Names);
-  EXPECT_THAT(Actual, StrEq(Expected));
+  auto Expected = R"((or
+    (and
+        False
+        B0)
+    (or
+        True
+        B1)))";
+  EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
+              StrEq(Expected));
+}
+
+TEST(ConstraintSetDebugStringTest, Empty) {
+  llvm::ArrayRef<BoolValue *> Constraints;
+  EXPECT_THAT(debugString(Constraints), StrEq(""));
+}
+
+TEST(ConstraintSetDebugStringTest, Simple) {
+  ConstraintContext Ctx;
+  std::vector<BoolValue *> Constraints;
+  auto X = cast<AtomicBoolValue>(Ctx.atom());
+  auto Y = cast<AtomicBoolValue>(Ctx.atom());
+  Constraints.push_back(Ctx.disj(X, Y));
+  Constraints.push_back(Ctx.disj(X, Ctx.neg(Y)));
+
+  auto Expected = R"((or
+    X
+    Y)
+(or
+    X
+    (not
+        Y))
+)";
+  EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
+              StrEq(Expected));
+}
+
+Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
+  return WatchedLiteralsSolver().solve(std::move(Constraints));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBoolean) {
+  // B0
+  ConstraintContext Ctx;
+  std::vector<BoolValue *> Constraints({Ctx.atom()});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+------------
+Satisfiable.
+
+B0 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
+  // B0, !B0
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(not
+    B0)
+------------
+Unsatisfiable.
+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
+  // B0, B1
+  ConstraintContext Ctx;
+  std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+B1
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Implication) {
+  // B0, B0 => B1
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  auto B1 = Ctx.atom();
+  auto Impl = Ctx.disj(Ctx.neg(B0), B1);
+  std::vector<BoolValue *> Constraints({B0, Impl});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(or
+    (not
+        B0)
+    B1)
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
 }
 
+TEST(SATCheckDebugStringTest, Iff) {
+  // B0, B0 <=> B1
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  auto B1 = Ctx.atom();
+  auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
+  std::vector<BoolValue *> Constraints({B0, Iff});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(and
+    (or
+        (not
+            B0)
+        B1)
+    (or
+        B0
+        (not
+            B1)))
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Xor) {
+  // B0, XOR(B0, B1)
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  auto B1 = Ctx.atom();
+  auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
+  std::vector<BoolValue *> Constraints({B0, XOR});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(or
+    (and
+        B0
+        (not
+            B1))
+    (and
+        (not
+            B0)
+        B1))
+------------
+Satisfiable.
+
+B0 = True
+B1 = False
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
+  // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
+  ConstraintContext Ctx;
+  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
+  auto Then = cast<AtomicBoolValue>(Ctx.atom());
+  auto Else = cast<AtomicBoolValue>(Ctx.atom());
+  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
+                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
+  std::vector<BoolValue *> Constraints({Cond, B});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+Cond
+
+(or
+    (and
+        Cond
+        (and
+            Then
+            (not
+                Else)))
+    (and
+        (not
+            Cond)
+        (and
+            (not
+                Then)
+            Else)))
+------------
+Satisfiable.
+
+Cond = True
+Else = False
+Then = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result,
+                          {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
+              StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
+  // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
+  ConstraintContext Ctx;
+  auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
+  auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+  auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+  auto BothZeroImpliesEQ =
+      Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
+  std::vector<BoolValue *> Constraints(
+      {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+ThisIntEqZero
+
+(not
+    IntsAreEq)
+
+(or
+    (not
+        (and
+            ThisIntEqZero
+            OtherIntEqZero))
+    IntsAreEq)
+------------
+Satisfiable.
+
+IntsAreEq      = False
+OtherIntEqZero = False
+ThisIntEqZero  = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result,
+                          {{IntsAreEq, "IntsAreEq"},
+                           {ThisIntEqZero, "ThisIntEqZero"},
+                           {OtherIntEqZero, "OtherIntEqZero"}}),
+              StrEq(Expected));
+}
 } // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index ba0a77a910d7c..9999dd3a475f1 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -9,10 +9,9 @@
 #include <utility>
 
 #include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
-#include "llvm/ADT/ArrayRef.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
@@ -24,31 +23,26 @@ using namespace dataflow;
 using test::ConstraintContext;
 using testing::_;
 using testing::AnyOf;
+using testing::IsEmpty;
+using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
 
-constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
-constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
-
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
-Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
+Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
   return WatchedLiteralsSolver().solve(Vals);
 }
 
-MATCHER(unsat, "") {
-  return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
+void expectUnsatisfiable(Solver::Result Result) {
+  EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
+  EXPECT_FALSE(Result.getSolution().has_value());
 }
-MATCHER_P(sat, SolutionMatcher,
-          "is satisfiable, where solution " +
-              (testing::DescribeMatcher<
-                  llvm::DenseMap<Atom, Solver::Result::Assignment>>(
-                  SolutionMatcher))) {
-  if (arg.getStatus() != Solver::Result::Status::Satisfiable)
-    return false;
-  auto Solution = *arg.getSolution();
-  return testing::ExplainMatchResult(SolutionMatcher, Solution,
-                                     result_listener);
+
+template <typename Matcher>
+void expectSatisfiable(Solver::Result Result, Matcher Solution) {
+  EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
+  EXPECT_THAT(Result.getSolution(), Optional(Solution));
 }
 
 TEST(SolverTest, Var) {
@@ -56,8 +50,9 @@ TEST(SolverTest, Var) {
   auto X = Ctx.atom();
 
   // X
-  EXPECT_THAT(solve({X}),
-              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
+  expectSatisfiable(
+      solve({X}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST(SolverTest, NegatedVar) {
@@ -66,8 +61,9 @@ TEST(SolverTest, NegatedVar) {
   auto NotX = Ctx.neg(X);
 
   // !X
-  EXPECT_THAT(solve({NotX}),
-              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
+  expectSatisfiable(
+      solve({NotX}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
 }
 
 TEST(SolverTest, UnitConflict) {
@@ -76,7 +72,7 @@ TEST(SolverTest, UnitConflict) {
   auto NotX = Ctx.neg(X);
 
   // X ^ !X
-  EXPECT_THAT(solve({X, NotX}), unsat());
+  expectUnsatisfiable(solve({X, NotX}));
 }
 
 TEST(SolverTest, DistinctVars) {
@@ -86,9 +82,36 @@ TEST(SolverTest, DistinctVars) {
   auto NotY = Ctx.neg(Y);
 
   // X ^ !Y
-  EXPECT_THAT(solve({X, NotY}),
-              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
-                                       Pair(Y->getAtom(), AssignedFalse))));
+  expectSatisfiable(
+      solve({X, NotY}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+                           Pair(Y, Solver::Result::Assignment::AssignedFalse)));
+}
+
+TEST(SolverTest, Top) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+
+  // X. Since Top is anonymous, we do not get any results in the solution.
+  expectSatisfiable(solve({X}), IsEmpty());
+}
+
+TEST(SolverTest, NegatedTop) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+
+  // !X
+  expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
+}
+
+TEST(SolverTest, DistinctTops) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+  auto Y = Ctx.top();
+  auto NotY = Ctx.neg(Y);
+
+  // X ^ !Y
+  expectSatisfiable(solve({X, NotY}), IsEmpty());
 }
 
 TEST(SolverTest, DoubleNegation) {
@@ -98,7 +121,7 @@ TEST(SolverTest, DoubleNegation) {
   auto NotNotX = Ctx.neg(NotX);
 
   // !!X ^ !X
-  EXPECT_THAT(solve({NotNotX, NotX}), unsat());
+  expectUnsatisfiable(solve({NotNotX, NotX}));
 }
 
 TEST(SolverTest, NegatedDisjunction) {
@@ -109,7 +132,7 @@ TEST(SolverTest, NegatedDisjunction) {
   auto NotXOrY = Ctx.neg(XOrY);
 
   // !(X v Y) ^ (X v Y)
-  EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
+  expectUnsatisfiable(solve({NotXOrY, XOrY}));
 }
 
 TEST(SolverTest, NegatedConjunction) {
@@ -120,7 +143,7 @@ TEST(SolverTest, NegatedConjunction) {
   auto NotXAndY = Ctx.neg(XAndY);
 
   // !(X ^ Y) ^ (X ^ Y)
-  EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
+  expectUnsatisfiable(solve({NotXAndY, XAndY}));
 }
 
 TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -130,7 +153,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) {
   auto XOrNotX = Ctx.disj(X, NotX);
 
   // X v !X
-  EXPECT_THAT(solve({XOrNotX}), sat(_));
+  expectSatisfiable(solve({XOrNotX}), _);
 }
 
 TEST(SolverTest, DisjunctionSameVar) {
@@ -139,7 +162,7 @@ TEST(SolverTest, DisjunctionSameVar) {
   auto XOrX = Ctx.disj(X, X);
 
   // X v X
-  EXPECT_THAT(solve({XOrX}), sat(_));
+  expectSatisfiable(solve({XOrX}), _);
 }
 
 TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -149,7 +172,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
   auto XAndNotX = Ctx.conj(X, NotX);
 
   // X ^ !X
-  EXPECT_THAT(solve({XAndNotX}), unsat());
+  expectUnsatisfiable(solve({XAndNotX}));
 }
 
 TEST(SolverTest, ConjunctionSameVar) {
@@ -158,7 +181,7 @@ TEST(SolverTest, ConjunctionSameVar) {
   auto XAndX = Ctx.conj(X, X);
 
   // X ^ X
-  EXPECT_THAT(solve({XAndX}), sat(_));
+  expectSatisfiable(solve({XAndX}), _);
 }
 
 TEST(SolverTest, PureVar) {
@@ -171,9 +194,10 @@ TEST(SolverTest, PureVar) {
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 
   // (!X v Y) ^ (!X v !Y)
-  EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
-              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
-                                       Pair(Y->getAtom(), _))));
+  expectSatisfiable(
+      solve({NotXOrY, NotXOrNotY}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+                           Pair(Y, _)));
 }
 
 TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -187,9 +211,10 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
-  EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
-              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
-                                       Pair(Y->getAtom(), AssignedTrue))));
+  expectSatisfiable(
+      solve({XOrY, NotXOrY, NotXOrNotY}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST(SolverTest, DeepConflict) {
@@ -204,7 +229,7 @@ TEST(SolverTest, DeepConflict) {
   auto XOrNotY = Ctx.disj(X, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
-  EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
+  expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
 }
 
 TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -218,7 +243,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
   auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
 
   // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
-  EXPECT_THAT(solve({NotEquivalent}), unsat());
+  expectUnsatisfiable(solve({NotEquivalent}));
 }
 
 TEST(SolverTest, IffSameVars) {
@@ -227,7 +252,7 @@ TEST(SolverTest, IffSameVars) {
   auto XEqX = Ctx.iff(X, X);
 
   // X <=> X
-  EXPECT_THAT(solve({XEqX}), sat(_));
+  expectSatisfiable(solve({XEqX}), _);
 }
 
 TEST(SolverTest, IffDistinctVars) {
@@ -237,12 +262,14 @@ TEST(SolverTest, IffDistinctVars) {
   auto XEqY = Ctx.iff(X, Y);
 
   // X <=> Y
-  EXPECT_THAT(
+  expectSatisfiable(
       solve({XEqY}),
-      sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
-                                     Pair(Y->getAtom(), AssignedTrue)),
-                UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
-                                     Pair(Y->getAtom(), AssignedFalse)))));
+      AnyOf(UnorderedElementsAre(
+                Pair(X, Solver::Result::Assignment::AssignedTrue),
+                Pair(Y, Solver::Result::Assignment::AssignedTrue)),
+            UnorderedElementsAre(
+                Pair(X, Solver::Result::Assignment::AssignedFalse),
+                Pair(Y, Solver::Result::Assignment::AssignedFalse))));
 }
 
 TEST(SolverTest, IffWithUnits) {
@@ -252,9 +279,10 @@ TEST(SolverTest, IffWithUnits) {
   auto XEqY = Ctx.iff(X, Y);
 
   // (X <=> Y) ^ X ^ Y
-  EXPECT_THAT(solve({XEqY, X, Y}),
-              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
-                                       Pair(Y->getAtom(), AssignedTrue))));
+  expectSatisfiable(
+      solve({XEqY, X, Y}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST(SolverTest, IffWithUnitsConflict) {
@@ -265,7 +293,7 @@ TEST(SolverTest, IffWithUnitsConflict) {
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X  !Y
-  EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
+  expectUnsatisfiable(solve({XEqY, X, NotY}));
 }
 
 TEST(SolverTest, IffTransitiveConflict) {
@@ -278,7 +306,7 @@ TEST(SolverTest, IffTransitiveConflict) {
   auto NotX = Ctx.neg(X);
 
   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
-  EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
+  expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
 }
 
 TEST(SolverTest, DeMorgan) {
@@ -295,7 +323,7 @@ TEST(SolverTest, DeMorgan) {
   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
 
   // A ^ B
-  EXPECT_THAT(solve({A, B}), sat(_));
+  expectSatisfiable(solve({A, B}), _);
 }
 
 TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -306,7 +334,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X ^ !Y
-  EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
+  expectUnsatisfiable(solve({XEqY, X, NotY}));
 }
 
 TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -318,7 +346,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) {
   auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
 
   // !((X => Y) <=> (!X v Y))
-  EXPECT_THAT(solve({NotEquivalent}), unsat());
+  expectUnsatisfiable(solve({NotEquivalent}));
 }
 
 TEST(SolverTest, ImplicationConflict) {
@@ -329,7 +357,7 @@ TEST(SolverTest, ImplicationConflict) {
   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
 
   // X => Y ^ X ^ !Y
-  EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
+  expectUnsatisfiable(solve({XImplY, XAndNotY}));
 }
 
 TEST(SolverTest, LowTimeoutResultsInTimedOut) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index 93991d87d77f2..e258eb7e75f59 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -43,7 +43,6 @@
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringMap.h"
 #include "llvm/ADT/StringRef.h"
-#include "llvm/Support/Allocator.h"
 #include "llvm/Support/Errc.h"
 #include "llvm/Support/Error.h"
 #include "llvm/Testing/Annotations/Annotations.h"
@@ -443,44 +442,55 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
 
 /// Creates and owns constraints which are boolean values.
 class ConstraintContext {
-  unsigned NextAtom = 0;
-  llvm::BumpPtrAllocator A;
-
-  const Formula *make(Formula::Kind K,
-                      llvm::ArrayRef<const Formula *> Operands) {
-    return &Formula::create(A, K, Operands);
+public:
+  // Creates an atomic boolean value.
+  BoolValue *atom() {
+    Vals.push_back(std::make_unique<AtomicBoolValue>());
+    return Vals.back().get();
   }
 
-public:
-  // Returns a reference to a fresh atomic variable.
-  const Formula *atom() {
-    return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
+  // Creates an instance of the Top boolean value.
+  BoolValue *top() {
+    Vals.push_back(std::make_unique<TopBoolValue>());
+    return Vals.back().get();
   }
 
-  // Creates a boolean conjunction.
-  const Formula *conj(const Formula *LHS, const Formula *RHS) {
-    return make(Formula::And, {LHS, RHS});
+  // Creates a boolean conjunction value.
+  BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+    Vals.push_back(
+        std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
+    return Vals.back().get();
   }
 
-  // Creates a boolean disjunction.
-  const Formula *disj(const Formula *LHS, const Formula *RHS) {
-    return make(Formula::Or, {LHS, RHS});
+  // Creates a boolean disjunction value.
+  BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+    Vals.push_back(
+        std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
+    return Vals.back().get();
   }
 
-  // Creates a boolean negation.
-  const Formula *neg(const Formula *Operand) {
-    return make(Formula::Not, {Operand});
+  // Creates a boolean negation value.
+  BoolValue *neg(BoolValue *SubVal) {
+    Vals.push_back(std::make_unique<NegationValue>(*SubVal));
+    return Vals.back().get();
   }
 
-  // Creates a boolean implication.
-  const Formula *impl(const Formula *LHS, const Formula *RHS) {
-    return make(Formula::Implies, {LHS, RHS});
+  // Creates a boolean implication value.
+  BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+    Vals.push_back(
+        std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
+    return Vals.back().get();
   }
 
-  // Creates a boolean biconditional.
-  const Formula *iff(const Formula *LHS, const Formula *RHS) {
-    return make(Formula::Equal, {LHS, RHS});
+  // Creates a boolean biconditional value.
+  BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+    Vals.push_back(
+        std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
+    return Vals.back().get();
   }
+
+private:
+  std::vector<std::unique_ptr<BoolValue>> Vals;
 };
 
 } // namespace test