[dataflow] Remove deprecated BoolValue flow condition accessors

[sammccall]

Summary

Use the Formula versions instead, now.

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

public:
   /// The FC is necessary but not sufficient for this point to be reachable.
   /// In particular, where the FC token appears in flow conditions of successor
   /// environments, it means "point X may have been reached", not
   /// "point X was reached".
   Atom getFlowConditionToken() const { return FlowConditionToken; }
 
   /// Record a fact that must be true if this point in the program is reached.
   void addToFlowCondition(const Formula &);
-  /// Deprecated: Use Formula version instead.
-  void addToFlowCondition(BoolValue &Val);
 
   /// Returns true if the formula is always true when this point is reached.
   /// Returns false if the formula may be false, or if the flow condition isn't
   /// sufficiently precise to prove that it is true.
   bool flowConditionImplies(const Formula &) const;
-  /// Deprecated: Use Formula version instead.
-  bool flowConditionImplies(BoolValue &Val) const;
 
   /// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
   /// returns null.
   const DeclContext *getDeclCtx() const { return CallStack.back(); }
 
   /// Returns the function currently being analyzed, or null if the code being
   /// analyzed isn't part of a function.
   const FunctionDecl *getCurrentFunc() const {

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

 const StorageLocation &Environment::skip(const StorageLocation &Loc,
                                          SkipPast SP) const {
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
 void Environment::addToFlowCondition(const Formula &Val) {
   DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
 }
-void Environment::addToFlowCondition(BoolValue &Val) {
-  addToFlowCondition(Val.formula());
-}
 
 bool Environment::flowConditionImplies(const Formula &Val) const {
   return DACtx->flowConditionImplies(FlowConditionToken, Val);
 }
-bool Environment::flowConditionImplies(BoolValue &Val) const {
-  return flowConditionImplies(Val.formula());
-}
 
 void Environment::dump(raw_ostream &OS) const {
   // FIXME: add printing for remaining fields and allow caller to decide what
   // fields are printed.
   OS << "DeclToLoc:\n";
   for (auto [D, L] : DeclToLoc)
     OS << "  [" << D->getNameAsString() << ", " << L << "]\n";
 

clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp

bool ChromiumCheckModel::transfer(const CFGElement &Element, Environment &Env) {
   auto CS = Element.getAs<CFGStmt>();
   if (!CS)
     return false;
   auto Stmt = CS->getStmt();
   if (const auto *Call = dyn_cast<CallExpr>(Stmt)) {
     if (const auto *M = dyn_cast<CXXMethodDecl>(Call->getDirectCallee())) {
       if (isCheckLikeMethod(CheckDecls, *M)) {
         // Mark this branch as unreachable.
-        Env.addToFlowCondition(Env.getBoolLiteralValue(false));
+        Env.addToFlowCondition(Env.arena().makeLiteral(false));
         return true;
       }
     }
   }
   return false;
 }
 
 } // namespace dataflow
 } // namespace clang

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/Stmt.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/ASTMatchers/ASTMatchersMacros.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/NoopLattice.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Basic/SourceLocation.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/ErrorHandling.h"
 #include <cassert>

 template <typename L, typename R>
 auto isComparisonOperatorCall(L lhs_arg_matcher, R rhs_arg_matcher) {
   return cxxOperatorCallExpr(
       anyOf(hasOverloadedOperatorName("=="), hasOverloadedOperatorName("!=")),
       argumentCountIs(2), hasArgument(0, lhs_arg_matcher),
       hasArgument(1, rhs_arg_matcher));
 }
 
-/// Ensures that `Expr` is mapped to a `BoolValue` and returns it.
-BoolValue &forceBoolValue(Environment &Env, const Expr &Expr) {
+/// Ensures that `Expr` is mapped to a `BoolValue` and returns its formula.
+const Formula &forceBoolValue(Environment &Env, const Expr &Expr) {
   auto *Value = cast_or_null<BoolValue>(Env.getValue(Expr, SkipPast::None));
   if (Value != nullptr)
-    return *Value;
+    return Value->formula();
 
   auto &Loc = Env.createStorageLocation(Expr);
   Value = &Env.makeAtomicBoolValue();
   Env.setValue(Loc, *Value);
   Env.setStorageLocation(Expr, Loc);
-  return *Value;
+  return Value->formula();
 }
 
 /// Sets `HasValueVal` as the symbolic value that represents the "has_value"
 /// property of the optional value `OptionalVal`.
 void setHasValue(Value &OptionalVal, BoolValue &HasValueVal) {
   OptionalVal.setProperty("has_value", HasValueVal);
 }
 

 }
 
 /// Returns true if and only if `OptionalVal` is initialized and known to be
 /// empty in `Env`.
 bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
   auto *HasValueVal =
       cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
   return HasValueVal != nullptr &&
-         Env.flowConditionImplies(Env.makeNot(*HasValueVal));
+         Env.flowConditionImplies(Env.arena().makeNot(HasValueVal->formula()));
 }
 
 /// Returns true if and only if `OptionalVal` is initialized and known to be
 /// non-empty in `Env`.
 bool isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) {
   auto *HasValueVal =
       cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
-  return HasValueVal != nullptr && Env.flowConditionImplies(*HasValueVal);
+  return HasValueVal != nullptr &&
+         Env.flowConditionImplies(HasValueVal->formula());
 }
 
 Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) {
   Value *Val = Env.getValue(E, SkipPast::Reference);
   if (auto *PointerVal = dyn_cast_or_null<PointerValue>(Val))
     return Env.getValue(PointerVal->getPointeeLoc());
   return Val;
 }
if (auto *HasValueVal = getHasValue(
     auto &CallExprLoc = State.Env.createStorageLocation(*CallExpr);
     State.Env.setValue(CallExprLoc, *HasValueVal);
     State.Env.setStorageLocation(*CallExpr, CallExprLoc);
   }
 }
 
 /// `ModelPred` builds a logical formula relating the predicate in
 /// `ValueOrPredExpr` to the optional's `has_value` property.
-void transferValueOrImpl(const clang::Expr *ValueOrPredExpr,
-                         const MatchFinder::MatchResult &Result,
-                         LatticeTransferState &State,
-                         BoolValue &(*ModelPred)(Environment &Env,
-                                                 BoolValue &ExprVal,
-                                                 BoolValue &HasValueVal)) {
+void transferValueOrImpl(
+    const clang::Expr *ValueOrPredExpr, const MatchFinder::MatchResult &Result,
+    const Formula &(*ModelPred)(Environment &Env, const Formula &ExprVal,
+                                const Formula &HasValueVal)) {
   auto &Env = State.Env;
 
   const auto *ObjectArgumentExpr =
       Result.Nodes.getNodeAs<clang::CXXMemberCallExpr>(ValueOrCallID)
           ->getImplicitObjectArgument();
 
   auto *HasValueVal = getHasValue(
       State.Env, getValueBehindPossiblePointer(*ObjectArgumentExpr, State.Env));
   if (HasValueVal == nullptr)
     return;
 
-  Env.addToFlowCondition(
-      ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr), *HasValueVal));
+  Env.addToFlowCondition(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
+                                   HasValueVal->formula()));
 }
 
 void transferValueOrStringEmptyCall(const clang::Expr *ComparisonExpr,
                                     const MatchFinder::MatchResult &Result,
                                     LatticeTransferState &State) {
   return transferValueOrImpl(ComparisonExpr, Result, State,
-                             [](Environment &Env, BoolValue &ExprVal,
-                                BoolValue &HasValueVal) -> BoolValue & {
+                             [](Environment &Env, const Formula &ExprVal,
+                                const Formula &HasValueVal) -> const Formula & {
+                               auto &A = Env.arena();
                                // If the result is *not* empty, then we know the
                                // optional must have been holding a value. If
                                // `ExprVal` is true, though, we don't learn
                                // anything definite about `has_value`, so we
                                // don't add any corresponding implications to
                                // the flow condition.
-                               return Env.makeImplication(Env.makeNot(ExprVal),
-                                                          HasValueVal);
+                               return A.makeImplies(A.makeNot(ExprVal),
                              });
 }
 
 void transferValueOrNotEqX(const Expr *ComparisonExpr,
                            const MatchFinder::MatchResult &Result,
                            LatticeTransferState &State) {
   transferValueOrImpl(ComparisonExpr, Result, State,
-                      [](Environment &Env, BoolValue &ExprVal,
-                         BoolValue &HasValueVal) -> BoolValue & {
+                      [](Environment &Env, const Formula &ExprVal,
+                         const Formula &HasValueVal) -> const Formula & {
+                        auto &A = Env.arena();
                         // We know that if `(opt.value_or(X) != X)` then
                         // `opt.hasValue()`, even without knowing further
                         // details about the contents of `opt`.
-                        return Env.makeImplication(ExprVal, HasValueVal);
+                        return A.makeImplies(ExprVal, HasValueVal);
                       });
 }
 
 void transferCallReturningOptional(const CallExpr *E,
                                    const MatchFinder::MatchResult &Result,
                                    LatticeTransferState &State) {
   if (State.Env.getStorageLocation(*E, SkipPast::None) != nullptr)
     return;
void transferStdForwardCall(const CallExpr *E, const MatchFinder::MatchResult &,
 
   // Create a new storage location
   LocRet = &State.Env.createStorageLocation(*E);
   State.Env.setStorageLocation(*E, *LocRet);
 
   State.Env.setValue(*LocRet, *ValArg);
 }
 
-BoolValue &evaluateEquality(Environment &Env, BoolValue &EqVal, BoolValue &LHS,
-                            BoolValue &RHS) {
+const Formula &evaluateEquality(Arena &A, const Formula &EqVal,
+                                const Formula &LHS, const Formula &RHS) {
   // Logically, an optional<T> object is composed of two values - a `has_value`
   // bit and a value of type T. Equality of optional objects compares both
   // values. Therefore, merely comparing the `has_value` bits isn't sufficient:
   // when two optional objects are engaged, the equality of their respective
   // values of type T matters. Since we only track the `has_value` bits, we
   // can't make any conclusions about equality when we know that two optional
   // objects are engaged.
   //
   // We express this as two facts about the equality:
   // a) EqVal => (LHS & RHS) v (!RHS & !LHS)
   //    If they are equal, then either both are set or both are unset.
   // b) (!LHS & !RHS) => EqVal
   //    If neither is set, then they are equal.
   // We rewrite b) as !EqVal => (LHS v RHS), for a more compact formula.
-  return Env.makeAnd(
-      Env.makeImplication(
-          EqVal, Env.makeOr(Env.makeAnd(LHS, RHS),
-                            Env.makeAnd(Env.makeNot(LHS), Env.makeNot(RHS)))),
-      Env.makeImplication(Env.makeNot(EqVal), Env.makeOr(LHS, RHS)));
+  return A.makeAnd(
+      A.makeImplies(EqVal, A.makeOr(A.makeAnd(LHS, RHS),
+                                    A.makeAnd(A.makeNot(LHS), A.makeNot(RHS)))),
+      A.makeImplies(A.makeNot(EqVal), A.makeOr(LHS, RHS)));
 }
 
 void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr,
                                     const MatchFinder::MatchResult &,
                                     LatticeTransferState &State) {
   Environment &Env = State.Env;
+  auto &A = Env.arena();
   auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
   if (auto *LHasVal = getHasValue(
           Env, Env.getValue(*CmpExpr->getArg(0), SkipPast::Reference)))
     if (auto *RHasVal = getHasValue(
             Env, Env.getValue(*CmpExpr->getArg(1), SkipPast::Reference))) {
       if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
-        CmpValue = &State.Env.makeNot(*CmpValue);
-      Env.addToFlowCondition(
-          evaluateEquality(Env, *CmpValue, *LHasVal, *RHasVal));
+        CmpValue = &A.makeNot(*CmpValue);
+      Env.addToFlowCondition(evaluateEquality(A, *CmpValue, LHasVal->formula(),
+                                              RHasVal->formula()));
     }
 }
 
 void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr,
                                  const clang::Expr *E, Environment &Env) {
+  auto &A = Env.arena();
   auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
   if (auto *HasVal = getHasValue(Env, Env.getValue(*E, SkipPast::Reference))) {
     if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
-      CmpValue = &Env.makeNot(*CmpValue);
-    Env.addToFlowCondition(evaluateEquality(Env, *CmpValue, *HasVal,
-                                            Env.getBoolLiteralValue(true)));
+      CmpValue = &A.makeNot(*CmpValue);
+    Env.addToFlowCondition(
+        evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));
   }
 }
 
 std::optional<StatementMatcher>
 ignorableOptional(const UncheckedOptionalAccessModelOptions &Options) {
   if (Options.IgnoreSmartPointerDereference) {
     auto SmartPtrUse = expr(ignoringParenImpCasts(cxxOperatorCallExpr(
         anyOf(hasOverloadedOperatorName("->"), hasOverloadedOperatorName("*")),
return CFGMatchSwitchBuilder<LatticeTransferState>()
       .Build();
 }
 
 std::vector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
                                                const Environment &Env) {
   if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) {
     auto *Prop = OptionalVal->getProperty("has_value");
     if (auto *HasValueVal = cast_or_null<BoolValue>(Prop)) {
-      if (Env.flowConditionImplies(*HasValueVal))
+      if (Env.flowConditionImplies(HasValueVal->formula()))
         return {};
     }
   }
 
   // Record that this unwrap is *not* provably safe.
   // FIXME: include either the name of the optional (if applicable) or a source
   // range of the access for easier interpretation of the result.
   return {ObjectExpr->getBeginLoc()};
bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
   if (!isOptionalType(Type))
     return true;
   // FIXME: uses same approach as join for `BoolValues`. Requires non-const
   // values, though, so will require updating the interface.
   auto &HasValueVal = MergedEnv.makeAtomicBoolValue();
   bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
   bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
   if (MustNonEmpty1 && MustNonEmpty2)
-    MergedEnv.addToFlowCondition(HasValueVal);
+    MergedEnv.addToFlowCondition(HasValueVal.formula());
   else if (
       // Only make the costly calls to `isEmptyOptional` if we got "unknown"
       // (false) for both calls to `isNonEmptyOptional`.
       !MustNonEmpty1 && !MustNonEmpty2 && isEmptyOptional(Val1, Env1) &&
       isEmptyOptional(Val2, Env2))
-    MergedEnv.addToFlowCondition(MergedEnv.makeNot(HasValueVal));
+    MergedEnv.addToFlowCondition(
+        MergedEnv.arena().makeNot(HasValueVal.formula()));
   setHasValue(MergedVal, HasValueVal);
   return true;
 }
 
 Value *UncheckedOptionalAccessModel::widen(QualType Type, Value &Prev,
                                            const Environment &PrevEnv,
                                            Value &Current,
                                            Environment &CurrentEnv) {

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

TerminatorVisitorRetTy extendFlowCondition(const Expr &Cond) {
     bool ConditionValue = true;
     // The condition must be inverted for the successor that encompasses the
     // "else" branch, if such exists.
     if (BlockSuccIdx == 1) {
       Val = &Env.makeNot(*Val);
       ConditionValue = false;
     }
 
-    Env.addToFlowCondition(*Val);
+    Env.addToFlowCondition(Val->formula());
     return {&Cond, ConditionValue};
   }
 
   const StmtToEnvMap &StmtToEnv;
   Environment &Env;
   int BlockSuccIdx;
 };
 

clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp

auto Expectations =
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
 
-        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+        EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula()));
       };
 
   std::string Code = R"(
     #include "check.h"
 
     void target(bool Foo) {
       $check(Foo);
       bool X = true;
auto Expectations =
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
 
-        EXPECT_FALSE(Env.flowConditionImplies(*FooVal));
+        EXPECT_FALSE(Env.flowConditionImplies(FooVal->formula()));
       };
 
   std::string Code = R"(
     #include "othercheck.h"
 
     void target(bool Foo) {
       if (!Foo) {
         (void)other::logging::CheckError::Check(__FILE__, __LINE__, "Foo");

clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp

 #include "gtest/gtest.h"
 #include <memory>
 
 namespace {
 
 using namespace clang;
 using namespace dataflow;
 using ::clang::dataflow::test::getFieldValue;
-using ::testing::ElementsAre;
 using ::testing::NotNull;
-using ::testing::Pair;
 
 class EnvironmentTest : public ::testing::Test {
 protected:
   EnvironmentTest() : DAContext(std::make_unique<WatchedLiteralsSolver>()) {}
 
   DataflowAnalysisContext DAContext;
 };
 
 TEST_F(EnvironmentTest, FlowCondition) {
   Environment Env(DAContext);
+  auto &A = Env.arena();
 
-  EXPECT_TRUE(Env.flowConditionImplies(Env.getBoolLiteralValue(true)));
-  EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
+  EXPECT_TRUE(Env.flowConditionImplies(A.makeLiteral(true)));
+  EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false)));
 
-  auto &X = Env.makeAtomicBoolValue();
+  auto &X = A.makeAtomRef(A.makeAtom());
   EXPECT_FALSE(Env.flowConditionImplies(X));
 
   Env.addToFlowCondition(X);
   EXPECT_TRUE(Env.flowConditionImplies(X));
 
-  auto &NotX = Env.makeNot(X);
+  auto &NotX = A.makeNot(X);
   EXPECT_FALSE(Env.flowConditionImplies(NotX));
 }
 
 TEST_F(EnvironmentTest, CreateValueRecursiveType) {
   using namespace ast_matchers;
 
   std::string Code = R"cc(
     struct Recursive {

clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp

if (OperandProps.Neg == nullptr)
     return {nullptr, {}, {}};
   // Properties for the operator expr itself.
   SignProperties UnaryOpProps = initUnknown(*UnaryOpValue, State.Env);
   return {UnaryOpValue, UnaryOpProps, OperandProps};
 }
 
 void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
                     LatticeTransferState &State) {
-  BoolValue *Comp = cast_or_null<BoolValue>(State.Env.getValueStrict(*BO));
-  if (!Comp) {
-    Comp = &State.Env.makeAtomicBoolValue();
-    State.Env.setValueStrict(*BO, *Comp);
+  auto &A = State.Env.arena();
+  const Formula *Comp;
+  if (BoolValue *V = cast_or_null<BoolValue>(State.Env.getValueStrict(*BO))) {
+    Comp = &V->formula();
+  } else {
+    Comp = &A.makeAtomRef(A.makeAtom());
+    State.Env.setValueStrict(*BO, A.makeBoolValue(*Comp));
   }
 
   // FIXME Use this as well:
   // auto *NegatedComp = &State.Env.makeNot(*Comp);
 
   auto *LHS = State.Env.getValueStrict(*BO->getLHS());
   auto *RHS = State.Env.getValueStrict(*BO->getRHS());
 
   if (!LHS || !RHS)
     return;
 
   SignProperties LHSProps = getSignProperties(*LHS, State.Env);
   SignProperties RHSProps = getSignProperties(*RHS, State.Env);
   if (LHSProps.Neg == nullptr || RHSProps.Neg == nullptr)
     return;
 
   switch (BO->getOpcode()) {
   case BO_GT:
     // pos > pos
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Pos, *LHSProps.Pos)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
+                                           LHSProps.Pos->formula())));
     // pos > zero
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Zero, *LHSProps.Pos)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
+                                           LHSProps.Pos->formula())));
     break;
   case BO_LT:
     // neg < neg
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Neg, *LHSProps.Neg)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
+                                           LHSProps.Neg->formula())));
     // neg < zero
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Zero, *LHSProps.Neg)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
+                                           LHSProps.Neg->formula())));
     break;
   case BO_GE:
     // pos >= pos
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Pos, *LHSProps.Pos)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
+                                           LHSProps.Pos->formula())));
     break;
   case BO_LE:
     // neg <= neg
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Neg, *LHSProps.Neg)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
+                                           LHSProps.Neg->formula())));
     break;
   case BO_EQ:
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Neg, *LHSProps.Neg)));
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Zero, *LHSProps.Zero)));
-    State.Env.addToFlowCondition(State.Env.makeImplication(
-        *Comp, State.Env.makeImplication(*RHSProps.Pos, *LHSProps.Pos)));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
+                                           LHSProps.Neg->formula())));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
+                                           LHSProps.Zero->formula())));
+    State.Env.addToFlowCondition(
+        A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
+                                           LHSProps.Pos->formula())));
     break;
   case BO_NE: // Noop.
     break;
   default:
     llvm_unreachable("not implemented");
   }
 }
 
 void transferUnaryMinus(const UnaryOperator *UO,
                         const MatchFinder::MatchResult &M,
                         LatticeTransferState &State) {
+  auto &A = State.Env.arena();
   auto [UnaryOpValue, UnaryOpProps, OperandProps] =
       getValueAndSignProperties(UO, M, State);
   if (!UnaryOpValue)
     return;
 
   // a is pos ==> -a is neg
   State.Env.addToFlowCondition(
-      State.Env.makeImplication(*OperandProps.Pos, *UnaryOpProps.Neg));
+      A.makeImplies(OperandProps.Pos->formula(), UnaryOpProps.Neg->formula()));
   // a is neg ==> -a is pos
   State.Env.addToFlowCondition(
-      State.Env.makeImplication(*OperandProps.Neg, *UnaryOpProps.Pos));
+      A.makeImplies(OperandProps.Neg->formula(), UnaryOpProps.Pos->formula()));
   // a is zero ==> -a is zero
-  State.Env.addToFlowCondition(
-      State.Env.makeImplication(*OperandProps.Zero, *UnaryOpProps.Zero));
+  State.Env.addToFlowCondition(A.makeImplies(OperandProps.Zero->formula(),
+                                             UnaryOpProps.Zero->formula()));
 }
 
 void transferUnaryNot(const UnaryOperator *UO,
                       const MatchFinder::MatchResult &M,
                       LatticeTransferState &State) {
+  auto &A = State.Env.arena();
   auto [UnaryOpValue, UnaryOpProps, OperandProps] =
       getValueAndSignProperties(UO, M, State);
   if (!UnaryOpValue)
     return;
 
   // a is neg or pos ==> !a is zero
-  State.Env.addToFlowCondition(State.Env.makeImplication(
-      State.Env.makeOr(*OperandProps.Pos, *OperandProps.Neg),
-      *UnaryOpProps.Zero));
+  State.Env.addToFlowCondition(A.makeImplies(
+      A.makeOr(OperandProps.Pos->formula(), OperandProps.Neg->formula()),
+      UnaryOpProps.Zero->formula()));
 
   // FIXME Handle this logic universally, not just for unary not. But Where to
   // put the generic handler, transferExpr maybe?
   if (auto *UOBoolVal = dyn_cast<BoolValue>(UnaryOpValue)) {
     // !a <==> a is zero
     State.Env.addToFlowCondition(
-        State.Env.makeIff(*UOBoolVal, *OperandProps.Zero));
+        A.makeEquals(UOBoolVal->formula(), OperandProps.Zero->formula()));
     // !a <==> !a is not zero
-    State.Env.addToFlowCondition(
-        State.Env.makeIff(*UOBoolVal, State.Env.makeNot(*UnaryOpProps.Zero)));
+    State.Env.addToFlowCondition(A.makeEquals(
+        UOBoolVal->formula(), A.makeNot(UnaryOpProps.Zero->formula())));
   }
 }
 
 // Returns the `Value` associated with `E` (which may be either a prvalue or
 // glvalue). Creates a `Value` or `StorageLocation` as needed if `E` does not
 // have either of these associated with it yet.
 //
 // If this functionality turns out to be needed in more cases, this function

 // Copied from crubit.
 BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
                            BoolValue &Bool2, const Environment &Env2,
                            Environment &MergedEnv) {
   if (&Bool1 == &Bool2) {
     return Bool1;
   }
 
+  auto &B1 = Bool1.formula();
+  auto &B2 = Bool2.formula();
+
+  auto &A = MergedEnv.arena();
   auto &MergedBool = MergedEnv.makeAtomicBoolValue();
 
   // If `Bool1` and `Bool2` is constrained to the same true / false value,
   // `MergedBool` can be constrained similarly without needing to consider the
   // path taken - this simplifies the flow condition tracked in `MergedEnv`.
   // Otherwise, information about which path was taken is used to associate
   // `MergedBool` with `Bool1` and `Bool2`.
-  if (Env1.flowConditionImplies(Bool1) && Env2.flowConditionImplies(Bool2)) {
-    MergedEnv.addToFlowCondition(MergedBool);
-  } else if (Env1.flowConditionImplies(Env1.makeNot(Bool1)) &&
-             Env2.flowConditionImplies(Env2.makeNot(Bool2))) {
-    MergedEnv.addToFlowCondition(MergedEnv.makeNot(MergedBool));
+  if (Env1.flowConditionImplies(B1) && Env2.flowConditionImplies(B2)) {
+    MergedEnv.addToFlowCondition(MergedBool.formula());
+  } else if (Env1.flowConditionImplies(A.makeNot(B1)) &&
+             Env2.flowConditionImplies(A.makeNot(B2))) {
+    MergedEnv.addToFlowCondition(A.makeNot(MergedBool.formula()));
   }
   return MergedBool;
 }
 
 bool SignPropagationAnalysis::merge(QualType Type, const Value &Val1,
                                     const Environment &Env1, const Value &Val2,
                                     const Environment &Env2, Value &MergedVal,
                                     Environment &MergedEnv) {

 template <typename Node>
 testing::AssertionResult isPropertyImplied(const Environment &Env,
                                            ASTContext &ASTCtx, const Node *N,
                                            StringRef Property, bool Implies) {
   auto [Result, Prop] = getProperty(Env, ASTCtx, N, Property);
   if (!Prop)
     return Result;
   auto *BVProp = cast<BoolValue>(Prop);
-  if (Env.flowConditionImplies(*BVProp) != Implies)
+  if (Env.flowConditionImplies(BVProp->formula()) != Implies)
     return testing::AssertionFailure()
            << Property << " is " << (Implies ? "not" : "") << " implied"
            << ", but should " << (Implies ? "" : "not ") << "be";
   return testing::AssertionSuccess();
 }
 
 template <typename Node>
 testing::AssertionResult isNegative(const Node *N, ASTContext &ASTCtx,

clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

void runDataflow(
     LangStandard::Kind Std = LangStandard::lang_cxx17,
     bool ApplyBuiltinTransfer = true, llvm::StringRef TargetFun = "target") {
   runDataflow(Code, std::move(VerifyResults),
               {ApplyBuiltinTransfer ? BuiltinOptions{}
                                     : std::optional<BuiltinOptions>()},
               Std, TargetFun);
 }
 
+const Formula &getFormula(const ValueDecl &D, const Environment &Env) {
+  return cast<BoolValue>(Env.getValue(D))->formula();
+}
+
 TEST(TransferTest, IntVarDeclNotTrackedWhenTransferDisabled) {
   std::string Code = R"(
     void target() {
       int Foo;
       // [[p]]
     }
   )";
   runDataflow(
runDataflow(
         const Environment &EnvThen =
             getEnvironmentAtAnnotation(Results, "p-then");
         const Environment &EnvElse =
             getEnvironmentAtAnnotation(Results, "p-else");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarValThen = *cast<BoolValue>(EnvThen.getValue(*BarDecl));
+        auto &BarValThen = getFormula(*BarDecl, EnvThen);
         EXPECT_TRUE(EnvThen.flowConditionImplies(BarValThen));
 
-        auto &BarValElse = *cast<BoolValue>(EnvElse.getValue(*BarDecl));
+        auto &BarValElse = getFormula(*BarDecl, EnvElse);
         EXPECT_FALSE(EnvElse.flowConditionImplies(BarValElse));
       });
 }
 
 TEST(TransferTest, BooleanInequality) {
   std::string Code = R"(
     void target(bool Bar) {
       bool Foo = true;
runDataflow(
         const Environment &EnvThen =
             getEnvironmentAtAnnotation(Results, "p-then");
         const Environment &EnvElse =
             getEnvironmentAtAnnotation(Results, "p-else");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarValThen = *cast<BoolValue>(EnvThen.getValue(*BarDecl));
+        auto &BarValThen = getFormula(*BarDecl, EnvThen);
         EXPECT_FALSE(EnvThen.flowConditionImplies(BarValThen));
 
-        auto &BarValElse = *cast<BoolValue>(EnvElse.getValue(*BarDecl));
+        auto &BarValElse = getFormula(*BarDecl, EnvElse);
         EXPECT_TRUE(EnvElse.flowConditionImplies(BarValElse));
       });
 }
 
 TEST(TransferTest, IntegerLiteralEquality) {
   std::string Code = R"(
     void target() {
       bool equal = (42 == 42);
       // [[p]]
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
-        auto &Equal = getValueForDecl<BoolValue>(ASTCtx, Env, "equal");
+        auto &Equal =
+            getValueForDecl<BoolValue>(ASTCtx, Env, "equal").formula();
         EXPECT_TRUE(Env.flowConditionImplies(Equal));
       });
 }
 
 TEST(TransferTest, CorrelatedBranches) {
   std::string Code = R"(
     void target(bool B, bool C) {
       if (B) {
runDataflow(
 
         const ValueDecl *CDecl = findValueDecl(ASTCtx, "C");
         ASSERT_THAT(CDecl, NotNull());
 
         {
           const Environment &Env = getEnvironmentAtAnnotation(Results, "p0");
           const ValueDecl *BDecl = findValueDecl(ASTCtx, "B");
           ASSERT_THAT(BDecl, NotNull());
-          auto &BVal = *cast<BoolValue>(Env.getValue(*BDecl));
+          auto &BVal = getFormula(*BDecl, Env);
 
-          EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BVal)));
+          EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BVal)));
         }
 
         {
           const Environment &Env = getEnvironmentAtAnnotation(Results, "p1");
-          auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl));
+          auto &CVal = getFormula(*CDecl, Env);
           EXPECT_TRUE(Env.flowConditionImplies(CVal));
         }
 
         {
           const Environment &Env = getEnvironmentAtAnnotation(Results, "p2");
-          auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl));
+          auto &CVal = getFormula(*CDecl, Env);
           EXPECT_TRUE(Env.flowConditionImplies(CVal));
         }
       });
 }
 
 TEST(TransferTest, LoopWithAssignmentConverges) {
   std::string Code = R"(
     bool foo();
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
+        auto &BarVal = getFormula(*BarDecl, Env);
+        EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
       });
 }
 
 TEST(TransferTest, LoopWithStagedAssignments) {
   std::string Code = R"(
     bool foo();
 
     void target() {
runDataflow(
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
         const ValueDecl *ErrDecl = findValueDecl(ASTCtx, "Err");
         ASSERT_THAT(ErrDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
-        auto &ErrVal = *cast<BoolValue>(Env.getValue(*ErrDecl));
+        auto &BarVal = getFormula(*BarDecl, Env);
+        auto &ErrVal = getFormula(*ErrDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(BarVal));
         // An unsound analysis, for example only evaluating the loop once, can
         // conclude that `Err` is false. So, we test that this conclusion is not
         // reached.
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(ErrVal)));
+        EXPECT_FALSE(
+            Env.flowConditionImplies(Env.arena().makeNot(ErrVal)));
       });
 }
 
 TEST(TransferTest, LoopWithReferenceAssignmentConverges) {
   std::string Code = R"(
     bool &foo();
 
     void target() {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
+        auto &BarVal = getFormula(*BarDecl, Env);
+        EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
       });
 }
 
 TEST(TransferTest, LoopWithStructReferenceAssignmentConverges) {
   std::string Code = R"(
     struct Lookup {
       int x;
     };
runDataflow(
         const Environment &ThenEnv =
             getEnvironmentAtAnnotation(Results, "if_then");
         const Environment &ElseEnv =
             getEnvironmentAtAnnotation(Results, "if_else");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        BoolValue &ThenFooVal = *cast<BoolValue>(ThenEnv.getValue(*FooDecl));
+        auto &ThenFooVal= getFormula(*FooDecl, ThenEnv);
         EXPECT_TRUE(ThenEnv.flowConditionImplies(ThenFooVal));
 
-        BoolValue &ElseFooVal = *cast<BoolValue>(ElseEnv.getValue(*FooDecl));
-        EXPECT_TRUE(ElseEnv.flowConditionImplies(ElseEnv.makeNot(ElseFooVal)));
+        auto &ElseFooVal = getFormula(*FooDecl, ElseEnv);
+        EXPECT_TRUE(
+            ElseEnv.flowConditionImplies(ElseEnv.arena().makeNot(ElseFooVal)));
       });
 }
 
 TEST(TransferTest, WhileStmtBranchExtendsFlowCondition) {
   std::string Code = R"(
     void target(bool Foo) {
       while (Foo) {
         (void)0;
runDataflow(
         const Environment &LoopBodyEnv =
             getEnvironmentAtAnnotation(Results, "loop_body");
         const Environment &AfterLoopEnv =
             getEnvironmentAtAnnotation(Results, "after_loop");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        BoolValue &LoopBodyFooVal =
-            *cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
+        auto &LoopBodyFooVal = getFormula(*FooDecl, LoopBodyEnv);
         EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
 
-        BoolValue &AfterLoopFooVal =
-            *cast<BoolValue>(AfterLoopEnv.getValue(*FooDecl));
+        auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
         EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
-            AfterLoopEnv.makeNot(AfterLoopFooVal)));
+            AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
       });
 }
 
 TEST(TransferTest, DoWhileStmtBranchExtendsFlowCondition) {
   std::string Code = R"(
     void target(bool Foo) {
       bool Bar = true;
       do {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(),
                     UnorderedElementsAre("loop_body", "after_loop"));
         const Environment &LoopBodyEnv =
             getEnvironmentAtAnnotation(Results, "loop_body");
         const Environment &AfterLoopEnv =
             getEnvironmentAtAnnotation(Results, "after_loop");
+        auto &A = AfterLoopEnv.arena();
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        BoolValue &LoopBodyFooVal =
-            *cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
-        BoolValue &LoopBodyBarVal =
-            *cast<BoolValue>(LoopBodyEnv.getValue(*BarDecl));
+        auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
+        auto &LoopBodyBarVal = getFormula(*BarDecl, LoopBodyEnv);
         EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(
-            LoopBodyEnv.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
+            A.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
 
-        BoolValue &AfterLoopFooVal =
-            *cast<BoolValue>(AfterLoopEnv.getValue(*FooDecl));
-        BoolValue &AfterLoopBarVal =
-            *cast<BoolValue>(AfterLoopEnv.getValue(*BarDecl));
-        EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
-            AfterLoopEnv.makeNot(AfterLoopFooVal)));
-        EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
-            AfterLoopEnv.makeNot(AfterLoopBarVal)));
+        auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
+        auto &AfterLoopBarVal = getFormula(*BarDecl, AfterLoopEnv);
+        EXPECT_TRUE(
+            AfterLoopEnv.flowConditionImplies(A.makeNot(AfterLoopFooVal)));
+        EXPECT_TRUE(
+            AfterLoopEnv.flowConditionImplies(A.makeNot(AfterLoopBarVal)));
       });
 }
 
 TEST(TransferTest, ForStmtBranchExtendsFlowCondition) {
   std::string Code = R"(
     void target(bool Foo) {
       for (; Foo;) {
         (void)0;
runDataflow(
         const Environment &LoopBodyEnv =
             getEnvironmentAtAnnotation(Results, "loop_body");
         const Environment &AfterLoopEnv =
             getEnvironmentAtAnnotation(Results, "after_loop");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        BoolValue &LoopBodyFooVal =
-            *cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
+        auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
         EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
 
-        BoolValue &AfterLoopFooVal =
-            *cast<BoolValue>(AfterLoopEnv.getValue(*FooDecl));
+        auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
         EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
-            AfterLoopEnv.makeNot(AfterLoopFooVal)));
+            AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
       });
 }
 
 TEST(TransferTest, ForStmtBranchWithoutConditionDoesNotExtendFlowCondition) {
   std::string Code = R"(
     void target(bool Foo) {
       for (;;) {
         (void)0;
         // [[loop_body]]
       }
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("loop_body"));
         const Environment &LoopBodyEnv =
             getEnvironmentAtAnnotation(Results, "loop_body");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        BoolValue &LoopBodyFooVal =
-            *cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
+        auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
         EXPECT_FALSE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
       });
 }
 
 TEST(TransferTest, ContextSensitiveOptionDisabled) {
   std::string Code = R"(
     bool GiveBool();
     void SetBool(bool &Var) { Var = true; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{/*.ContextSensitiveOpts=*/std::nullopt}});
 }
 
 TEST(TransferTest, ContextSensitiveReturnReference) {
   std::string Code = R"(
     class S {};
     S& target(bool b, S &s) {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/0}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetTrue) {
   std::string Code = R"(
     bool GiveBool();
     void SetBool(bool &Var) { Var = true; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetFalse) {
   std::string Code = R"(
     bool GiveBool();
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        auto &FooVal = getFormula(*FooDecl, Env);
+        EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetBothTrueAndFalse) {
   std::string Code = R"(
     bool GiveBool();
     void SetBool(bool &Var, bool Val) { Var = Val; }
 
     void target() {
       bool Foo = GiveBool();
       bool Bar = GiveBool();
       SetBool(Foo, true);
       SetBool(Bar, false);
       // [[p]]
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
+        auto &A = Env.arena();
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(A.makeNot(FooVal)));
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
+        auto &BarVal = getFormula(*BarDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(BarVal));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
+        EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(BarVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetTwoLayersDepthOne) {
   std::string Code = R"(
     bool GiveBool();
     void SetBool1(bool &Var) { Var = true; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/1}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetTwoLayersDepthTwo) {
   std::string Code = R"(
     bool GiveBool();
     void SetBool1(bool &Var) { Var = true; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetThreeLayersDepthTwo) {
   std::string Code = R"(
     bool GiveBool();
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetThreeLayersDepthThree) {
   std::string Code = R"(
     bool GiveBool();
     void SetBool1(bool &Var) { Var = true; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/3}}});
 }
 
 TEST(TransferTest, ContextSensitiveMutualRecursion) {
   std::string Code = R"(
     bool Pong(bool X, bool Y);
runDataflow(
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         // The analysis doesn't crash...
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         // ... but it also can't prove anything here.
         EXPECT_FALSE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/4}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetMultipleLines) {
   std::string Code = R"(
     void SetBools(bool &Var1, bool &Var2) {
       Var1 = true;
runDataflow(
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
+        auto &BarVal = getFormula(*BarDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(BarVal));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
+        EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveSetMultipleBlocks) {
   std::string Code = R"(
     void IfCond(bool Cond, bool &Then, bool &Else) {
       if (Cond) {
runDataflow(
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
         const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz");
         ASSERT_THAT(BazDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
+        auto &BarVal = getFormula(*BarDecl, Env);
         EXPECT_FALSE(Env.flowConditionImplies(BarVal));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
+        EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
 
-        auto &BazVal = *cast<BoolValue>(Env.getValue(*BazDecl));
+        auto &BazVal = getFormula(*BazDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(BazVal));
-        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(BazVal)));
+        EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(BazVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveReturnVoid) {
   std::string Code = R"(
     void Noop() { return; }
 
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveReturnFalse) {
   std::string Code = R"(
     bool GiveBool() { return false; }
 
     void target() {
       bool Foo = GiveBool();
       // [[p]]
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+        auto &FooVal = getFormula(*FooDecl, Env);
+        EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveReturnArg) {
   std::string Code = R"(
     bool GiveBool();
     bool GiveBack(bool Arg) { return Arg; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz");
         ASSERT_THAT(BazDecl, NotNull());
 
-        auto &BazVal = *cast<BoolValue>(Env.getValue(*BazDecl));
+        auto &BazVal = getFormula(*BazDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(BazVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveReturnInt) {
   std::string Code = R"(
     int identity(int x) { return x; }
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveMethodGetter) {
   std::string Code = R"(
     class MyClass {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveMethodSetter) {
   std::string Code = R"(
     class MyClass {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveMethodGetterAndSetter) {
   std::string Code = R"(
     class MyClass {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 
 TEST(TransferTest, ContextSensitiveMethodTwoLayersVoid) {
   std::string Code = R"(
runDataflow(
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         ;
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveMethodTwoLayersReturn) {
   std::string Code = R"(
     class MyClass {
runDataflow(
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         ;
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveConstructorBody) {
   std::string Code = R"(
     class MyClass {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveConstructorInitializer) {
   std::string Code = R"(
     class MyClass {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, ContextSensitiveConstructorDefault) {
   std::string Code = R"(
     class MyClass {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
+        auto &FooVal = getFormula(*FooDecl, Env);
         EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       },
       {BuiltinOptions{ContextSensitiveOptions{}}});
 }
 
 TEST(TransferTest, UnnamedBitfieldInitializer) {
   std::string Code = R"(
     struct B {};
bool target() {
       return b;
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
-        auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b");
+        auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b").formula();
         EXPECT_TRUE(Env.flowConditionImplies(B));
       });
 }
 
 // Repro for a crash that used to occur when we call a `noreturn` function
 // within one of the operands of a `&&` or `||` operator.
 TEST(TransferTest, NoReturnFunctionInsideShortCircuitedBooleanOp) {
   std::string Code = R"(
std::string Code = R"(
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
+        auto &A = Env.arena();
 
         // Check that [[p]] is reachable with a non-false flow condition.
-        EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
+        EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false)));
 
-        auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1");
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(B1)));
+        auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1").formula();
+        EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(B1)));
 
         auto &NoreturnOnRhsOfAnd =
-            getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd");
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(NoreturnOnRhsOfAnd)));
+            getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd").formula();
+        EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(NoreturnOnRhsOfAnd)));
 
-        auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2");
+        auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2").formula();
         EXPECT_TRUE(Env.flowConditionImplies(B2));
 
         auto &NoreturnOnRhsOfOr =
-            getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr");
+            getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr")
+                .formula();
         EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnRhsOfOr));
 
         auto &NoreturnOnLhsMakesAndUnreachable = getValueForDecl<BoolValue>(
-            ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable");
+            ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable").formula();
         EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesAndUnreachable));
 
         auto &NoreturnOnLhsMakesOrUnreachable = getValueForDecl<BoolValue>(
-            ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable");
+            ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable").formula();
         EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesOrUnreachable));
       });
 }
 
 TEST(TransferTest, NewExpressions) {
   std::string Code = R"(
     void target() {
       int *p = new int(42);
runDataflow(
             findIndirectFieldDecl(ASTCtx, "b");
 
         auto *S =
             cast<AggregateStorageLocation>(Env.getStorageLocation(*SDecl));
         auto &AnonStruct = cast<AggregateStorageLocation>(
             S->getChild(*cast<ValueDecl>(IndirectField->chain().front())));
 
         auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
-        ASSERT_TRUE(Env.flowConditionImplies(*B));
+        ASSERT_TRUE(Env.flowConditionImplies(B->formula()));
       });
 }
 
 TEST(TransferTest, AnonymousStructWithInitializer) {
   std::string Code = R"(
     struct target {
       target() {
         (void)0;
runDataflow(
             findIndirectFieldDecl(ASTCtx, "b");
 
         auto *ThisLoc =
             cast<AggregateStorageLocation>(Env.getThisPointeeStorageLocation());
         auto &AnonStruct = cast<AggregateStorageLocation>(ThisLoc->getChild(
             *cast<ValueDecl>(IndirectField->chain().front())));
 
         auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
-        ASSERT_TRUE(Env.flowConditionImplies(*B));
+        ASSERT_TRUE(Env.flowConditionImplies(B->formula()));
       });
 }
 
 TEST(TransferTest, AnonymousStructWithReferenceField) {
   std::string Code = R"(
     int global_i = 0;
     struct target {
       target() {

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

ComparisonResult compare(QualType Type, const Value &Val1,
     auto *IsSet2 = cast_or_null<BoolValue>(Val2.getProperty("is_set"));
     if (IsSet1 == nullptr)
       return IsSet2 == nullptr ? ComparisonResult::Same
                                : ComparisonResult::Different;
 
     if (IsSet2 == nullptr)
       return ComparisonResult::Different;
 
-    return Env1.flowConditionImplies(*IsSet1) ==
-                   Env2.flowConditionImplies(*IsSet2)
+    return Env1.flowConditionImplies(IsSet1->formula()) ==
+                   Env2.flowConditionImplies(IsSet2->formula())
                ? ComparisonResult::Same
                : ComparisonResult::Different;
   }
 
   // Always returns `true` to accept the `MergedVal`.
   bool merge(QualType Type, const Value &Val1, const Environment &Env1,
              const Value &Val2, const Environment &Env2, Value &MergedVal,
              Environment &MergedEnv) override {
     const auto *Decl = Type->getAsCXXRecordDecl();
     if (Decl == nullptr || Decl->getIdentifier() == nullptr ||
         Decl->getName() != "SpecialBool")
       return true;
 
     auto *IsSet1 = cast_or_null<BoolValue>(Val1.getProperty("is_set"));
     if (IsSet1 == nullptr)
       return true;
 
     auto *IsSet2 = cast_or_null<BoolValue>(Val2.getProperty("is_set"));
     if (IsSet2 == nullptr)
       return true;
 
     auto &IsSet = MergedEnv.makeAtomicBoolValue();
     MergedVal.setProperty("is_set", IsSet);
-    if (Env1.flowConditionImplies(*IsSet1) &&
-        Env2.flowConditionImplies(*IsSet2))
-      MergedEnv.addToFlowCondition(IsSet);
+    if (Env1.flowConditionImplies(IsSet1->formula()) &&
+        Env2.flowConditionImplies(IsSet2->formula()))
+      MergedEnv.addToFlowCondition(IsSet.formula());
 
     return true;
   }
 };
 
 class JoinFlowConditionsTest : public Test {
 protected:
   template <typename Matcher>
runDataflow(
         const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
         const Environment &Env3 = getEnvironmentAtAnnotation(Results, "p3");
         const Environment &Env4 = getEnvironmentAtAnnotation(Results, "p4");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
-        auto GetFooValue = [FooDecl](const Environment &Env) {
-          return cast<BoolValue>(Env.getValue(*FooDecl)->getProperty("is_set"));
+        auto GetFoo = [FooDecl](const Environment &Env) -> const Formula & {
+          return cast<BoolValue>(Env.getValue(*FooDecl)->getProperty("is_set"))
+              ->formula();
         };
 
-        EXPECT_FALSE(Env1.flowConditionImplies(*GetFooValue(Env1)));
-        EXPECT_TRUE(Env2.flowConditionImplies(*GetFooValue(Env2)));
-        EXPECT_TRUE(Env3.flowConditionImplies(*GetFooValue(Env3)));
-        EXPECT_TRUE(Env4.flowConditionImplies(*GetFooValue(Env4)));
+        EXPECT_FALSE(Env1.flowConditionImplies(GetFoo(Env1)));
+        EXPECT_TRUE(Env2.flowConditionImplies(GetFoo(Env2)));
+        EXPECT_TRUE(Env3.flowConditionImplies(GetFoo(Env3)));
+        EXPECT_TRUE(Env4.flowConditionImplies(GetFoo(Env4)));
       });
 }
 
 class OptionalIntAnalysis final
     : public DataflowAnalysis<OptionalIntAnalysis, NoopLattice> {
 public:
   explicit OptionalIntAnalysis(ASTContext &Context)
       : DataflowAnalysis<OptionalIntAnalysis, NoopLattice>(Context) {}
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
         const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-        auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
-        EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+        auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
+        EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
 
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-        auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
-        EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+        auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
+        EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
       });
 }
 
 TEST_F(FlowConditionTest, IfStmtSingleNegatedVar) {
   std::string Code = R"(
     void target(bool Foo) {
       if (!Foo) {
         (void)0;
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
         const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-        auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
-        EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+        auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
+        EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
 
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-        auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
-        EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
+        auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
+        EXPECT_TRUE(Env2.flowConditionImplies(FooVal2));
       });
 }
 
 TEST_F(FlowConditionTest, WhileStmt) {
   std::string Code = R"(
     void target(bool Foo) {
       while (Foo) {
         (void)0;
         /*[[p]]*/
       }
     }
   )";
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
-        auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
-        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+        auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula();
+        EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       });
 }
 
 TEST_F(FlowConditionTest, Conjunction) {
   std::string Code = R"(
     void target(bool Foo, bool Bar) {
       if (Foo && Bar) {
         (void)0;
runDataflow(Code, [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>>
     ASSERT_THAT(FooDecl, NotNull());
 
     const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
     ASSERT_THAT(BarDecl, NotNull());
 
     ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
     const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-    auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
-    auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
-    EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
-    EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
+    auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
+    auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
+    EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
+    EXPECT_TRUE(Env1.flowConditionImplies(BarVal1));
 
     const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-    auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
-    auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
-    EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
-    EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+    auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
+    auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
+    EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
+    EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
   });
 }
 
 TEST_F(FlowConditionTest, Disjunction) {
   std::string Code = R"(
     void target(bool Foo, bool Bar) {
       if (Foo || Bar) {
         (void)0;
runDataflow(Code, [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>>
     ASSERT_THAT(FooDecl, NotNull());
 
     const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
     ASSERT_THAT(BarDecl, NotNull());
 
     ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
     const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-    auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
-    auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
-    EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
-    EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
+    auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
+    auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
+    EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
+    EXPECT_FALSE(Env1.flowConditionImplies(BarVal1));
 
     const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-    auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
-    auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
-    EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
-    EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+    auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
+    auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
+    EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
+    EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
   });
 }
 
 TEST_F(FlowConditionTest, NegatedConjunction) {
   std::string Code = R"(
     void target(bool Foo, bool Bar) {
       if (!(Foo && Bar)) {
         (void)0;
runDataflow(Code, [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>>
     ASSERT_THAT(FooDecl, NotNull());
 
     const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
     ASSERT_THAT(BarDecl, NotNull());
 
     ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
     const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-    auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
-    auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
-    EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
-    EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
+    auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
+    auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
+    EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
+    EXPECT_FALSE(Env1.flowConditionImplies(BarVal1));
 
     const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-    auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
-    auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
-    EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
-    EXPECT_TRUE(Env2.flowConditionImplies(*BarVal2));
+    auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
+    auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
+    EXPECT_TRUE(Env2.flowConditionImplies(FooVal2));
+    EXPECT_TRUE(Env2.flowConditionImplies(BarVal2));
   });
 }
 
 TEST_F(FlowConditionTest, DeMorgan) {
   std::string Code = R"(
     void target(bool Foo, bool Bar) {
       if (!(!Foo || !Bar)) {
         (void)0;
runDataflow(Code, [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>>
     ASSERT_THAT(FooDecl, NotNull());
 
     const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
     ASSERT_THAT(BarDecl, NotNull());
 
     ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
     const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-    auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
-    auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
-    EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
-    EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
+    auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
+    auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
+    EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
+    EXPECT_TRUE(Env1.flowConditionImplies(BarVal1));
 
     const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-    auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
-    auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
-    EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
-    EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+    auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
+    auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
+    EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
+    EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
   });
 }
 
 TEST_F(FlowConditionTest, Join) {
   std::string Code = R"(
     void target(bool Foo, bool Bar) {
       if (Bar) {
         if (!Foo)
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
-        auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
-        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+        auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula();
+        EXPECT_TRUE(Env.flowConditionImplies(FooVal));
       });
 }
 
 // Verifies that flow conditions are properly constructed even when the
 // condition is not meaningfully interpreted.
 //
 // Note: currently, arbitrary function calls are uninterpreted, so the test
 // exercises this case. If and when we change that, this test will not add to
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
+        auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
 
         EXPECT_FALSE(Env.flowConditionImplies(BarVal));
       });
 }
 
 // Verifies that flow conditions are properly constructed even when the
 // condition is not meaningfully interpreted.
 //
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
+        auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
 
         EXPECT_FALSE(Env.flowConditionImplies(BarVal));
       });
 }
 
 // Verifies that flow conditions are properly constructed even when the
 // condition is not meaningfully interpreted. Adds to above by nesting the
 // interestnig case inside a normal branch. This protects against degenerate
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
-        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
+        auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
 
         EXPECT_FALSE(Env.flowConditionImplies(BarVal));
       });
 }
 
 TEST_F(FlowConditionTest, PointerToBoolImplicitCast) {
   std::string Code = R"(
     void target(int *Ptr) {
runDataflow(
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
-        auto &FooVal1 = *cast<BoolValue>(Env1.getValue(*FooDecl));
+        auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
         EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
 
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
-        auto &FooVal2 = *cast<BoolValue>(Env2.getValue(*FooDecl));
+        auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
         EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
       });
 }
 
 class TopAnalysis final : public DataflowAnalysis<TopAnalysis, NoopLattice> {
 public:
   explicit TopAnalysis(ASTContext &Context)
       : DataflowAnalysis<TopAnalysis, NoopLattice>(Context) {}
runDataflow(
         ASSERT_THAT(BarDecl, NotNull());
 
         auto *FooVal = dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
         ASSERT_THAT(FooVal, NotNull());
 
         auto *BarVal = dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
         ASSERT_THAT(BarVal, NotNull());
 
-        EXPECT_TRUE(Env.flowConditionImplies(Env.makeIff(*FooVal, *BarVal)));
+        EXPECT_TRUE(Env.flowConditionImplies(
+            Env.arena().makeEquals(FooVal->formula(), BarVal->formula())));
       });
 }
 
 TEST_F(TopTest, TopUnusedBeforeLoopHeadJoinsToTop) {
   std::string Code = R"(
     bool makeTop();
 
     void target(bool Cond, bool F) {