Skip to content

Conversation

@AdamZsofi
Copy link
Member

@leventeBajczi and I just found that --max-bound on xcfa-cli does nothing. Now it's properly added to the checker.

Also, unknown results were actually not working so far, proofs (well, partial results) were null and this caused issues. Now the different levels of SafetyResult, logging, etc. actually handle it.

@mondokm can you check please if it seems to be in order? Thanks!

@AdamZsofi AdamZsofi requested a review from mondokm November 29, 2025 14:11
@AdamZsofi AdamZsofi added the bug label Nov 29, 2025
@AdamZsofi AdamZsofi changed the title Missing bmc bound and unknown details added to checker Missing bmc bound and unknown result details added to checker Nov 29, 2025
@AdamZsofi AdamZsofi changed the title Missing bmc bound and unknown result details added to checker Missing bmc bound and unknown result details added Nov 29, 2025
@github-actions
Copy link
Contributor

❗ Please modify build.gradle.kts to contain a later version than 6.27.5. Current version is 6.27.5.

@github-actions
Copy link
Contributor

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition COMPLEX EMERGENT HORN
SV-COMP25_no-data-race ✅ (59 / 0 / 89) HTML/CSV ✅ (32 / 0 / 68) HTML/CSV ✅ (20 / 0 / 83) HTML/CSV
SV-COMP25_no-overflow ✅ (16 / 0 / 48) HTML/CSV ❓ (0 / 0 / 37) HTML/CSV ❓ (0 / 0 / 90) HTML/CSV
SV-COMP25_termination ✅ (1 / 0 / 202) HTML/CSV ✅ (1 / 0 / 202) HTML/CSV ✅ (14 / 0 / 304) HTML/CSV
SV-COMP25_unreach-call ✅ (18 / 0 / 87) HTML/CSV ✅ (16 / 0 / 93) HTML/CSV ✅ (10 / 0 / 191) HTML/CSV
SV-COMP25_valid-memcleanup ❓ (0 / 0 / 66) HTML/CSV ❓ (0 / 0 / 66) HTML/CSV ❓ (0 / 0 / 66) HTML/CSV
SV-COMP25_valid-memsafety ✅ (34 / 0 / 317) HTML/CSV ✅ (3 / 0 / 276) HTML/CSV ❓ (0 / 0 / 356) HTML/CSV

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants