When an assertion is introduced after the sync point following desync/sync analysis, it may need to be propagated back through one or both of the single-sided analyses in order to be proven. Currently when propagating through a sync point we duplicate the assertion and try to propagate it separately through both of the single-sided analyses. This is incorrect and will almost necessarily introduce unprovable assertions, as it results in introducing unbounded symbolic terms (i.e. the variables representing the undefined state of the opposite program state during a single-sided analysis step).
This issue was hiding behind #447, which caused these unprovable assertions to be undetected.
When an assertion is introduced after the sync point following desync/sync analysis, it may need to be propagated back through one or both of the single-sided analyses in order to be proven. Currently when propagating through a sync point we duplicate the assertion and try to propagate it separately through both of the single-sided analyses. This is incorrect and will almost necessarily introduce unprovable assertions, as it results in introducing unbounded symbolic terms (i.e. the variables representing the undefined state of the opposite program state during a single-sided analysis step).
This issue was hiding behind #447, which caused these unprovable assertions to be undetected.