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
@@ -20,7 +20,9 @@
 /// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
 class Arena {
 public:
-  Arena() : True(makeAtom()), False(makeAtom()) {}
+  Arena()
+      : True(Formula::create(Alloc, Formula::Literal, {}, 1)),
+        False(Formula::create(Alloc, Formula::Literal, {}, 0)) {}
   Arena(const Arena &) = delete;
   Arena &operator=(const Arena &) = delete;
 
@@ -106,9 +108,7 @@
   const Formula &makeAtomRef(Atom A);
 
   /// Returns a formula for a literal true/false.
-  const Formula &makeLiteral(bool Value) {
-    return makeAtomRef(Value ? True : False);
-  }
+  const Formula &makeLiteral(bool Value) { return Value ? True : False; }
 
   // Parses a formula from its textual representation.
   // This may refer to atoms that were not produced by makeAtom() yet!
@@ -144,7 +144,7 @@
   llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
   unsigned NextAtom = 0;
 
-  Atom True, False;
+  const Formula &True, &False;
 };
 
 } // namespace clang::dataflow
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
@@ -466,9 +466,8 @@
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`
-  AtomicBoolValue &getBoolLiteralValue(bool Value) const {
-    return cast<AtomicBoolValue>(
-        arena().makeBoolValue(arena().makeLiteral(Value)));
+  BoolValue &getBoolLiteralValue(bool Value) const {
+    return arena().makeBoolValue(arena().makeLiteral(Value));
   }
 
   /// Returns an atomic boolean value.
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h
--- a/clang/include/clang/Analysis/FlowSensitive/Formula.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -53,7 +53,8 @@
     /// 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
+    /// Constant true or false.
+    Literal,
 
     Not, /// True if its only operand is false
 
@@ -70,6 +71,11 @@
     return static_cast<Atom>(Value);
   }
 
+  bool literal() const {
+    assert(kind() == Literal);
+    return static_cast<bool>(Value);
+  }
+
   ArrayRef<const Formula *> operands() const {
     return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
                     numOperands(kind()));
@@ -82,9 +88,9 @@
   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);
+  static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+                               ArrayRef<const Formula *> Operands,
+                               unsigned Value = 0);
 
 private:
   Formula() = default;
@@ -94,6 +100,7 @@
   static unsigned numOperands(Kind K) {
     switch (K) {
     case AtomRef:
+    case Literal:
       return 0;
     case Not:
       return 1;
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
@@ -22,63 +22,83 @@
   return Res;
 }
 
-const Formula &Arena::makeAtomRef(Atom A) {
-  auto [It, Inserted] = AtomRefs.try_emplace(A);
+template <class Key, class ComputeFunc>
+const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
+                      ComputeFunc &&Compute) {
+  auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K));
   if (Inserted)
-    It->second =
-        &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+    It->second = Compute();
   return *It->second;
 }
 
-const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return LHS;
+const Formula &Arena::makeAtomRef(Atom A) {
+  return cached(AtomRefs, A, [&] {
+    return &Formula::create(Alloc, Formula::AtomRef, {},
+                            static_cast<unsigned>(A));
+  });
+}
 
-  auto [It, Inserted] =
-      Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
-  return *It->second;
+const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
+  return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
+    if (&LHS == &RHS)
+      return &LHS;
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &LHS;
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &LHS : &RHS;
+
+    return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return LHS;
-
-  auto [It, Inserted] =
-      Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
-  return *It->second;
+  return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
+    if (&LHS == &RHS)
+      return &LHS;
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &LHS : &RHS;
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &RHS : &LHS;
+
+    return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+  });
 }
 
 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;
+  return cached(Nots, &Val, [&] {
+    if (Val.kind() == Formula::Not)
+      return Val.operands()[0];
+    if (Val.kind() == Formula::Literal)
+      return &makeLiteral(!Val.literal());
+
+    return &Formula::create(Alloc, Formula::Not, {&Val});
+  });
 }
 
 const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return makeLiteral(true);
-
-  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;
+  return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
+    if (&LHS == &RHS)
+      return &makeLiteral(true);
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &makeLiteral(true);
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &RHS : &makeNot(LHS);
+
+    return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return makeLiteral(true);
-
-  auto [It, Inserted] =
-      Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
-  return *It->second;
+  return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
+    if (&LHS == &RHS)
+      return &makeLiteral(true);
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &makeNot(RHS);
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &LHS : &makeNot(LHS);
+
+    return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+  });
 }
 
 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
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
@@ -141,8 +141,6 @@
 
 Solver::Result DataflowAnalysisContext::querySolver(
     llvm::SetVector<const Formula *> Constraints) {
-  Constraints.insert(&arena().makeLiteral(true));
-  Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
   return S->solve(Constraints.getArrayRef());
 }
 
@@ -213,13 +211,8 @@
   Constraints.insert(&arena().makeAtomRef(Token));
   addTransitiveFlowConditionConstraints(Token, Constraints);
 
-  // TODO: have formulas know about true/false directly instead
-  Atom True = arena().makeLiteral(true).getAtom();
-  Atom False = arena().makeLiteral(false).getAtom();
-  Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
-
   for (const auto *Constraint : Constraints) {
-    Constraint->print(OS, &Names);
+    Constraint->print(OS);
     OS << "\n";
   }
 }
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -17,8 +17,9 @@
 
 namespace clang::dataflow {
 
-Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
-                         ArrayRef<const Formula *> Operands, unsigned Value) {
+const 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);
@@ -38,6 +39,7 @@
 static llvm::StringLiteral sigil(Formula::Kind K) {
   switch (K) {
   case Formula::AtomRef:
+  case Formula::Literal:
     return "";
   case Formula::Not:
     return "!";
@@ -62,7 +64,16 @@
 
   switch (numOperands(kind())) {
   case 0:
-    OS << getAtom();
+    switch (kind()) {
+    case AtomRef:
+      OS << getAtom();
+      break;
+    case Literal:
+      OS << (literal() ? "true" : "false");
+      break;
+    default:
+      llvm_unreachable("unhandled formula kind");
+    }
     break;
   case 1:
     OS << sigil(kind());
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -322,6 +322,9 @@
     switch (Val->kind()) {
     case Formula::AtomRef:
       break;
+    case Formula::Literal:
+      CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
+      break;
     case Formula::And: {
       const Variable LHS = GetVar(Val->operands()[0]);
       const Variable RHS = GetVar(Val->operands()[1]);
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
@@ -34,12 +34,6 @@
   EXPECT_NE(&X, &Y);
 }
 
-TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.makeAtomRef(A.makeAtom());
-  auto &XAndX = A.makeAnd(X, X);
-  EXPECT_EQ(&XAndX, &X);
-}
-
 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
@@ -55,12 +49,6 @@
   EXPECT_NE(&XAndY1, &XAndZ);
 }
 
-TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.makeAtomRef(A.makeAtom());
-  auto &XOrX = A.makeOr(X, X);
-  EXPECT_EQ(&XOrX, &X);
-}
-
 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
@@ -86,12 +74,6 @@
   EXPECT_NE(&NotX1, &NotY);
 }
 
-TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
-  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.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
@@ -107,12 +89,6 @@
   EXPECT_NE(&XImpliesY1, &XImpliesZ);
 }
 
-TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
-  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.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
@@ -181,5 +157,36 @@
    ^)"));
 }
 
+TEST_F(ArenaTest, IdentitySimplification) {
+  auto &X = A.makeAtomRef(A.makeAtom());
+
+  EXPECT_EQ(&X, &A.makeAnd(X, X));
+  EXPECT_EQ(&X, &A.makeOr(X, X));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
+  EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
+}
+
+TEST_F(ArenaTest, LiteralSimplification) {
+  auto &X = A.makeAtomRef(A.makeAtom());
+
+  EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
+
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
+  EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
+
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
+  EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
+
+  EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
+
+  EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
+}
+
 } // namespace
 } // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -30,6 +30,12 @@
   EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
+TEST(BoolValueDebugStringTest, Literal) {
+  ConstraintContext Ctx;
+  EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true)));
+  EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false)));
+}
+
 TEST(BoolValueDebugStringTest, Negation) {
   ConstraintContext Ctx;
   auto B = Ctx.neg(Ctx.atom());
@@ -91,16 +97,14 @@
 
 TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
   ConstraintContext Ctx;
-  auto True = Ctx.atom();
-  auto False = Ctx.atom();
-  auto V2 = Ctx.atom();
-  auto V3 = Ctx.atom();
+  auto X = Ctx.atom();
+  auto Y = Ctx.atom();
   Formula::AtomNames Names;
-  Names[True->getAtom()] = "true";
-  Names[False->getAtom()] = "false";
-  auto B = Ctx.disj(Ctx.conj(False, V2), Ctx.disj(True, V3));
+  Names[X->getAtom()] = "X";
+  Names[Y->getAtom()] = "Y";
+  auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom()));
 
-  auto Expected = R"(((false & V2) | (true | V3)))";
+  auto Expected = R"(((Y & V2) | (X | V3)))";
   std::string Actual;
   llvm::raw_string_ostream OS(Actual);
   B->print(OS, &Names);
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -482,6 +482,11 @@
     return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
   }
 
+  // Returns a reference to a literal boolean value.
+  const Formula *literal(bool B) {
+    return &Formula::create(A, Formula::Literal, {}, B);
+  }
+
   // Creates a boolean conjunction.
   const Formula *conj(const Formula *LHS, const Formula *RHS) {
     return make(Formula::And, {LHS, RHS});
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
@@ -3202,14 +3202,14 @@
         ASSERT_THAT(FooDecl, NotNull());
 
         const auto *FooVal =
-            dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
         ASSERT_THAT(FooVal, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
         const auto *BarVal =
-            dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*BarDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
         ASSERT_THAT(BarVal, NotNull());
 
         EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true));
@@ -3387,7 +3387,7 @@
         ASSERT_THAT(FooDecl, NotNull());
 
         const auto *FooVal =
-            dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
         ASSERT_THAT(FooVal, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");