We should more clearly link these instances to the literature, e.g., https://doi.org/10.1145/605466.605475,
to highlight that these (correct) rewrites might hint at correctness errors in the analyzed code.
Of course, when these rewrites are part of post processing (beautification) no error is present.
The pattern
https://github.com/TNO/Rewriters-Ada/blob/736dbf041188f3ed22423f91467df0d6358b5197/src/predefined_rewriters_boolean_expression_simplify.ads#L68 is an instance of a "redundant operation" that commonly flag correctness errors. We have many of such instances in the rewriter library.
We should more clearly link these instances to the literature, e.g., https://doi.org/10.1145/605466.605475, to highlight that these (correct) rewrites might hint at correctness errors in the analyzed code.
Of course, when these rewrites are part of post processing (beautification) no error is present.