Internal errors are not just impossible executions

[sauclovian-g]

In general when all branches of execution become impossible, and you were not intending that, it's hard for a computer to tell which of them are impossible because they should be impossible and which are impossible because there's something wrong with your spec.

Therefore in this case saw prints what stopped each one. AIUI; at least, that's what appears to happen.

Currently, if some branches of execution crash (cause internal errors in saw, step on unsupported operations in crucible, etc.) those are apparently treated as impossible branches rather than as immediate errors, and so it's possible to get a report about such a problem combined with other entirely unimportant or bogus reports about non-matching overrides or other things in other branches.

This shouldn't be done that way. Not only are the reports on other branches of execution generally confusing, it's quite easy for a naive user to go on a wild goose chase investigating them in detail.

I think there must not be enough granularity in failure tracking somewhere.

(Also I hope that if one branch of execution crashes and others succeed that we aren't accidentally suppressing the crash message as if it's a routine false branch. That could turn out to be a pretty serious soundness problem.)

[RyanGlScott]

It would be helpful to distill a relatively self-contained example of this behavior happening.

[sauclovian-g]

No disagreement there 😐