Skip to content

Conversation

@karoliineh
Copy link
Member

TODO: we want to cherry-pick some parts of these changes

due to the uncil-ing only changing next but not the prev nodes
and only consider  `InlineEntry` and `InlineReturn` without `Entry` and `Ret` for creating the callstack
…d by Witch) in the path suffix when trimming the path
@karoliineh karoliineh added the sv-comp SV-COMP (analyses, results), witnesses label Nov 27, 2025
@sim642 sim642 self-requested a review November 27, 2025 13:44
@sim642 sim642 added this to the v2.8.0 milestone Nov 27, 2025
sim642 and others added 20 commits November 28, 2025 15:42
Last usage was removed a long time ago in cb32b12.
…h leads to unfollowable path

partition_if_next uses List.find to find one branch, but there may be multiple with different paths.
If the arbitrarily chosen path ends up being dead in the ARG, some ARG node may be missing, just because partition_if_next picked the "wrong" path.
Instead their paths should just be concatenated.
Introduced in b8b6041.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

feature sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants