SMT-COMP · martinjonas · Jul 4, 2025 · Jul 4, 2025 · Jul 4, 2025 · Jul 4, 2025
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/.../STP-Parti-Bitwuzla-at-SMT-COMP-2025.json → submissions/STP-Parti-Bitwuzla.json b/.../STP-Parti-Bitwuzla-at-SMT-COMP-2025.json → 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 <[email protected]>"],
     "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-base.json → submissions/Z3-Owl-base.json b/submissions/Z3-base.json → 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/...sions/Z3-Parti-Z3pp-at-SMT-COMP-2025.json → submissions/Z3-Parti-Z3pp.json b/...sions/Z3-Parti-Z3pp-at-SMT-COMP-2025.json → 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/z3siri-base.json → submissions/z3-siri-base.json b/submissions/z3siri-base.json → 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 change
@@ Expand Up / @@ -24,5 +24,6 @@ @@
                     "QF_BVFP"
                 ]
             }
-        ]
+        ],
+        "final" : true
     }