https://github.com/NagyDonat commented:
Do I understand it correctly that this deficiency affects the standalone Z3 analysis mode (as opposed to the "Z3 refutation" where the analysis is performed with the native range-based constraint manager, and then the results are validated with Z3 to discard the logically impossible paths)? https://github.com/llvm/llvm-project/pull/108900 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
