From 419bf025cba98b93a519ae6d384a4b9f2e41fd4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Jon=C3=A1=C5=A1?= Date: Mon, 20 Jul 2026 09:00:15 +0200 Subject: [PATCH 1/3] chore: Mark fixed bitwuzla as noncompeting. --- submissions/bitwuzla-fixed.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/bitwuzla-fixed.json b/submissions/bitwuzla-fixed.json index 8d48e09ae..39a4ac7ee 100644 --- a/submissions/bitwuzla-fixed.json +++ b/submissions/bitwuzla-fixed.json @@ -3,7 +3,7 @@ "contributors": ["Aina Niemetz", "Mathias Preiner"], "contacts": ["Mathias Preiner "], "final": true, - + "competitive": false, "archive": { "url": "https://zenodo.org/records/21445437/files/bitwuzla-submission-smtcomp-2026.zip?download=1", "h": {"sha256": "9ff83e5a77d5af392386341e462c5fb2d420d0e9e27ab22900b02026d2871745"} From 5dd93fe2c405fba414e0fd0431300f3eac7abe6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Jon=C3=A1=C5=A1?= Date: Mon, 20 Jul 2026 09:00:40 +0200 Subject: [PATCH 2/3] chore: Remove seed (it is already fixed). --- submissions/bitwuzla-fixed.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/bitwuzla-fixed.json b/submissions/bitwuzla-fixed.json index 39a4ac7ee..a722b6899 100644 --- a/submissions/bitwuzla-fixed.json +++ b/submissions/bitwuzla-fixed.json @@ -14,7 +14,7 @@ "website": "https://bitwuzla.github.io", "system_description": "https://bitwuzla.github.io/data/smtcomp2026/paper.pdf", "solver_type": "Standalone", - "seed": "42", + "seed": "0", "participations": [ { "tracks": ["SingleQuery"], From 475e221214fc4a6cf0193f0fa22e946517778955 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Jon=C3=A1=C5=A1?= Date: Mon, 20 Jul 2026 09:02:08 +0200 Subject: [PATCH 3/3] chore: Lint. --- web/content/cloud_track/call-for-solvers.txt | 12 +++++----- web/content/cloud_track/index.md | 23 +++++++++++++------- web/content/news/2026-05-16-final-call.md | 15 +++++-------- 3 files changed, 27 insertions(+), 23 deletions(-) diff --git a/web/content/cloud_track/call-for-solvers.txt b/web/content/cloud_track/call-for-solvers.txt index 4d334e35f..0d1fc264f 100644 --- a/web/content/cloud_track/call-for-solvers.txt +++ b/web/content/cloud_track/call-for-solvers.txt @@ -11,9 +11,9 @@ k We invite registration of solvers for the cloud track at SMT-COMP 2026. -The cloud track is run separately from all other tracks with its own procedur es, -infrastructure, deadlines, and result announcement. Please read the related -instructions on the SMT-COMP website [1]. +The cloud track is run separately from all other tracks with its own procedur es, +infrastructure, deadlines, and result announcement. Please read the related +instructions on the SMT-COMP website [1]. The submission deadline for (first versions of) cloud solvers is @@ -25,8 +25,8 @@ submitted solvers may be updated via the pull request until ***Aug 22, 2026 AoE*** -The cloud track is hosted by AWS and uses a different infrastructure than -all other tracks. +The cloud track is hosted by AWS and uses a different infrastructure than +all other tracks. The organizing team @@ -34,7 +34,7 @@ Dominik Winterer (chair) - University of Manchester, United Kingdom Martin Jonáš - Masaryk University, Czechia Tomáš Kolárik - Università della Svizzera italiana, Switzerland -Contacts for inquiries about the cloud track: +Contacts for inquiries about the cloud track: Cayden Codel — crcodel@amazon.com Robert Jones — rbtjones@amazon.com diff --git a/web/content/cloud_track/index.md b/web/content/cloud_track/index.md index 306e45ba6..9f8690aac 100644 --- a/web/content/cloud_track/index.md +++ b/web/content/cloud_track/index.md @@ -2,45 +2,52 @@ The cloud track of SMT-COMP '26 is run separately from all other tracks with its own procedures, infrastructure, deadlines, and result announcement. -### Key dates +### Key dates + - **Aug 8, 2026**— preliminary call for solvers (should compile & pass basic tests). - **Aug 22, 2026** — final call for solvers All deadlines are 11:59 PM AoE (Anywhere on Earth). -### Submission Instructions +### Submission Instructions + +#### Infrastructure -#### Infrastructure -[`aws-samples/aws-batch-comp-infrastructure-sample`](https://github.com/aws-samples/aws-batch-comp-infrastructure-sample) on the **`mainline-2026`** (default). +[`aws-samples/aws-batch-comp-infrastructure-sample`](https://github.com/aws-samples/aws-batch-comp-infrastructure-sample) on the **`mainline-2026`** (default). -*Each submission needs to be prepared according based on this repository.* +_Each submission needs to be prepared according based on this repository._ #### What to Submit + In your solver's repo, add a top-level **`aws-build/`** directory containing: + 1. **Dockerfile** — must extend the provided base Dockerfile; build solver **from source**; dependencies only via standard package managers (e.g. `apt-get`); `git clone` allowed only for open-source repos. 2. **`solver_cmd.py`** — returns the command-line args used to invoke your solver. Repo (including source) must stay **open source** at least through the final deadline. #### Solver Requirements + - Return exit codes: **10 = SAT, 20 = UNSAT, 0 = UNKNOWN**, anything else = error. -- (Distributed only) Your Dockerfile should compile solvers for both the leader and the worker. Note that the solver harness invokes one machine (the leader) per problem; the leader is responsible for driving workers over SSH/MPI using the provided list of IP addresses. +- (Distributed only) Your Dockerfile should compile solvers for both the leader and the worker. Note that the solver harness invokes one machine (the leader) per problem; the leader is responsible for driving workers over SSH/MPI using the provided list of IP addresses. - The provided solver harness downloads benchmarks previously uploaded to S3 (`.cnf`/`.smt2`, compressed OK) and runs until timeout/memout. - #### Steps + 1. Fix exit codes. 2. Write Dockerfile + `solver_cmd.py`. 3. Add YAML config describing the solver. 4. Build/test locally with `satcomp.py` (recommended before submitting). -5. *(Optional, encouraged)* Test on AWS — you cover costs, likely under $100. +5. _(Optional, encouraged)_ Test on AWS — you cover costs, likely under $100. 6. Submit repo link (or tarball) with `aws-build/`. #### Timeouts & Specs + - Cloud track timeout: **200s** (recommended, mirrors SAT-COMP). - Parallel track timeout: **1000s**. - 2024 hardware reference: 100x m4.4xlarge (16 vCPU / 8 core, 64GB RAM each). ### Contacts + - Cayden Codel — crcodel@amazon.com - Robert Jones — rbtjones@amazon.com diff --git a/web/content/news/2026-05-16-final-call.md b/web/content/news/2026-05-16-final-call.md index f7143c50c..40f889115 100644 --- a/web/content/news/2026-05-16-final-call.md +++ b/web/content/news/2026-05-16-final-call.md @@ -1,22 +1,19 @@ --- layout: single author: -title: Final Call for Solvers +title: Final Call for Solvers date: 2026-05-16T00:00:00+01:00 --- - 21st International Satisfiability Modulo Theories Competition - (SMT-COMP'26) - FINAL CALL FOR SOLVERS +21st International Satisfiability Modulo Theories Competition +(SMT-COMP'26) +FINAL CALL FOR SOLVERS July 24–25, 2026 Lisbon, Portugal - - We invite registration of solvers for SMT-COMP 2026. - Solvers are entered into the competition via a pull request to the SMT-COMP GitHub repository at: @@ -71,7 +68,7 @@ These can be specified as part of the solver submission and changed until the deadline for the final solver. The default configuration is used for all other tracks. -Please see the competition rules for further details. Do not hesitate contacting us +Please see the competition rules for further details. Do not hesitate contacting us if you have any questions or comments. Sincerely, @@ -83,6 +80,7 @@ Martin Jonáš - Masaryk University, Czechia Tomáš Kolárik - Università della Svizzera italiana, Switzerland ## COMMUNICATION: + The competition website is at https://smt-comp.github.io/2026/ @@ -91,4 +89,3 @@ https://github.com/SMT-COMP/smt-comp.github.io Public email regarding the competition may be sent to smt-announce@googlegroups.com -