Caesar 4.1 fixes soundness bugs in @ast, @past, and @omega_invariant that could let invalid proofs pass verification.
It also introduces @uwlp, extends @ast to finite demonic nondeterminism, infers loop terminators, and adds HeyVL reference hovers in Visual Studio Code.
Recheck termination and ω-invariant proofs:
Earlier versions could accept invalid proofs using @ast, @past, or @omega_invariant.
Re-run their verification after upgrading.
In this release: