NoQ added a comment. In https://reviews.llvm.org/D45920#1074439, @george.karpenkov wrote:
> Another approach would be to instead teach `RangedConstraintManager` to > convert it's constraints to Z3. That would be an unwanted dependency, but the > change would be much smaller, and the internals of the solver would not have > to be exposed. @NoQ thoughts? Dunno. Obviously, the adaptor code between the constraint manager and the refutation manager (i think the word "solver" is causing confusion now) would have to access internals of both managers, so the situation is quite symmetric. Repository: rC Clang https://reviews.llvm.org/D45920 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
