Skip to content

Expected verdicts of PieSegment_true and AlbersProjection_true #63

Open

Description

@nils-loose

Two _true tasks have reachable assertion failures, so SWAT's VIOLATION verdict is correct but is scored as wrong (-16 each). Replaying the witness values confirms both:

  • argv-tasks/PieSegment_true: nondetFloat() = NaN gives cAngle = NaN % 360, so assert cAngle >= 0.0 && cAngle <= 360.0 fails (Main.java:47). Upstream MR !1675 adds a finiteness guard to this task.
  • argv-tasks/AlbersProjection_true: all nondetDouble() = 0.0 gives result == 0, so assert result > 0 fails (Main.java:69). No upstream change known.

Witnesses: /home/nils/dev/sv-comp-validators/campaign-full-2026-10-15/witnesses/ (local).

Activity

  1. added this to the SV-COMP 2027 milestone on Oct 15, 2026
  2. nils-loose commented on Oct 18, 2026

    @nils-loose
    ContributorAuthor

    Also java/objects/objects09 (valid-assert, expected true): AFactory.createObject() returns null in its default case, and Verifier.nondetObject just calls factory.createObject(). So !(a instanceof A) holds and assert false is reached. Plain java -ea with the benchmark Verifier throws AssertionError at Main.java:19. Found with #66.

  3. nils-loose commented on Oct 18, 2026

    @nils-loose
    ContributorAuthor

    Also java-ranger-regression/apachecli_eqchk (no-runtime-exception, expected true). CLI.execute catches the ParseException (CLI.java:101) and returns commandLine, which is still null. TestCLI.java:18 then calls outSPF.equals(...) on null, a real NullPointerException. Inputs: - then seven \0 chars, and false. It reproduces on a plain JVM. Found with #72.

  4. nils-loose commented on Oct 19, 2026

    @nils-loose
    ContributorAuthor

    Also argv-tasks/WeibullGenerator_exceptionless (no-runtime-exception, expected true). This reproduces on a plain JVM:

    1. An infinite lamda is reset to 0.
    2. A tiny negative beta makes (int)(1/beta) equal Integer.MIN_VALUE.
    3. pow then becomes infinite, and 0 × infinity is NaN, so the uncaught RuntimeException is real.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions