https://github.com/isuckatcs commented: LGTM apart from some typos. Maybe we also want to add the unary negation part to the documentation of `ShouldEagerlyAssume` in `AnalyzerOptions.def`. https://github.com/llvm/llvm-project/pull/112209