Fix for largest contribution and all Unsat Core

data/latex-certificates/input_for_certificates.tex

@@ -2,23 +2,23 @@
 \newpage
 \MakeOnePage{Amaya}{}{}{\withtrack{NIA}{\fast}}{}{}
 \newpage
-\MakeOnePage{Bitwuzla}{\withtrack{Biggest Lead}{\inc}}{\withtrack{Bitvec}{\sat}, \withtrack{Equality\_MachineArith}{\inc,\uc}, \withtrack{FPArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{QF\_ADT\_BitVec}{\mv}, \withtrack{QF\_Bitvec}{\seq,\paral,\unsat,\fast,\inc}, \withtrack{QF\_Equality\_Bitvec}{\seq,\paral,\sat,\unsat,\inc}, \withtrack{QF\_FPArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}}{\withtrack{ABVFP}{\sat}, \withtrack{AUFBV}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{AUFBVFP}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{BVFPLRA}{\uc}, \withtrack{QF\_ABV}{\uc\textsuperscript\seq}, \withtrack{QF\_ABVFP}{\mv}, \withtrack{QF\_BVFPLRA}{\mv}, \withtrack{QF\_FPLRA}{\mv}, \withtrack{QF\_UFBV}{\fast}, \withtrack{UFBV}{\fast}}{s}{s}
+\MakeOnePage{Bitwuzla}{\withtrack{Biggest Lead}{\inc}}{\withtrack{Bitvec}{\sat}, \withtrack{Equality\_MachineArith}{\inc}, \withtrack{FPArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_ADT\_BitVec}{\mv}, \withtrack{QF\_Bitvec}{\seq,\paral,\unsat,\fast,\inc,\uc}, \withtrack{QF\_Equality\_Bitvec}{\seq,\paral,\sat,\unsat,\inc}, \withtrack{QF\_FPArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}}{\withtrack{ABVFP}{\sat}, \withtrack{AUFBV}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{AUFBVFP}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_ABV}{\uc}, \withtrack{QF\_ABVFP}{\mv}, \withtrack{QF\_BVFPLRA}{\mv}, \withtrack{QF\_FPLRA}{\mv}, \withtrack{QF\_UFBV}{\fast}, \withtrack{UFBV}{\fast}}{s}{s}
 \newpage
 \MakeOnePage{COLIBRI}{}{}{\withtrack{QF\_ABVFPLRA}{\unsat}, \withtrack{QF\_FP}{\fast}, \withtrack{QF\_FPLRA}{\unsat,\fast}}{}{s}
 \newpage
-\MakeOnePage{cvc5}{\withtrack{Biggest Lead}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{Largest Contribution}{\seq,\paral,\sat,\unsat,\fast}}{\withtrack{Arith}{\seq,\paral,\unsat,\inc}, \withtrack{Bitvec}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Equality}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{Equality\_LinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{Equality\_MachineArith}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{Equality\_NonLinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{FPArith}{\uc}, \withtrack{QF\_Datatypes}{\sat,\uc}, \withtrack{QF\_Equality\_LinearArith}{\uc\textsuperscript\paral}, \withtrack{QF\_Equality\_NonLinearArith}{\unsat,\inc,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_FPArith}{\mv}, \withtrack{QF\_LinearIntArith}{\unsat}, \withtrack{QF\_LinearRealArith}{\unsat}, \withtrack{QF\_NonLinearRealArith}{\unsat}, \withtrack{QF\_Strings}{\uc}}{\withtrack{ANIA}{\uc}, \withtrack{AUFBV}{\uc\textsuperscript\paral}, \withtrack{AUFBVDTLIA}{\uc}, \withtrack{AUFBVDTNIRA}{\uc}, \withtrack{AUFDTLIRA}{\uc\textsuperscript\seq}, \withtrack{AUFFPDTNIRA}{\uc}, \withtrack{AUFLIRA}{\uc\textsuperscript\seq}, \withtrack{AUFNIA}{\uc\textsuperscript\paral}, \withtrack{BVFPLRA}{\unsat}, \withtrack{FP}{\fast}, \withtrack{LIA}{\sat,\fast}, \withtrack{NIA}{\sat}, \withtrack{QF\_AUFLIA}{\inc,\uc\textsuperscript\seq}, \withtrack{QF\_AX}{\mv}, \withtrack{QF\_BVFP}{\inc}, \withtrack{QF\_FP}{\sat,\uc}, \withtrack{QF\_IDL}{\uc}, \withtrack{QF\_LIA}{\mv}, \withtrack{QF\_SNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFBVDT}{\seq,\paral,\unsat,\fast,\uc,\mv}, \withtrack{QF\_UFDT}{\seq,\paral,\mv}, \withtrack{QF\_UFDTLIRA}{\seq,\paral,\sat,\unsat,\fast,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_UFDTNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFFPDTNIRA}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_UFLRA}{\inc,\uc\textsuperscript\seq}, \withtrack{UFDT}{\uc\textsuperscript\seq}, \withtrack{UFDTLIA}{\uc\textsuperscript\seq}, \withtrack{UFDTNIA}{\uc\textsuperscript\seq}, \withtrack{UFFPDTNIRA}{\uc}, \withtrack{UFIDL}{\uc\textsuperscript\seq}, \withtrack{UFLRA}{\uc}, \withtrack{UFNIRA}{\uc\textsuperscript\seq}}{s}{s}
+\MakeOnePage{cvc5}{\withtrack{Biggest Lead}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{Largest Contribution}{\seq,\paral,\sat,\unsat,\fast}}{\withtrack{Arith}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Bitvec}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Equality}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{Equality\_LinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{Equality\_MachineArith}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{Equality\_NonLinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_Datatypes}{\sat,\uc}, \withtrack{QF\_Equality\_Bitvec}{\uc}, \withtrack{QF\_Equality\_NonLinearArith}{\unsat,\inc,\uc,\mv}, \withtrack{QF\_FPArith}{\mv}, \withtrack{QF\_LinearIntArith}{\unsat}, \withtrack{QF\_LinearRealArith}{\unsat}, \withtrack{QF\_NonLinearIntArith}{\uc}, \withtrack{QF\_NonLinearRealArith}{\unsat,\uc}, \withtrack{QF\_Strings}{\uc}}{\withtrack{BVFPLRA}{\unsat}, \withtrack{FP}{\fast}, \withtrack{LIA}{\sat,\fast}, \withtrack{NIA}{\sat}, \withtrack{QF\_AUFLIA}{\inc,\uc}, \withtrack{QF\_AX}{\mv}, \withtrack{QF\_BVFP}{\inc}, \withtrack{QF\_FP}{\sat,\uc}, \withtrack{QF\_IDL}{\uc}, \withtrack{QF\_LIA}{\mv}, \withtrack{QF\_SNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFBVDT}{\seq,\paral,\unsat,\fast,\mv}, \withtrack{QF\_UFDT}{\seq,\paral,\mv}, \withtrack{QF\_UFDTLIRA}{\seq,\paral,\sat,\unsat,\fast,\uc,\mv}, \withtrack{QF\_UFDTNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFFPDTNIRA}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_UFLRA}{\inc}}{s}{s}
 \newpage
 \MakeOnePage{iProver v3.9}{}{}{\withtrack{ALIA}{\paral,\unsat}, \withtrack{UF}{\fast}, \withtrack{UFNIRA}{\seq,\unsat}}{}{s}
 \newpage
-\MakeOnePage{OpenSMT}{}{\withtrack{QF\_Equality}{\mv}, \withtrack{QF\_Equality\_LinearArith}{\unsat,\mv}, \withtrack{QF\_LinearIntArith}{\seq,\paral,\mv}, \withtrack{QF\_LinearRealArith}{\seq,\paral,\sat,\inc,\mv}}{\withtrack{QF\_LIA}{\sat}, \withtrack{QF\_LRA}{\unsat,\fast}, \withtrack{QF\_UFIDL}{\seq,\paral,\sat}}{s}{s}
+\MakeOnePage{OpenSMT}{}{\withtrack{QF\_Equality}{\mv}, \withtrack{QF\_Equality\_LinearArith}{\unsat,\mv}, \withtrack{QF\_LinearIntArith}{\seq,\paral,\mv}, \withtrack{QF\_LinearRealArith}{\seq,\paral,\sat,\inc,\uc,\mv}}{\withtrack{QF\_LIA}{\sat}, \withtrack{QF\_LRA}{\unsat,\fast}, \withtrack{QF\_UF}{\uc\textsuperscript\seq}, \withtrack{QF\_UFIDL}{\seq,\paral,\sat}, \withtrack{QF\_UFLRA}{\uc}}{s}{s}
 \newpage
 \MakeOnePage{SMT-RAT}{}{\withtrack{QF\_NonLinearRealArith}{\mv}}{\withtrack{NRA}{\seq,\paral,\unsat,\fast}}{}{}
 \newpage
-\MakeOnePage{SMTInterpol}{\withtrack{Biggest Lead}{\uc,\mv}}{\withtrack{Arith}{\uc}, \withtrack{Equality}{\uc\textsuperscript\paral}, \withtrack{Equality\_LinearArith}{\uc}, \withtrack{Equality\_NonLinearArith}{\uc}, \withtrack{QF\_ADT\_LinArith}{\mv}, \withtrack{QF\_Datatypes}{\mv}, \withtrack{QF\_Equality\_LinearArith}{\seq,\paral,\sat,\inc,\uc\textsuperscript\seq}, \withtrack{QF\_Equality\_NonLinearArith}{\uc\textsuperscript\paral}, \withtrack{QF\_NonLinearIntArith}{\inc,\uc}, \withtrack{QF\_NonLinearRealArith}{\uc}}{\withtrack{ALIA}{\sat}, \withtrack{ANIA}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_ALIA}{\uc\textsuperscript\paral}, \withtrack{QF\_ANIA}{\unsat,\fast,\inc,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_AUFNIA}{\sat,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_LIA}{\unsat}, \withtrack{QF\_LIRA}{\uc\textsuperscript\paral}, \withtrack{QF\_UF}{\uc\textsuperscript\paral}, \withtrack{QF\_UFBVDT}{\sat}, \withtrack{QF\_UFDTLIA}{\unsat,\fast,\uc\textsuperscript\paral}, \withtrack{QF\_UFDTNIA}{\uc\textsuperscript\seq,\mv}, \withtrack{QF\_UFLIA}{\unsat,\mv}, \withtrack{QF\_UFNRA}{\uc\textsuperscript\seq}, \withtrack{UFIDL}{\sat}, \withtrack{UFLIA}{\sat}}{s}{s}
+\MakeOnePage{SMTInterpol}{\withtrack{Biggest Lead}{\mv}}{\withtrack{QF\_ADT\_LinArith}{\mv}, \withtrack{QF\_Datatypes}{\mv}, \withtrack{QF\_Equality\_LinearArith}{\seq,\paral,\sat,\inc}, \withtrack{QF\_LinearIntArith}{\uc}, \withtrack{QF\_NonLinearIntArith}{\inc}}{\withtrack{ALIA}{\sat,\uc}, \withtrack{ANIA}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{AUFDTLIA}{\uc}, \withtrack{QF\_ALIA}{\uc}, \withtrack{QF\_ANIA}{\unsat,\fast,\inc,\uc,\mv}, \withtrack{QF\_AUFNIA}{\sat,\uc,\mv}, \withtrack{QF\_LIA}{\unsat}, \withtrack{QF\_NIRA}{\uc}, \withtrack{QF\_UF}{\uc\textsuperscript\paral}, \withtrack{QF\_UFBVDT}{\sat}, \withtrack{QF\_UFDT}{\uc\textsuperscript\paral}, \withtrack{QF\_UFDTLIA}{\unsat,\fast,\uc}, \withtrack{QF\_UFDTNIA}{\uc,\mv}, \withtrack{QF\_UFLIA}{\unsat,\mv}, \withtrack{UFIDL}{\sat}, \withtrack{UFLIA}{\sat}}{s}{s}
 \newpage
 \MakeOnePage{STP}{}{\withtrack{QF\_Bitvec}{\sat,\mv}}{}{}{}
 \newpage
-\MakeOnePage{Yices2}{\withtrack{Largest Contribution}{\uc,\mv}}{\withtrack{Equality}{\uc\textsuperscript\seq}, \withtrack{QF\_Bitvec}{\uc}, \withtrack{QF\_Equality}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_Equality\_Bitvec}{\fast,\uc,\mv}, \withtrack{QF\_Equality\_Bitvec\_Arith}{\inc}, \withtrack{QF\_Equality\_LinearArith}{\fast}, \withtrack{QF\_Equality\_NonLinearArith}{\seq,\paral,\sat,\fast}, \withtrack{QF\_LinearIntArith}{\fast,\inc,\uc}, \withtrack{QF\_LinearRealArith}{\fast,\uc}, \withtrack{QF\_NonLinearIntArith}{\fast,\mv}, \withtrack{QF\_NonLinearRealArith}{\fast}}{\withtrack{QF\_ALIA}{\unsat}, \withtrack{QF\_AUFLIA}{\seq,\paral,\sat,\unsat}, \withtrack{QF\_AUFNIA}{\unsat}, \withtrack{QF\_IDL}{\mv}, \withtrack{QF\_LIRA}{\sat,\mv}, \withtrack{QF\_RDL}{\seq,\paral,\sat,\unsat,\mv}, \withtrack{QF\_UFLIA}{\inc,\uc\textsuperscript\seq}, \withtrack{QF\_UFLRA}{\seq,\paral,\sat,\unsat,\mv}, \withtrack{QF\_UFNRA}{\unsat,\mv}, \withtrack{UF}{\uc\textsuperscript\paral}}{s}{s}
+\MakeOnePage{Yices2}{\withtrack{Largest Contribution}{\inc,\uc,\mv}}{\withtrack{QF\_Equality}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_Equality\_Bitvec}{\fast,\mv}, \withtrack{QF\_Equality\_Bitvec\_Arith}{\inc}, \withtrack{QF\_Equality\_LinearArith}{\fast,\uc}, \withtrack{QF\_Equality\_NonLinearArith}{\seq,\paral,\sat,\fast}, \withtrack{QF\_LinearIntArith}{\fast,\inc}, \withtrack{QF\_LinearRealArith}{\fast}, \withtrack{QF\_NonLinearIntArith}{\fast,\mv}, \withtrack{QF\_NonLinearRealArith}{\fast}}{\withtrack{QF\_ALIA}{\unsat}, \withtrack{QF\_AUFBV}{\uc}, \withtrack{QF\_AUFLIA}{\seq,\paral,\sat,\unsat}, \withtrack{QF\_AUFNIA}{\unsat}, \withtrack{QF\_IDL}{\mv}, \withtrack{QF\_LIA}{\uc}, \withtrack{QF\_LIRA}{\sat,\mv}, \withtrack{QF\_RDL}{\seq,\paral,\sat,\unsat,\mv}, \withtrack{QF\_UFLIA}{\inc}, \withtrack{QF\_UFLRA}{\seq,\paral,\sat,\unsat,\mv}, \withtrack{QF\_UFNRA}{\unsat}}{s}{s}
 \newpage
 \MakeOnePage{YicesQS}{}{\withtrack{Arith}{\sat,\fast}, \withtrack{Bitvec}{\fast}}{\withtrack{LRA}{\seq,\paral,\unsat}}{s}{}
 \newpage

smtcomp/defs.py

@@ -165,7 +165,10 @@ class Answer(EnumAutoInt):
     """
     At least one wrong answer
     """
-    UnsatCoreNotValidated = "UnsatCoreNotValidated"
+    UnsatCoreInvalidated = "UnsatCoreNotValidated"
+    """
+    More solver said sat than unsat
+    """
 
 
 class Track(EnumAutoInt):
@@ -1453,8 +1456,22 @@ class Config:
             "logic": int(Logic.QF_LIA),
             "family": "20210219-Dartagnan/ConcurrencySafety-Main",
             "name": "39_rand_lock_p0_vs-O0.smt2",
-        }
+        }  # scrambler segfault (perhaps stack limit)
+    ]
+    """
+    Benchmarks to remove before selection (currently just for aws)
+    """
+
+    removed_results = [
+        {
+            "logic": int(Logic.QF_BV),
+            "family": "20230221-oisc-gurtner",
+            "name": "SLL-NESTED-8-32-sp-not-excluded.smt2",
+        }  # wrong status in SMTLIB
     ]
+    """
+    Benchmarks to remove after running the solvers. Can be used when the selection has already been done.
+    """
 
     def __init__(self, data: Path | None) -> None:
         self.id = self.__class__.__next_id__
@@ -1477,12 +1494,13 @@ def data(self) -> Path:
             raise ValueError("Configuration without data")
         return self._data
 
+    @functools.cached_property
+    def previous_years(self) -> list[int]:
+        return list(range(self.oldest_previous_results, self.current_year))
+
     @functools.cached_property
     def previous_results(self) -> list[tuple[int, Path]]:
-        return [
-            (year, self.data.joinpath(f"results-sq-{year}.json.gz"))
-            for year in range(Config.oldest_previous_results, Config.current_year)
-        ]
+        return [(year, self.data.joinpath(f"results-sq-{year}.json.gz")) for year in self.previous_years]
 
     @functools.cached_property
     def current_results(self) -> dict[Track, Path]:

smtcomp/generate_website_page.py

@@ -469,22 +469,29 @@ def aux(k: smtcomp.scoring.Kind, div: str) -> List[PodiumStepLargestContribution
         virtual = v_steps[0]
         assert virtual.name == "virtual"
         ratio = ratio_by_division[div]
+
+        def timeScore(vws_step: PodiumStep) -> float:
+            assert vws_step.correctScore <= virtual.correctScore
+            if k == smtcomp.scoring.Kind.seq:
+                v_time_score = virtual.CPUScore
+                vws_time_score = vws_step.CPUScore
+            else:
+                v_time_score = virtual.WallScore
+                vws_time_score = vws_step.WallScore
+            if vws_time_score == 0:
+                # The rules do not take into account this case
+                return ratio
+            else:
+                return ratio * (1.0 - ((v_time_score / vws_time_score)))
+
         return [
             PodiumStepLargestContribution(
-                name=step.name,
-                correctScore=ratio * (1.0 - (step.correctScore / virtual.correctScore)),
-                timeScore=ratio
-                * (
-                    1.0
-                    - (
-                        (virtual.CPUScore / step.CPUScore)
-                        if k == smtcomp.scoring.Kind.seq
-                        else (virtual.WallScore / step.WallScore)
-                    )
-                ),
+                name=vws_step.name,
+                correctScore=ratio * (1.0 - (vws_step.correctScore / virtual.correctScore)),
+                timeScore=timeScore(vws_step),
                 division=div,
             )
-            for step in vws_steps
+            for vws_step in vws_steps
         ]
 
     ld = dict(
@@ -525,7 +532,7 @@ def largest_contribution(
     # For each solver compute its corresponding best solver
     # TODO: check what is competitive solver (unsound?)
 
-    scores = scores.filter(error_score=0, sound_solver=True).filter(smtcomp.scoring.known_answer)
+    scores = scores.filter(error_score=0, sound_solver=True).filter(pl.col("correctly_solved_score") > 0)
     scores_col = scores.collect()
     total_len = len(scores_col)
     scores = scores_col.lazy()

smtcomp/main.py

@@ -205,6 +205,7 @@ def store_results(
 
     config = defs.Config(data)
     lf = pl.concat(pl.read_ipc(results / "parsed.feather").lazy() for results in lresults)
+
     benchmarks = pl.read_ipc(config.cached_non_incremental_benchmarks).lazy()
     benchmarks_inc = pl.read_ipc(config.cached_incremental_benchmarks).lazy()
     for track, dst in config.current_results.items():
@@ -221,19 +222,23 @@ def store_results(
                 print("[bold][red]Validation as not been attempted for all the results[/red][/bold]")
                 exit(1)
         if track == defs.Track.UnsatCore:
-            df = lf.filter(track=int(track), answer=int(defs.Answer.UnsatCoreNotValidated)).collect()
+            df = lf.filter(track=int(track), answer=int(defs.Answer.Unsat)).collect()
             if len(df) > 0:
+                # Tested in two phases, because validation_attempted is not always present
                 df = df.filter(validation_attempted=False)
                 if len(df) > 0:
                     print("[bold][red]Validation as not been attempted for all the results[/red][/bold]")
+                    print(df.select("logic", "solver"))
                     exit(1)
+        removed_results = pl.LazyFrame(config.removed_results)
         df = (
             add_columns(
                 lf.filter(track=int(track)).drop("logic"),
                 b.select("file", "logic", "family", "name"),
                 on=["file"],
                 defaults={"logic": -1, "family": "", "name": ""},
             )
+            .join(removed_results, on=["logic", "family", "name"], how="anti")
             .sort("file", "solver")
             .collect()
         )
@@ -258,7 +263,12 @@ def store_results(
                     for d in df.to_dicts()
                 ]
             )
-            write_cin(dst, results_track.model_dump_json(indent=1))
+            write_cin(
+                dst,
+                results_track.model_dump_json(
+                    indent=1, exclude_defaults=(track not in [defs.Track.Incremental, defs.Track.UnsatCore])
+                ),
+            )
 
 
 @app.command(rich_help_panel=benchexec_panel)

smtcomp/results.py

@@ -406,28 +406,31 @@ def parse_dir(dir: Path) -> pl.LazyFrame:
     results = add_columns(results, lf, on=["scramble_id"], defaults=defaults)
 
     ucvr = dir / "../unsat_core_validation_results" / "parsed.feather"
-    if (dir.name).endswith("unsatcore") and ucvr.is_file():
-        vr = pl.read_ipc(ucvr).lazy()
-        vr = (
-            vr.select("answer", "unsat_core", scramble_id="scramble_id_orig")
-            .group_by("scramble_id", "unsat_core")
-            .agg(
-                sat=(pl.col("answer") == int(defs.Answer.Sat)).count(),
-                unsat=(pl.col("answer") == int(defs.Answer.Unsat)).count(),
-                validation_attempted=True,
+    if (dir.name).endswith("unsatcore"):
+        if ucvr.is_file():
+            vr = pl.read_ipc(ucvr).lazy()
+            vr = (
+                vr.select("answer", "unsat_core", scramble_id="scramble_id_orig")
+                .group_by("scramble_id", "unsat_core")
+                .agg(
+                    sat=(pl.col("answer") == int(defs.Answer.Sat)).count(),
+                    unsat=(pl.col("answer") == int(defs.Answer.Unsat)).count(),
+                    validation_attempted=True,
+                )
             )
-        )
-        results = add_columns(
-            results,
-            vr,
-            on=["scramble_id", "unsat_core"],
-            defaults={"sat": 0, "unsat": 0, "validation_attempted": False},
-        )
-        results = results.with_columns(
-            answer=pl.when((pl.col("answer") == int(defs.Answer.Unsat)) & (pl.col("sat") > pl.col("unsat")))
-            .then(int(defs.Answer.UnsatCoreNotValidated))
-            .otherwise("answer")
-        ).drop("sat", "unsat", "unsat_core")
+            results = add_columns(
+                results,
+                vr,
+                on=["scramble_id", "unsat_core"],
+                defaults={"sat": 0, "unsat": 0, "validation_attempted": False},
+            )
+            results = results.with_columns(
+                answer=pl.when((pl.col("answer") == int(defs.Answer.Unsat)) & (pl.col("sat") > pl.col("unsat")))
+                .then(int(defs.Answer.UnsatCoreInvalidated))
+                .otherwise("answer")
+            ).drop("sat", "unsat", "unsat_core")
+        else:
+            results = results.with_columns(validation_attempted=False)
 
     return results
 
@@ -443,6 +446,8 @@ def helper_get_results(
 
     -1 is used when no answer is available.
 
+    The second value returned is the selection
+
     """
     if len(results) == 0:
         lf = (