`location_invariant` YAML entry type as schema
This adapts #59 on top of #61. Since this depends on #61 being merged, the PR diff currently isn't nice, but a nicer diff can be seen here: https://github.com/sim642/sv-witnesses/compare/yaml-schema...goblint:sv-witnesses:location_invariant.
Changes
- Add
location_invariant
YAML entry type. - Generalize
loop_invariant_certificate
entry type toinvariant_certificate
entry type, which may target both invariant entry types. This avoids unnecessary duplication. - Clarifies that
loop_invariant
entries are strictly for loops.
These changes solve https://github.com/sosy-lab/sv-witnesses/issues/60.
Edited by Simmo Saan