Consider an option to hide "always-true" enforcements in the report, but maybe with a warning

[dgpv]

From https://github.com/dgpv/bsst/pull/33#issuecomment-2123371113:

I'm doing the first case, so hiding the impossible things would be good for me right now, but the second case is definitely a real thing too.

I would say that 'always-true' enforcements are not "impossible" things. They might be called "irrelevant" in some narrow context. If you do not care about the facts that script might be doing something irrelevant, like checking a condition that is always true, then ignoring them does not do harm.

But for bsst to find out that the enforcement is always true, it will need Z3 enabled. And then it will mark that enforcement with <*> or {*}

I guess there could be a mode that will eliminate always-true enforcements from the report. But I think it will need to come with a visible warning indicating that the information reported about the script is not complete