Skip to content

Review and update dependency versions #50

Closed

Description

@nils-loose

Check which dependencies can/should be updated before the SV-COMP 2027 submission (target: Ubuntu 26.04, Python 3.14, JDK 17).

  • Z3: native libs 4.15.4 (build.gradle copyNativeLibs, glibc-2.39 build) and z3-solver==4.15.4.0 (explorer + svcomp package) — keep both in sync; see Fetch Z3 distribution during build #44 / Fetch z3 version instead of packaging it #7
  • JavaSMT, ASM (asmAsmVersion), Lombok, Jackson, logback in symbolic-executor
  • Python deps in symbolic-explorer/requirements.txt and scripts/svcomp-package/requirements.txt (Python 3.14 wheels)
  • Build tooling: Gradle wrapper 8.4, shadow 8.1.1, lombok plugin 8.4
  • Note for each: current → latest, breaking changes, decision (update / keep)
  • For Z3 and JavaSMT: review release notes for features worth using before the final resubmission (Nov 17), e.g. solver performance, new theories/APIs, string/FP improvements

Activity

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

    @nils-loose
    ContributorAuthor

    Done in #92:

    • Z3 4.15.4 → 5.3.1 in the executor and the explorer. The explorer keeps the previous regex solver (smt.seq.regex_monadic=false), because the new default turned a SAFE task into a timeout.
    • JavaSMT 6.0.0 plus upstream fix 3113516df, vendored in libs/maven.
    • ASM 9.11.1, Jackson 2.22.4, logback 1.6.5, SLF4J 2.0.20, Spock 2.5, Mockito 5.24.
    • Gradle 8.14.6 and the plugins.
    • The Python dependencies and the CI actions.
    • Kept: Gradle 9, because the Spring Boot 2 plugin of the target apps fails under it.
    • Measured on all 1713 runs: +8 points, 0 new wrong verdicts. coral81 and Optimization2 time out because some FP queries are slower in Z3 5.x.

    Worth trying before Nov 17:

    • try the monadic regex solver first, then fall back to the old one;
    • symbolic DREM/FREM, now that the Z3 FP fixes are in;
    • incremental solving over shared path prefixes.

    Note: the global Z3 options of the JavaSMT fork (feature/z3-native-options) never took effect, because the build uses Maven JavaSMT. The key solver.z3.timout in ThreadContext is also misspelled.

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