2026 execution

README.md

@@ -116,7 +116,7 @@ Which outputs:
 The final solvers submitted during the smtcomp 2023 can be used:
 
 ```
-smtcomp convert-csv tests/solvers_divisions_final.csv ../tmp/submissions
+smtcomp convert-csv tests/solvers_divisions_final.csv ../execution/submissions
 ```
 
 The generated files can be visualized using:
@@ -125,22 +125,22 @@ The generated files can be visualized using:
 smtcomp show ../tmp/submissions/YicesQS.json
 ```
 
-The solver downloaded using:
+All solvers are downloaded and unpacked using:
 
 ```
-smtcomp download-archive submissions/*.json ../tmp/execution
+smtcomp download-archive submissions/*.json ../execution
 ```
 
-Trivial tests benchmarks generated with:
+Trivial tests benchmarks can be generated with:
 
 ```
-smtcomp generate-trivial-benchmarks ../tmp/execution/benchmarks
+smtcomp generate-trivial-benchmarks ../execution/benchmarks
 ```
 
-The benchexec execution environment generated using:
+The benchexec execution environment is generated using:
 
 ```
-smtcomp prepare-execution ../tmp/execution
+smtcomp prepare-execution ../execution
 ```
 
 The benchmarks can be selected by running
@@ -183,7 +183,7 @@ We will suppose that the results are locally available in directory `tmp/final_r
 For example using rsync if `sosy` is configured in `.ssh/config`:
 
 ```
-rsync sosy:/localhome/smt-comp/final_results -ra tmp/ --progress --exclude="*.logfiles"
+rsync sosy:/localhome/smt-comp/results -ra .. --progress --exclude="*.logfiles"
 ```
 
 The `original_id.csv` file generated at the same time that the scrambled benchmarks is needed in the results directory (even if we can recompute it, we use this one for safety):
@@ -195,19 +195,19 @@ scp sosy:/localhome/smt-comp/execution/benchmarks/files/original_id.csv tmp/fina
 In order to allow looking at the results incrementally, the first step is to translate each `.xml` into a faster `.feather` file. The translation is done only for `.xml` without a corresponding `.feather` file.
 
 ```
-smtcomp convert-benchexec-results tmp/final_results
+smtcomp convert-benchexec-results ../results
 ```
 
 Information on missing results can be obtained using:
 
 ```
-smtcomp stats-of-benchexec-results data tmp/final_results SingleQuery
+smtcomp stats-of-benchexec-results data ../results SingleQuery
 ```
 
 Computation of the scores can be obtained for the different way (parallel, sequential, sat, unsat, twenty-four seconds):
 
 ```
-smtcomp show-scores data tmp/final_results/ [par|seq|sat|unsat|24]
+smtcomp show-scores data SingleQuery ../results/ [par|seq|sat|unsat|24]
 ```
 
 Once all the results are available, they can be stored in `data/results-sq-{year}.json.gz`:
@@ -224,7 +224,11 @@ As usual the `.feather` cache need to be computed (`--only-current` create only
 smtcomp create-cache data --only-current
 ```
 
-Now the `tmp/final_results` directory is not needed anymore, since it will look into `data` for the current year results.
+Now the `../results` directory is not needed anymore, since it will look into `data` for the current year results. The `show-scores` command can be called without the results file to show the results from the stored data:
+
+```
+smtcomp show-scores data SingleQuery [par|seq|sat|unsat|24]
+```
 
 # Model Validation
 

pyproject.toml

@@ -79,7 +79,9 @@ ignore_missing_imports = true
 target-version = "py37"
 line-length = 120
 fix = true
-lint.select = [
+
+[tool.ruff.lint]
+select = [
     # flake8-2020
     "YTT",
     # flake8-bandit
@@ -112,7 +114,7 @@ lint.select = [
     "TRY",
 ]
 
-lint.ignore = [
+ignore = [
     # LineTooLong
     "E501",
     # DoNotAssignLambda

smtcomp/defs.py

@@ -1465,6 +1465,8 @@ class Config:
     unsatcore_validation_cpuCores = 4
     min_used_benchmarks = 300
     ratio_of_used_benchmarks = 0.5
+    large_logic_threshold = 1000
+    large_logic_used_ratio = 0.1
     use_previous_results_for_status = False
     """
     Complete the status given in the benchmarks using previous results

smtcomp/results.py

@@ -107,12 +107,16 @@ def parse_result(s: str) -> defs.Answer:
         return defs.Answer.Incremental
     if s.startswith("OUT OF MEMORY") or s.startswith("KILLED BY SIGNAL 9"):
         return defs.Answer.OOM
+    if s.startswith("ERROR"):
+        return defs.Answer.Unknown
     match s:
         case "false":
             return defs.Answer.Unsat
         case "true":
             return defs.Answer.Sat
-        case "unknown" | "ERROR":
+        case "WRONG":
+            return defs.Answer.IncrementalError
+        case "unknown":
             return defs.Answer.Unknown
         case "OUT OF MEMORY" | "OUT OF JAVA MEMORY" | "KILLED BY SIGNAL 9":
             return defs.Answer.OOM
@@ -345,7 +349,7 @@ def convert(a: Run) -> Dict[str, Any]:
         return d
 
     # compute the list eagerly to avoid problems with 'infer_schema_length'
-    lf = pl.LazyFrame(list(map(convert, r.runs)))
+    lf = pl.LazyFrame(list(map(convert, r.runs)), schema_overrides={"unsat_core": pl.List(pl.Int64)})
     return lf.with_columns(solver=pl.lit(r.runid.solver), participation=r.runid.participation, track=int(r.runid.track))
 
 
@@ -478,6 +482,7 @@ def helper_get_results(config: defs.Config, results: List[Path], track: defs.Tra
         lf = pl.concat(pl.read_ipc(p / "parsed.feather").lazy() for p in results)
         lf = lf.drop("logic", "participation")  # Hack for participation 0 bug move "participation" to on= for 2025,
         lf = lf.drop("benchmark_yml", "unsat_core")
+        lf = lf.filter(track=int(track))
 
     if False:
         selection = smtcomp.selection.helper(config, track).drop("result")
@@ -537,7 +542,9 @@ def helper_get_results(config: defs.Config, results: List[Path], track: defs.Tra
     defaults["walltime_s"] = 0
     defaults["answer"] = -1
 
-    selected = intersect(selection, smtcomp.selection.solver_competing_logics(config), on=["logic", "track"])
+    selected = intersect(
+        selection, smtcomp.selection.solver_competing_logics(config, only_competitive=False), on=["logic", "track"]
+    )
 
     selected = add_columns(
         selected,

smtcomp/scramble_benchmarks.py

@@ -87,7 +87,7 @@ def scramble_file(fdict: dict, incremental: bool, srcdir: Path, dstdir: Path, ar
     mangled_name = "_".join(
         [str(fdict["file"]), str(defs.Logic.of_int(fdict["logic"])), fdict["family"].replace("/", "__"), fdict["name"]]
     )
-    yaml_dst = dstdir.joinpath(mangled_name).with_suffix(".yml")
+    yaml_dst = dstdir.joinpath(mangled_name[:150]).with_suffix(".yml")
 
     generate_benchmark_yml(yaml_dst, scrambled_path, expected, orig_path.relative_to(srcdir))
 

smtcomp/selection.py

@@ -100,10 +100,10 @@ def add_trivial_run_info(benchmarks: pl.LazyFrame, previous_results: pl.LazyFram
 
 
 def track_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config, target_track: SimpleTrack) -> pl.LazyFrame:
-    used_logics = defs.logic_used_for_track(target_track)
+    used_logics = competitive_logics(config, target_track).filter(competitive=True).drop("competitive")
 
-    # Keep only logics used by the track
-    b = benchmarks_with_info.filter(c_logic.is_in(set(map(int, used_logics))))
+    # Keep only benchmarks used by the competitive logics
+    b = intersect(benchmarks_with_info, used_logics, on=["logic"])
 
     # Specific track filter
     match target_track:
@@ -134,7 +134,17 @@ def track_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config, tar
     sample_size = pl.min_horizontal(
         c_all_len,
         pl.max_horizontal(
-            config.min_used_benchmarks, (c_all_len * config.ratio_of_used_benchmarks).floor().cast(pl.UInt32)
+            config.min_used_benchmarks,  ## ensures cases (a) and (b) of rules
+            pl.when(c_all_len <= config.large_logic_threshold)
+            # case (c) of rules
+            .then(c_all_len * config.ratio_of_used_benchmarks)
+            # case (d) of rules
+            .otherwise(
+                config.large_logic_threshold * config.ratio_of_used_benchmarks
+                + (c_all_len - config.large_logic_threshold) * config.large_logic_used_ratio
+            )
+            .floor()
+            .cast(pl.UInt32),
         ),
     )
     new_sample_size = pl.min_horizontal(sample_size, c_new_len).cast(pl.UInt32)
@@ -233,27 +243,31 @@ def helper(config: defs.Config, track: defs.Track) -> pl.LazyFrame:
     return selected
 
 
-def solver_competing_logics(config: defs.Config) -> pl.LazyFrame:
+def solver_competing_logics(
+    config: defs.Config, target_track: Optional[defs.Track] = None, only_competitive: bool = True
+) -> pl.LazyFrame:
     """
     returned columns solver, track, logic
     """
     l = (
         (s.name, int(track), int(logic), p_id)
         for s in config.submissions
+        if not only_competitive or s.competitive
         for p_id, p in enumerate(s.participations.root)
         for (track, logics) in p.get_logics_by_track().items()
+        if target_track is None or target_track == track
         for logic in logics
     )
     return pl.LazyFrame(
         l, schema={"solver": pl.String, "track": pl.Int32, "logic": pl.Int64, "participation": pl.Int32}
     )
 
 
-def competitive_logics(config: defs.Config) -> pl.LazyFrame:
+def competitive_logics(config: defs.Config, track: Optional[defs.Track] = None) -> pl.LazyFrame:
     """
     returned columns track, logic, competitive:bool
     """
-    return solver_competing_logics(config).group_by("track", "logic").agg(competitive=(pl.len() > 1))
+    return solver_competing_logics(config, track).group_by("track", "logic").agg(competitive=(pl.len() > 1))
 
 
 @functools.cache

submissions/Bitwuzla-SPFD-at-SMT-COMP-2026-base.json

@@ -1,5 +1,5 @@
 {
-  "name": "Bitwuzla-0-9-1",
+  "name": "Bitwuzla-SPFD-base",
   "archive": {
     "url": "https://zenodo.org/records/20637194/files/Bitwuzla-SPFD-at-SMT-COMP-2026.zip"
   },