Prepare to release sum type support in verify

[shonfeder]

This PR includes the updates we need prior to cutting a release that brings support of sum types into the verify command.

• Updates to examples to ensure we are testing some edge cases
• Updates to the examples dashboard and runner script to reflect current abilities
• Updating the apalache version pinned to the latest release
• Updating the feature table on the readme

---

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[bugarela]

LGTM, only one non-blocking point

[bugarela]

I'd rather not have this if and always keep the explanations updated. If something is succeeding, then there should be no explanation, and a new failing thing should prompt us to "investigate" enough to assign a new explanation to the failing cell. Otherwise, we might fall back to old explanations that are not the real problem anymore.

[shonfeder]

This conditional ensures that will only be an explanation if something fails. If it success, we don't print the explanation. My thinking was that will result in a bigger diff and a better chance of someone noticing that this needs to be updated. With the current logic, the explanation is printed whether or not the run succeeds, which I think makes it less likely for the required change to be noted.

It's exactly your concern that motivated this change :)

But I think we ought to rework this script entirely before long. So if you don't object hard here, I'll leave it as is and either adjust in a followup or when we rework this.

[konnov]

LGTM!

[konnov]

That's nice :)

[shonfeder]

Thanks for the reviews!