Termination analysis cleanup

[sim642]

#1093 leaves a bunch of things to clean up after merging for SV-COMP 2024:

• [ ] Clarify and document new test annotations: https://github.com/goblint/analyzer/pull/1093#discussion_r1356945296.
• [ ] Fix incremental analysis support: https://github.com/goblint/analyzer/pull/1093#discussion_r1345624525, https://github.com/goblint/analyzer/pull/1093#discussion_r1345647274.
• [ ] Refactor CIL location based logic: https://github.com/goblint/analyzer/pull/1093#discussion_r1345624525.
• [ ] Fix CIL location based upjumping goto check: https://github.com/goblint/analyzer/pull/1093#issuecomment-1759089957.
• [ ] Improve termination check with upjumping goto-s: https://github.com/goblint/analyzer/pull/1093#issuecomment-1700500890.
• [ ] Exclude termination variables from witness invariants.
• [ ] Exclude inserted statement nodes from witnesses.
• [ ] Optimize analysis: https://github.com/goblint/analyzer/pull/1093#issuecomment-1816126920.