RecordFlux icon indicating copy to clipboard operation
RecordFlux copied to clipboard

Published 20 hours ago • verified publisher icon AdaCore

Fix and simplify message proofs

Open senier opened this issue 2 years ago • 0 comments

Currently _prove_reachability does not include constraints (type constraints and potentially others) which prevents it from finding unreachable paths.

When the reachability proof is fixed, _prove_contradictions can be removed.

senier avatar Jun 28 '22 12:06 senier