Remove benchmark with wrong status in results

smtcomp/defs.py

@@ -1456,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__

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,18 +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.Unsat), validation_attempted=False).collect()
+            df = lf.filter(track=int(track), answer=int(defs.Answer.Unsat)).collect()
             if len(df) > 0:
-                print("[bold][red]Validation as not been attempted for all the results[/red][/bold]")
-                print(df["answer"].unique())
-                exit(1)
+                # 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()
         )
@@ -257,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)