analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Widening tokens for YAML `invariant_set` entries

Open sim642 opened this issue 8 months ago • 0 comments

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.

sim642 avatar Dec 19 '23 14:12 sim642