2025 final submissions (#200)

martinjonas · Martin Jonáš · web-flow · commit 853f52100ff7 · 2025-07-04T13:33:42.000+02:00
* Rename z3siri-base.

* Mark all submissions as final.

* Mark base solvers as noncompetitive.

* Always generate participant data.

* Remove extra commas.

* Shorten names of some tools.

* Rename base solver of Z3-Owl and make it noncompetitive.

* Export noncompetitive flag into the submission summary.

* Mark noncompetitive participants.

* Fix Z3-Noodler-Mocha-base submission.

* Separate non-competing participants.

* Add participants menu page.

* Add 2025 NYSE seed.

* Skip non-competitive participants in seed computation.

* Remove seeds from base solvers.

* Also display seeds of participants.

* Fix formatting.

* Add Participants page.

* Add news about final list of participants.

* Fix formatting.

* Fix path to the base solver of Z3-Noodler-Mocha.

---------

Co-authored-by: Martin Jonáš &lt;martin.jonas@mail.muni.cz&gt;
diff --git a/Makefile b/Makefile
@@ -55,7 +55,7 @@ submission-doc: submission-generation
 
 participant-data:
 	@echo "🚀 Generating participant data to $(PARTICIPANT_DATA_FILE)"
-	@if [ -e "submissions/*.json" ]; then poetry run smtcomp show-json submissions/*.json $(PARTICIPANT_DATA_FILE); fi
+	@poetry run smtcomp show-json submissions/*.json $(PARTICIPANT_DATA_FILE)
 
 track-data:
 	@echo "🚀 Generating track data to $(TRACK_DATA_FILE)"
diff --git a/smtcomp/defs.py b/smtcomp/defs.py
@@ -1466,9 +1466,9 @@ class Config:
     """Prioritize triviality as much as possible for testing purpose.
         Look for simple problems instead of hard one"""
 
-    nyse_seed = 17817
+    nyse_seed = 20_338_41
     """The integer part of one hundred times the opening value of the New York Stock Exchange Composite Index on the first day the exchange is open on or after the date specified in nyse_date"""
-    nyse_date = date(year=2024, month=6, day=17)
+    nyse_date = date(year=2025, month=6, day=30)
 
     aws_timelimit_hard = 180
     """
@@ -1594,6 +1594,9 @@ def seed(self) -> int:
         unknown_seed = 0
         seed = 0
         for s in self.submissions:
+            if not s.competitive:
+                continue
+
             if s.seed is None:
                 unknown_seed += 1
             else:
diff --git a/smtcomp/submission.py b/smtcomp/submission.py
@@ -57,7 +57,9 @@ def raw_summary(s: Submission) -> dict[str, Any]:
     data["website"] = str(s.website)
     data["archive_url"] = str(s.archive.url if s.archive is not None else "")
     data["system_description"] = str(s.system_description)
+    data["competitive"] = s.competitive
     data["tracks"] = dict[str, dict[str, list[str]]]()
+    data["seed"] = s.seed
 
     tracks = s.participations.get()
     for track, divs in sorted(tracks.items()):
diff --git a/submissions/Amaya.json b/submissions/Amaya.json
@@ -18,5 +18,6 @@
             "tracks": ["SingleQuery"],
             "logics": ["LIA", "NIA"]
         }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2025-base.json b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2025-base.json
@@ -10,7 +10,6 @@
     "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-031-37703-7_1",
     "command": [ "./bitwuzla" ],
     "solver_type": "Standalone",
-    "seed": 42,
     "participations": [
         { "tracks": ["SingleQuery"], "logics": "QF_BV" }
     ],
diff --git a/submissions/COLIBRI.json b/submissions/COLIBRI.json
@@ -18,5 +18,6 @@
             "logics": "QF_.*FP(?!DT).*"
         }
     ],
-    "seed": 0
+    "seed": 0,
+    "final" : true
 }
diff --git a/submissions/STP-Parti-Bitwuzla.json b/submissions/STP-Parti-Bitwuzla.json
@@ -1,5 +1,5 @@
 {
-    "name": "STP-Parti-Bitwuzla-at-SMT-COMP-2025",
+    "name": "STP-Parti-Bitwuzla",
     "contributors": [
         "Mengyu Zhao",
         "Zhenghang Xu",
diff --git a/submissions/Z3-Inc-Z3++-base.json b/submissions/Z3-Inc-Z3++-base.json
@@ -11,9 +11,9 @@
     "system_description": "https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24",
     "command": [ "./smtcomp_run_incremental" ],
     "solver_type": "Standalone",
-    "seed": 174228,
     "participations": [
         { "tracks": ["Incremental"], "logics": "QF_NIA" }
     ],
-    "competitive": false
+    "competitive": false,
+    "final" : true
 }
diff --git a/submissions/Z3-Inc-Z3++.json b/submissions/Z3-Inc-Z3++.json
@@ -15,5 +15,6 @@
     "seed": "19970530",
     "participations": [
         { "tracks": ["Incremental"], "logics": "QF_NIA" }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/Z3-Noodler-Mocha-base.json b/submissions/Z3-Noodler-Mocha-base.json
@@ -14,11 +14,10 @@
     "contacts": ["Lukáš Holík <holik@fit.vutbr.cz>"],
     "website": "https://github.com/VeriFIT/z3-noodler",
     "system_description": "https://github.com/VeriFIT/z3-noodler/blob/devel/doc/noodler/z3-noodler-system-description-2025.pdf",
-    "command": [ "./z3-noodler" ],
+    "command": [ "./z3-noodler/build/z3" ],
     "solver_type": "derived",
-    "seed": 48655,
     "participations": [
-        { "tracks": ["SingleQuery"], "logics": "QF_Strings" }
+        { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] }
     ],
     "competitive": false,
     "final": true
diff --git a/submissions/Z3-Owl-base.json b/submissions/Z3-Owl-base.json
@@ -1,5 +1,5 @@
 {
-    "name": "Z3-4.15.2.0",
+    "name": "Z3-Owl-base",
     "contributors": [
         "Nikolaj Bjørner et al."
     ],
@@ -11,7 +11,6 @@
     "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf",
     "solver_type": "Standalone",
     "command": ["./z3"],
-    "seed": "421",
     "participations": [
         {
             "tracks": ["SingleQuery"],
@@ -24,5 +23,7 @@
                 "QF_BVFP"
             ]
         }
-    ]
+    ],
+    "final" : true,
+    "competitive": false
 }
diff --git a/submissions/Z3-Owl.json b/submissions/Z3-Owl.json
@@ -24,5 +24,6 @@
                 "QF_BVFP"
             ]
         }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/Z3-Parti-Z3pp.json b/submissions/Z3-Parti-Z3pp.json
@@ -1,5 +1,5 @@
 {
-    "name": "Z3-Parti-Z3pp-at-SMT-COMP-2025",
+    "name": "Z3-Parti-Z3pp",
     "contributors": [
         "Mengyu Zhao",
         "Shaowei Cai"
diff --git a/submissions/bv_decide-nokernel.json b/submissions/bv_decide-nokernel.json
@@ -43,5 +43,6 @@
                 "--maxRecDepth=1048576"
             ]
         }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/bv_decide.json b/submissions/bv_decide.json
@@ -42,5 +42,6 @@
                 "--maxRecDepth=1048576"
             ]
         }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/cvc5.json b/submissions/cvc5.json
@@ -59,5 +59,6 @@
       "command": [ "bin/smtcomp_run_incremental" ]
     }
   ],
-"seed": 8465677983
+  "seed": 8465677983,
+  "final" : true
 }
diff --git a/submissions/iprover.json b/submissions/iprover.json
@@ -51,5 +51,6 @@
             ]
         }
     ],
-    "seed": 139 
+    "seed": 139,
+    "final" : true
 }
diff --git a/submissions/ostrich.json b/submissions/ostrich.json
@@ -21,5 +21,6 @@
     "seed": "718582",
     "participations": [
         { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json
@@ -40,5 +40,6 @@
             "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?",
             "command": ["smtinterpol"]
         }
-    ]
+    ],
+    "final" : true
 }
diff --git a/submissions/z3-noodler-base.json b/submissions/z3-noodler-base.json
@@ -11,7 +11,6 @@
     "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf",
     "solver_type": "Standalone",
     "command": ["./z3-noodler_smt-comp25/z3/z3"],
-    "seed": 4134,
     "participations": [
         {
             "tracks": ["SingleQuery"],
diff --git a/submissions/z3-siri-base.json b/submissions/z3-siri-base.json
@@ -11,11 +11,12 @@
     "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf",
     "solver_type": "Standalone",
     "command": ["./z3"],
-    "seed": "33",
     "participations": [
         { 
             "tracks": ["SingleQuery"], 
             "divisions": ["QF_NonLinearIntArith", "QF_NonLinearRealArith", "QF_Bitvec"]
         }
-    ]
+    ],
+    "final" : true,
+    "competitive": false
 }
diff --git a/submissions/z3alpha-base.json b/submissions/z3alpha-base.json
@@ -11,7 +11,6 @@
     "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf",
     "solver_type": "Standalone",
     "command": ["./z3"],
-    "seed": "33",
     "participations": [
         { 
             "tracks": ["SingleQuery"], 
@@ -26,5 +25,7 @@
                 "QF_Strings"
             ]
         }
-    ]
+    ],
+    "final" : true,
+    "competitive": false
 }
diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json
@@ -29,5 +29,6 @@
                 "QF_Strings"
             ]
         }
-    ]
-}
+    ],
+    "final" : true
+}
diff --git a/web/content/news/2025-07-04-list-of-participants.md b/web/content/news/2025-07-04-list-of-participants.md
@@ -0,0 +1,10 @@
+---
+layout: single
+author:
+title: List of participants is final
+date: 2025-07-04T00:00:00+01:00
+---
+
+The [list of participants](/2025/participants) of SMT-COMP 2025 is final. We are happy to have received so many solvers and we are looking forward to the results.
+
+New York Stock Exchange index on the date after the submission deadline (i.e, 2025-06-30) was 20338.41, resulting in a competition seed of 2033841 + 755033430 = **757067271**.
diff --git a/web/content/participants/_index.md b/web/content/participants/_index.md
@@ -0,0 +1,12 @@
++++
+layout = 'single'
+title = 'Participants'
++++
+
+The following solvers have been submitted to SMT-COMP 2025 or were entered as non-competing solvers by the organizers for comparison.
+
+{{< participants >}}
+
+n Non-competing.
+
+The opening value of the NYSE Composite Index on 2025-06-30 was 20338.41, resulting in a competition seed of 2033841 + 755033430 = **757067271**.
diff --git a/web/hugo.toml b/web/hugo.toml
@@ -70,7 +70,7 @@ theme = 'smtcomp'
     pageRef = 'parallel_track'
     weight = 30
 
-# [[menu.year]]
-#     name = 'Participants'
-#     pageRef = 'participants'
-#     weight = 50
+[[menu.year]]
+    name = 'Participants'
+    pageRef = 'participants'
+    weight = 50
diff --git a/web/themes/smtcomp/assets/css/main.css b/web/themes/smtcomp/assets/css/main.css
@@ -695,13 +695,19 @@ table.participants {
 
 col.authors,
 td.authors {
-  width: 35%;
+  width: 20%;
+  white-space: normal;
+}
+
+col.seed,
+td.seed {
+  width: 7em;
   white-space: normal;
 }
 
 col.track,
 td.track {
-  width: 6em;
+  width: 5.6em;
   white-space: normal;
 }
 
@@ -710,3 +716,7 @@ td.archive {
   width: 6em;
   white-space: normal;
 }
+
+tr.noncompetitive a {
+  color: black;
+}
diff --git a/web/themes/smtcomp/layouts/partials/participant.html b/web/themes/smtcomp/layouts/partials/participant.html
@@ -1,5 +1,7 @@
-<tr>
-  <td><a href="{{ .website }}">{{ .name }}</a></td>
+<tr {{ if not .competitive }} class="noncompetitive" {{ end }}>
+  <td><a href="{{ .website }}">{{ .name }}</a>
+    {{ if not .competitive }}<sup>n</sup>{{ end }}
+  </td>
 
   <td>{{ with .tracks.SingleQuery }}X{{ end }}</td>
   <td>{{ with .tracks.Incremental }}X{{ end }}</td>
@@ -8,6 +10,7 @@
   <td>{{ with .tracks.Cloud }}X{{ end }}</td>
   <td>{{ with .tracks.Parallel }}X{{ end }}</td>
 
+  <td class="seed">{{ .seed | string }}</td>
   <td class="authors">{{ delimit .authors ",\n" }}</td>
   <td><a href="{{ .archive_url }}">Archive</a></td>
   <td><a href="{{ .system_description }}">System description</a></td>
diff --git a/web/themes/smtcomp/layouts/shortcodes/participants.html b/web/themes/smtcomp/layouts/shortcodes/participants.html
@@ -9,6 +9,7 @@
     <col class="track"> <!-- cloud -->
     <col class="track"> <!-- parallel -->
 
+    <col class="seed">
     <col class="authors">
     <col class="archive">
     <col>
@@ -24,12 +25,13 @@
       <th>Cloud Track</th>
       <th>Parallel Track</th>
 
+      <th>Seed</th>
       <th>Contributors</th>
       <th>Archive</th>
       <th>System description</th>
     </tr>
 
-    {{ range (sort $.Site.Data.participants "name" "asc") }}
+    {{ range (sort (sort $.Site.Data.participants "name" "asc") "competitive" "desc") }}
     {{ partial "participant.html" . }}
     {{ end }}
 

Original file line number	Diff line number	Diff line change
`@@ -18,5 +18,6 @@`
`18`	`18`	`"tracks": ["SingleQuery"],`
`19`	`19`	`"logics": ["LIA", "NIA"]`
`20`	`20`	`}`
`21`		`- ]`
	`21`	`+ ],`
	`22`	`+ "final" : true`
`22`	`23`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,5 @@`
`1`	`1`	`{`
`2`		`- "name": "STP-Parti-Bitwuzla-at-SMT-COMP-2025",`
	`2`	`+ "name": "STP-Parti-Bitwuzla",`
`3`	`3`	`"contributors": [`
`4`	`4`	`"Mengyu Zhao",`
`5`	`5`	`"Zhenghang Xu",`
Original file line number	Diff line number	Diff line change
`@@ -15,5 +15,6 @@`
`15`	`15`	`"seed": "19970530",`
`16`	`16`	`"participations": [`
`17`	`17`	`{ "tracks": ["Incremental"], "logics": "QF_NIA" }`
`18`		`- ]`
	`18`	`+ ],`
	`19`	`+ "final" : true`
`19`	`20`	`}`