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.
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.