-
Johannes Kanig authored
On N127-001, an optimisation of the fast WP was introduced, based on marking states that contain variables that need to be refreshed when merging them. However, this "marked" status was incorrectly reset to false when merging states, even though some of those "unfresh" variables could survive the merge. The consequence was that the WP was reusing variables too aggressively, which would result in incorrect VCs. We now compute the marked status of a merged state from the states to be merged: if one of them is marked, the merged state is marked too. mlw_wp.ml: (merge): synthetize marked status from input states Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995
6c65e7ee