[PATCH] D45517: [analyzer] False positive refutation with Z3

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:928
+  bool isModelFeasible() override {
+    return Solver.check() != Z3_L_FALSE;
+  }
----------------
george.karpenkov wrote:
> The semantics of this method is incorrect. It should return a tri-value somehow (e.g. `Optional<bool>`, and then higher-level logic in visitor should decide what to do with it.)
We could also use `ConditionTruthVal` for this purpose.


https://reviews.llvm.org/D45517