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

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391
+    if (!RefutationMgr->isModelFeasible())
+      BR.markInvalid("Infeasible constraints", N->getLocationContext());
+  }
----------------
george.karpenkov wrote:
> That would be checking all constraints in all nodes one by one. I thought the idea was to encode all constraints from the entire path and then check all of it.
All the constraints are being added in the previous for loop, isModelFeasible only calls check().


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925
 
+  void reset() override { Solver.reset(); }
+
----------------
george.karpenkov wrote:
> We don't need `reset` anymore.
We don't need it but there's no reason to remove it, right? I might be useful in the future.


https://reviews.llvm.org/D45517