Skip to content

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Sep 5, 2025

Closes #1782.

In the problematic test, the changed line was casting 4294967295UL (same after division by sizeof(char)) to the type of the lvalue n_update, which is int. This cast is not safe and caused an incorrect -1 bound to be used.

This PR adds a check with VD.is_dynamically_safe_cast before doing the cast.

This is the very base case of invariant_fallback, so the change could have quite an impact. Although lvalues are also refined by HC4's inv_exp at the non-fallback level. So I'm not sure how often the fallback case actually gets used.

@sim642 sim642 added this to the SV-COMP 2026 milestone Sep 5, 2025
@sim642 sim642 added bug unsound sv-comp SV-COMP (analyses, results), witnesses labels Sep 5, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug sv-comp SV-COMP (analyses, results), witnesses unsound
Projects
None yet
Development

Successfully merging this pull request may close these issues.

base invariant_fallback mishandles casts
1 participant