[Formal][Property Annotation] Annotate path--single-sent-fork-output#713

Draft

Basmet0 wants to merge 10 commits intoEPFL-LAP:mainfrom

Basmet0:invariant3

Commits on Feb 5, 2026

invariant 3 boilerplate
Bas Niekel
committed
invariant 3 annotation and generation
Bas Niekel
committed
comment explaining the invariant
Bas Niekel
committed
removed debug prints
Bas Niekel
committed
added consistent naming of load operator slots in the smv unit generator
Bas Niekel
committed
better naming of functions
Bas Niekel
committed
formatting
Bas Niekel
committed
expand acronyms
Bas Niekel
committed
combined everything into a single function
Bas Niekel
committed
formatting
Bas Niekel
committed