Skip to content

2025 final execution #216

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
bobot merged 97 commits into from
Aug 11, 2025
Merged

2025 final execution #216

bobot merged 97 commits into from
Aug 11, 2025

Conversation

@martinjonas
Copy link
Contributor

@martinjonas martinjonas commented Aug 10, 2025

No description provided.

Martin Jonáš and others added 30 commits July 6, 2025 08:40
Add generation of parallel benchmarks and test runs.
90cd20d
Do not use walltime killer anymore.
5452dd7
Use --continue-after-unknown.
bca1f08
Better status reporting.
6258316
Show contacts only of competitive solvers.
c635d8e
Generate more meaningful YML names.
680a97a
Update removed benchmarks.
ce5b4e7
Remove benchmarks also for non-AWS tracks.
e12e8a1
Revert "Do not use walltime killer anymore."
0402477 
This reverts commit 5452dd7.
Parse the single query/incremental results without scramble_id.
8800f20
@mpreiner
bitwuzla: Change options for parallel track. (#201)
b7c46ac 
* bitwuzla: Change options for parallel track.

Add additional configurations for lower CPU core counts.

* Make additional configurations non-competitive.
@zmylinxi99
submission: add additional configurations for lower CPU core counts. (#…
4fddcda 
…202)
Remove unused AWS infrastructure.
dde119e
fix: Use LazyFrame during selection of incremental benchmarks.
2c57e14
feat: Do not declare required machines for the parallel track.
f95717c
feat: Memory limit for parallel track.
76076e2
Change names of reduced-core parallel solvers.
f75b731
fix: Correctly recognize out of memory for incremental track.
96256c6
feat: Adapt parsing of Incremental results to new YML names.
8297d7f
fix: Add nb_answers to all results.
9ebce05
feat: Update year.
24a718f
feat: Better structure of generated result directories.
f4beace
@Tomaqa
SMTS submission 2025 update (bug fix + 2 more versions) (#203)
509927e
feat: Do not fail on missing runs, only report errors.
04d8bff
feat: Adapt unsat core and model result parsing to new YML names.
66c5d56
fix: Unify columns for all tracks to get consistent data set.
fc197d5
fix: Drop benchmark_yml only during result processing.
d79ee2b
fix: Initialize unsat core column.
3640e5d
fix: Move previous year.
af6462e 
Temporary fix to get the correct statistics of executed results, because the
benchmarks were generated before the year was moved to 2025.
feat: Allow flushing cache in benchexec conversion.
5b7bfd4
@github-actions
Copy link

github-actions bot commented Aug 10, 2025 •
edited
Loading

Summary of modified submissions

STP-Parti-Bitwuzla-32core

STP-Parti-Bitwuzla-64core

STP-Parti-Bitwuzla-16core

Z3-Parti-Z3pp-32core

Z3-Parti-Z3pp-64core

Z3-Parti-Z3pp-16core

Bitwuzla-32core

  • 2 authors
  • website: https://bitwuzla.github.io/
  • Participations
    • Parallel
      • Bitvec
        • all
      • Equality+MachineArith
        • ABV
        • ABVFP
        • ABVFPLRA
        • AUFBV
        • AUFBVFP
        • UFBV
        • UFBVFP
      • FPArith
        • all
      • QF_Bitvec
        • all
      • QF_Equality+Bitvec
        • QF_UFBVDT
      • QF_FPArith
        • QF_UFFPDTNIRA

Bitwuzla-64core

  • 2 authors
  • website: https://bitwuzla.github.io/
  • Participations
    • Parallel
      • Bitvec
        • all
      • Equality+MachineArith
        • ABV
        • ABVFP
        • ABVFPLRA
        • AUFBV
        • AUFBVFP
        • UFBV
        • UFBVFP
      • FPArith
        • all
      • QF_Bitvec
        • all
      • QF_Equality+Bitvec
        • QF_UFBVDT
      • QF_FPArith
        • QF_UFFPDTNIRA

Z3-alpha-base

  • 1 authors
  • website: https://github.com/Z3Prover/z3
  • Participations
    • SingleQuery
      • Arith
        • all
      • QF_Bitvec
        • all
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
      • QF_Strings
        • all

@bobot bobot merged commit c3cc3f0 into master Aug 11, 2025
5 checks passed
@bobot bobot deleted the 2025_final_execution branch August 11, 2025 11:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@martinjonas @bobot @mpreiner @zmylinxi99 @Tomaqa @wintered