1 files changed, 8 insertions, 1 deletions
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 28a8595..e81048c 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -141,6 +141,8 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
 
 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());
 }
 
@@ -211,8 +213,13 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
   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);
+    Constraint->print(OS, &Names);
     OS << "\n";
   }
 }