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
