george.karpenkov added a comment. > If the type extension approach is proven to be sound
I lack the full context here, but in my experience Z3 is really great for proving whether certain operations may or may not overflow, using the built-in bitvector type. (I'm not sure though if that is what is being done here). https://reviews.llvm.org/D35109 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
