Nodes are not properly re-queued when propagating conditions across desync points #447
Comments
danmatichuk
added a commit
that referenced
this issue
Sep 11, 2024
this ensures that the domain is computed under the strongest possible set of assumptions, as well as ensuring that assertions are necessarily propagated NB: this breaks challenge 10 and target 7, since it fixes #447 but not #448 (i.e. desync points are now properly re-queued for analysis during propagation, but the generated assertions are incorrect)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When a condition is propagated through a single-sided analysis, it needs to be propagated from the single-sided copy of the desync node to the original two-sided node (if it is not provable yet at the desync point).
Currently when a condition is added to a single-sided desync point, the two-sided node is not re-queued for analysis and as a result the condition is not propagated by default. As a result, assertions that are unprovable are not caught, as they stop propagating at the desync point and then are allowed to remain unproven without raising any errors.
The text was updated successfully, but these errors were encountered: