On Thu, 5 Jun 2025 at 02:15, Tom Honermann <tom_at_[hidden]> wrote:
> > Relying on a hypothetical assume semantic doesn't help, especially
> > because using that makes it not the same program, the compiled-altered
> > program
> > has different semantics.
>
> The semantics are only different, discounting side effects of contract
> predicate evaluation, if an assume semantic is violated.

Which itself means that the semantics are different. They are
different in exactly the same way
as

switch (foo) {
case 1: bar1();break;
case 2: bar2(); break;
case 3: bar3(); break;
default: std::unreachable();
}
code_that_follows();

and

switch (foo) {
case 1: bar1();break;
case 2: bar2(); break;
case 3: bar3(); break;
}
code_that_follows();

are different.

And then, when there is a contract annotation that doesn't change the
well-defined/undefined behavior sets of a program, and an annotation
that does,
they *should* be different, in source code.

Thank you very much for this discussion. It crystallized the above.