You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The move from separate location_invariant and loop_invariant entries to one invariant_set entry in YAML witnesses had an unintended consequence: all invariants from the set are tagged with the same UUID of the entry.
These UUIDs are used as widening tokens that should delay widening. However, since there's just one widening token, only one widening is ever delayed. As opposed to delaying widening of each invariant unassume separately. This may cause significant precision loss in the YAML witness validator.
The text was updated successfully, but these errors were encountered:
The move from separate
location_invariant
andloop_invariant
entries to oneinvariant_set
entry in YAML witnesses had an unintended consequence: all invariants from the set are tagged with the same UUID of the entry.These UUIDs are used as widening tokens that should delay widening. However, since there's just one widening token, only one widening is ever delayed. As opposed to delaying widening of each invariant unassume separately. This may cause significant precision loss in the YAML witness validator.
The text was updated successfully, but these errors were encountered: