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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292
+      Constraints =
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+    }
----------------
george.karpenkov wrote:
> I'm very confused as to why are we doing disjunctions here.
I think this corresponds to RangeSet being a union of Ranges.


https://reviews.llvm.org/D45517