usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

Graph: More carefule node elimination #52

Closed blishko closed 9 months ago

blishko commented 9 months ago

When contracting a vertex with an incoming edge that has auxiliary variables, we have to be careful not to end up with the same auxiliary variable in the labels of multiple edges. This could cause problems when considering paths containing such edges, because we could end up with a name clash.

The current fix is to rename auxiliary variables when this potential clash could occur.

In the future we should rethink our versioning strategy, possibly enforce stronger invariants that would prevent this scenario in the first place.

Fixes #51.