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
@@ -161,8 +161,9 @@
   /// `Val2` imposed by the flow condition.
   bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
 
-  LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
-                                          llvm::raw_ostream &OS = llvm::dbgs());
+  LLVM_DUMP_METHOD void
+  dumpFlowCondition(Atom Token, llvm::raw_ostream &OS = llvm::dbgs(),
+                    llvm::function_ref<Formula::DelegatePrinter> = nullptr);
 
   /// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
   /// returns null.
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
@@ -548,7 +548,9 @@
   Arena &arena() const { return DACtx->arena(); }
 
   LLVM_DUMP_METHOD void dump() const;
-  LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;
+  LLVM_DUMP_METHOD void
+  dump(raw_ostream &OS,
+       llvm::function_ref<Formula::DelegatePrinter> = nullptr) const;
 
 private:
   /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
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
@@ -189,8 +189,9 @@
   }
 }
 
-void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
-                                                llvm::raw_ostream &OS) {
+void DataflowAnalysisContext::dumpFlowCondition(
+    Atom Token, llvm::raw_ostream &OS,
+    llvm::function_ref<Formula::DelegatePrinter> OuterDelegate) {
   llvm::DenseSet<const Formula *> Constraints = {&arena().makeAtomRef(Token)};
   llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
@@ -199,6 +200,8 @@
   auto &True = arena().makeLiteral(true);
   auto &False = arena().makeLiteral(false);
   auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
+    if (OuterDelegate(OS, F))
+      return true;
     if (&F == &True) {
       OS << "True";
       return true;
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
@@ -898,7 +898,9 @@
   return flowConditionImplies(Val.formula());
 }
 
-void Environment::dump(raw_ostream &OS) const {
+void Environment::dump(
+    raw_ostream &OS,
+    llvm::function_ref<Formula::DelegatePrinter> Delegate) const {
   // FIXME: add printing for remaining fields and allow caller to decide what
   // fields are printed.
   OS << "DeclToLoc:\n";
@@ -914,8 +916,8 @@
     OS << "  [" << L << ", " << V << ": " << *V << "]\n";
   }
 
-  OS << "FlowConditionToken:\n";
-  DACtx->dumpFlowCondition(FlowConditionToken, OS);
+  OS << "Flow condition:\n";
+  DACtx->dumpFlowCondition(FlowConditionToken, OS, Delegate);
 }
 
 void Environment::dump() const {
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
@@ -154,6 +154,8 @@
   std::vector<std::pair<const CFGBlock *, unsigned>> Iters;
   // Number of times each CFG block has been seen.
   llvm::DenseMap<const CFGBlock *, unsigned> BlockIters;
+  // Labels assigned to SAT atoms.
+  llvm::DenseMap<Atom, std::string> AtomNames;
   // The messages logged in the current context but not yet written.
   std::string ContextLogs;
   // The number of elements we have visited within the current CFG block.
@@ -245,6 +247,9 @@
   void recordState(TypeErasedDataflowAnalysisState &State) override {
     unsigned Block = Iters.back().first->getBlockID();
     unsigned Iter = Iters.back().second;
+    AtomNames.try_emplace(State.Env.getFlowConditionToken(),
+                          iterID(Block, Iter));
+
     JOS->attributeObject(elementIterID(Block, Iter, ElementIndex), [&] {
       JOS->attribute("block", blockID(Block));
       JOS->attribute("iter", Iter);
@@ -266,7 +271,17 @@
       {
         std::string BuiltinLattice;
         llvm::raw_string_ostream BuiltinLatticeS(BuiltinLattice);
-        State.Env.dump(BuiltinLatticeS);
+        State.Env.dump(BuiltinLatticeS,
+                       [&](llvm::raw_ostream &OS, const Formula &F) {
+                         if (F.kind() == Formula::AtomRef) {
+                           if (auto It = AtomNames.find(F.atom());
+                               It != AtomNames.end()) {
+                             OS << It->second;
+                             return true;
+                           }
+                         }
+                         return false;
+                       });
         JOS->attribute("builtinLattice", BuiltinLattice);
       }
     });