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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits