[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:1267
+
+    Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
----------------
george.karpenkov wrote:
> almost certainly a bug, we shouldn't default to unfeasible when the list of constraints is empty.
Ooops, sorry, now I see how the code is supposed to work.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292
+      Constraints =
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+    }
----------------
NoQ wrote:
> 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.
Ah, thanks, right! Then my previous comment regarding `false` is wrong.


https://reviews.llvm.org/D45517