Relational: Assert type bounds after branch

[michael-schwarz]

After branches, it pays off to check that computed constraints remain consistent with type-bounds.

This closes #1697 where this issue manifested as a both branches dead message. The test is for an equivalent arithmetic on integer bot case.

[sim642]

The CI shows a lot of test failures with this.

What I'm wondering is why type bounds would be lost by branch to begin with?
I guess this assertion wasn't added there because intuitively type bounds would persist which would make this unnecessary, but seems like that's not the case?

[michael-schwarz]

The CI shows a lot of test failures with this.

Yeah, I used e instead of e' by mistake.

What I'm wondering is why type bounds would be lost by branch to begin with?

This is avery good question I also have no answer to.

[michael-schwarz]

The remaining regression test are ones where the termination analysis tries to build non-terminating loops over int, which does not work because that analysis set the assume_none flag.

[sim642]

The remaining regression test are ones where the termination analysis tries to build non-terminating loops over int, which does not work because that analysis set the assume_none flag.

This might be the place where I wondered about a #1696 (comment) -like situation before: what's supposed to happen if we want to assume that something, which definitely happens, does not happen?
It's the kind of nonsense where UB allows compilers to do weird things (delete the loop altogether or whatever), but I don't know what an analyzer should do about it.

[michael-schwarz]

Closed in favor of #1699.