baloghadamsoftware added a comment. Of course we would like to try the Z3 for refutation, we do not dispute its usefulness. This patch is about something really different. It extends the range-based constraint manager in a very natural way. Is the code of the range-based constraint manager frozen for some reason? If not, then why not add multiplication and division as well, where addition and subtraction is already supported?
https://reviews.llvm.org/D49074 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits