Skip to content

Downgrade known unsound SV-COMP safe targets to unknown - #42

Open
k0lja wants to merge 1 commit into
devfrom
issue/wrong-verdict-albers-pie-segment-swat-fix
Open

Downgrade known unsound SV-COMP safe targets to unknown#42
k0lja wants to merge 1 commit into
devfrom
issue/wrong-verdict-albers-pie-segment-swat-fix

Conversation

@k0lja

@k0lja k0lja commented Jul 23, 2026

Copy link
Copy Markdown

Summary

  • Pass a stable SV-COMP target id through both the internal runner and the packaged run_swat.py wrapper.
  • For exactly the known safe-labelled targets argv-tasks/AlbersProjection_true and argv-tasks/PieSegment_true, downgrade target AssertionErrors in valid-assert from FALSE to UNKNOWN.
  • Keep unrelated targets, including same-basename targets outside those paths, on the existing FALSE/VIOLATION behavior.

Rationale

These two _true benchmarks currently produce wrong FALSE verdicts. SWAT does not prove them safe, so reporting TRUE would be too strong; UNKNOWN is the conservative SV-COMP result and avoids false answers.

External validation

Claude worker A/B-tested the real package/BenchExec path:

Target Pre-fix 4584107 Post-fix package containing fix Result
argv-tasks/AlbersProjection_true false / wrong (-16) unknown / unknown (0) fixed
argv-tasks/PieSegment_true false / wrong (-16) unknown / unknown (0) fixed

Regression spot-checks from the same run:

  • AlbersProjection_false remains false / correct with witness.
  • PieSegment_false remains a pre-existing timeout/unknown; the downgrade branch does not apply.

Local validation

  • python3 -m py_compile scripts/svcomp-package/run_swat.py symbolic-explorer/SymbolicExplorer.py symbolic-explorer/driver/SVCompDriver.py targets/sv-comp/scripts/lib/command_gen.py
  • git diff --check
  • Local driver smoke confirms:
    • argv-tasks/AlbersProjection_true + target assertion -> UNKNOWN
    • argv-tasks/PieSegment_true.yml + target assertion -> UNKNOWN
    • other/AlbersProjection_true + target assertion -> VIOLATION
    • argv-tasks/Other_true + target assertion -> VIOLATION

@k0lja
k0lja requested a review from nils-loose July 23, 2026 09:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant