diff --git a/tools/benchcomp/benchcomp/parsers/kani_perf.py b/tools/benchcomp/benchcomp/parsers/kani_perf.py
index 76a4fd90af30..4dcf00fe3c26 100755
--- a/tools/benchcomp/benchcomp/parsers/kani_perf.py
+++ b/tools/benchcomp/benchcomp/parsers/kani_perf.py
@@ -30,6 +30,28 @@ def _get_metrics():
             "pat": re.compile(r"Runtime Solver: (?P<value>[-e\d\.]+)s"),
             "parse": float,
         },
+        # CBMC solves a harness in several calls, and the number of calls is not stable across
+        # runs of the same code (https://github.com/model-checking/kani/issues/4821). Counting
+        # them, and deriving `solver_runtime_per_call` in `main`, explains a differing
+        # `solver_runtime`, which sums over all calls.
+        "solver_calls": {
+            "pat": re.compile(r"Solving with (?P<value>.+)"),
+            "parse": lambda _: 1,
+        },
+        # The size of the SAT instance CBMC hands its built-in solver. Later calls in the same
+        # harness solve that instance incrementally, one clause and variable at a time, so only
+        # the first call is recorded: it pins the instance more tightly than the VCC and step
+        # counts do, without inheriting the instability of the call count.
+        "solver_variables": {
+            "pat": re.compile(r"(?P<value>\d+) variables, \d+ clauses"),
+            "parse": int,
+            "first_only": True,
+        },
+        "solver_clauses": {
+            "pat": re.compile(r"\d+ variables, (?P<value>\d+) clauses"),
+            "parse": int,
+            "first_only": True,
+        },
         "removed_program_steps": {
             "pat": re.compile(r"slicing removed (?P<value>\d+) assignments"),
             "parse": int,
@@ -57,13 +79,17 @@ def _get_metrics():
 def get_metrics():
     metrics = dict(_get_metrics())
     for metric, info in metrics.items():
-        for field in ("pat", "parse"):
-            info.pop(field)
+        for field in ("pat", "parse", "first_only"):
+            info.pop(field, None)
 
     # This is not a metric we return; it is used to find the correct value for
     # the number_program_steps metric
     metrics.pop("removed_program_steps", None)
 
+    # Derived in `main` from `solver_runtime` and `solver_calls` rather than parsed from a line,
+    # so it has no pattern to strip.
+    metrics["solver_runtime_per_call"] = {}
+
     return metrics
 
 
@@ -90,13 +116,17 @@ def main(root_dir):
                         continue
 
                     parse = metric_info["parse"]
+                    bench_metrics = benchmarks[bench_name]["metrics"]
+                    if metric_info.get("first_only"):
+                        bench_metrics.setdefault(metric, parse(m["value"]))
+                        continue
                     try:
                         # CBMC prints out some metrics more than once, e.g.
                         # "Solver" and "decision procedure". Add those
                         # values together
-                        benchmarks[bench_name]["metrics"][metric] += parse(m["value"])
+                        bench_metrics[metric] += parse(m["value"])
                     except (KeyError, TypeError):
-                        benchmarks[bench_name]["metrics"][metric] = parse(m["value"])
+                        bench_metrics[metric] = parse(m["value"])
                     break
 
     for bench_name, bench_info in benchmarks.items():
@@ -108,6 +138,13 @@ def main(root_dir):
         except KeyError:
             pass
 
+        try:
+            calls = bench_info["metrics"]["solver_calls"]
+            runtime = bench_info["metrics"]["solver_runtime"]
+            bench_info["metrics"]["solver_runtime_per_call"] = runtime / calls
+        except (KeyError, ZeroDivisionError):
+            pass
+
     return {
         "metrics": get_metrics(),
         "benchmarks": benchmarks,
diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py
index 5700e049b8b8..8d03b77cb303 100644
--- a/tools/benchcomp/benchcomp/visualizers/__init__.py
+++ b/tools/benchcomp/benchcomp/visualizers/__init__.py
@@ -79,6 +79,23 @@ class error_on_regression:
         test: "lambda old, new: False if not old else not new"
     ```
 
+    A check may instead set `all_metrics: true`, in which case the test receives the two
+    variants' entire metric dicts rather than a single metric's values. `metric` is still
+    required, but is then only used to label the warning that the check prints; a benchmark
+    that lacks it is still passed to the test, which must handle missing metrics itself (e.g.
+    with `dict.get`):
+
+    ```
+    visualize:
+    - type: error_on_regression
+      variant_pairs:
+      - [variant_1, variant_2]
+      checks:
+      - metric: runtime
+        all_metrics: true
+        test: "lambda old, new: new['runtime'] / old['runtime'] > 1.1 and old['steps'] != new['steps']"
+    ```
+
     This says to check whether any benchmark regressed when run under variant_2
     compared to variant_1. A benchmark is considered to have regressed if the
     value of the 'runtime' metric under variant_2 is 10% higher than the value
diff --git a/tools/benchcomp/benchcomp/visualizers/utils.py b/tools/benchcomp/benchcomp/visualizers/utils.py
index bbd927034ef5..65dad05e7915 100644
--- a/tools/benchcomp/benchcomp/visualizers/utils.py
+++ b/tools/benchcomp/benchcomp/visualizers/utils.py
@@ -24,10 +24,14 @@ class SingleRegressionCheck:
 
     metric: str
     test: typing.Callable
+    all_metrics: bool
 
 
-    def __init__(self, metric, test_program):
+    def __init__(self, metric, test_program, all_metrics=False):
         self.metric = metric
+        # When set, the test receives the two variants' whole metric dicts instead of a single
+        # metric's values, so it can judge one metric in the light of the others.
+        self.all_metrics = all_metrics
         try:
             self.test = eval(test_program)
         except SyntaxError:
@@ -79,10 +83,20 @@ def __call__(self, results):
                             bench_name, self.metric, variant)
                         continue
 
-                old = bench["variants"][old_variant]["metrics"][self.metric]
-                new = bench["variants"][new_variant]["metrics"][self.metric]
-
-                if has_regressed(old, new):
+                old_metrics = bench["variants"][old_variant]["metrics"]
+                new_metrics = bench["variants"][new_variant]["metrics"]
+                if has_regressed.all_metrics:
+                    # `metric` only labels the warning here, so a benchmark that lacks it is
+                    # still judged: the test decides what the absence of a metric means.
+                    old = old_metrics.get(self.metric)
+                    new = new_metrics.get(self.metric)
+                    regressed = has_regressed(old_metrics, new_metrics)
+                else:
+                    old = old_metrics[self.metric]
+                    new = new_metrics[self.metric]
+                    regressed = has_regressed(old, new)
+
+                if regressed:
                     logging.warning(
                         "Benchmark '%s' regressed on metric '%s' (%s -> %s)",
                         bench_name, self.metric, old, new)
diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml
index d1e65b24ca2c..b33d892cc5e6 100644
--- a/tools/benchcomp/configs/perf-regression.yaml
+++ b/tools/benchcomp/configs/perf-regression.yaml
@@ -82,6 +82,13 @@ visualize:
           + "%.3f%%" % ((b["kani_new"] - b["kani_old"]) * 100 / b["kani_old"])
           + ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "")
 
+      solver_calls:
+      - column_name: diff old → new
+        text: >
+          lambda b: "" if b["kani_new"] == b["kani_old"]
+          else ("+" if b["kani_new"] > b["kani_old"] else "")
+          + str(b["kani_new"] - b["kani_old"])
+
       # For success metric, display some text if success has changed
       success:
       - column_name: change
@@ -97,7 +104,41 @@ visualize:
         # Compare the old and new variants of each benchmark. The
         # benchmark has regressed if the lambda returns true.
         test: "lambda old, new: False if not old else not new"
+
+      # Solver time on the perf suite's heavy harnesses is noisy even when nothing changed: over
+      # seven `main` runs, 910 (benchmark, run) pairs with identical VCC *and* step counts had a
+      # median old→new ratio of 0.99x but a range of 0.41x to 2.41x, and
+      # `inet::checksum::tests::differential` alone ranged 38.8s to 116.0s on the `main` side.
+      # A flat 1.5x therefore tripped on #4801, #4804 and #4820, none of which touched the
+      # harnesses involved (https://github.com/model-checking/kani/issues/4822).
+      #
+      # So the threshold depends on whether the SAT instance moved. When the VCC and step counts
+      # and the size of the first solver call's instance all match (CBMC prints that size only
+      # for its built-in solvers, so for an external solver such as kissat it is absent on both
+      # sides), the two sides are likely, not certainly, solving the same instance, and only a
+      # slowdown well past the observed noise (4x) counts: that still catches a large slowdown
+      # from, e.g., a change to the solver options Kani passes. Otherwise the original 1.5x
+      # applies. Both compare the *total* solver time, so a change that adds solver calls is
+      # caught even if each call is as fast as before; `solver_calls` and
+      # `solver_runtime_per_call` are in the results table to explain a differing total. A
+      # harness that newly needs 10s or more of solver time also counts.
+      #
+      # What this gives up: a slowdown between 1.5x and 4x on an instance of unchanged size
+      # passes. Much of the noise comes from symbol names that depend on rustc allocation
+      # order, which changes the variable order the solver sees
+      # (https://github.com/model-checking/kani/issues/4821). Fixing that, or re-running a
+      # tripped harness on both sides (https://github.com/model-checking/kani/issues/4918),
+      # would let the 4x come down.
       - metric: solver_runtime
-        test: "lambda old, new: False if new < 10 else new/old > 1.5"
+        all_metrics: true
+        test: >
+          lambda old, new: new.get("solver_runtime", 0) >= 10 and (
+            not old.get("solver_runtime")
+            or new["solver_runtime"] / old["solver_runtime"] > (
+              4 if all(old.get(k) == new.get(k) for k in (
+                "number_vccs", "number_program_steps", "solver_variables", "solver_clauses"))
+              else 1.5))
+
+      # Symex time is deterministic given the formula, so it keeps the simple rule.
       - metric: symex_runtime
         test: "lambda old, new: False if new < 10 else new/old > 1.5"
diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py
index 00256aa891ab..3173b28c3659 100644
--- a/tools/benchcomp/test/test_regression.py
+++ b/tools/benchcomp/test/test_regression.py
@@ -228,6 +228,68 @@ def test_error_on_regression_two_benchmarks_one_failed(self):
                 run_bc.proc.returncode, 1, msg=run_bc.stderr)
 
 
+    def test_error_on_regression_all_metrics(self):
+        """Ensure that a check with `all_metrics` judges one metric in the light of another: a
+        slowdown only counts when the `steps` metric moved too."""
+
+        def config(new_steps):
+            return {
+                "variants": {
+                    "old": {
+                        "config": {
+                            "directory": str(self.tmp),
+                            "command_line":
+                                "mkdir bench_1 && "
+                                "echo 10 > bench_1/runtime && "
+                                "echo 100 > bench_1/steps"
+                        },
+                    },
+                    "new": {
+                        "config": {
+                            "directory": str(self.tmp),
+                            "command_line":
+                                "mkdir bench_1 && "
+                                "echo 30 > bench_1/runtime && "
+                                f"echo {new_steps} > bench_1/steps"
+                        }
+                    }
+                },
+                "run": {
+                    "suites": {
+                        "suite_1": {
+                            "parser": {"module": "test_file_to_metric"},
+                            "variants": ["old", "new"]
+                        }
+                    }
+                },
+                "visualize": [{
+                    "type": "error_on_regression",
+                    "variant_pairs": [["old", "new"]],
+                    "checks": [{
+                        "metric": "runtime",
+                        "all_metrics": True,
+                        "test":
+                            "lambda old, new: old['steps'] != new['steps'] "
+                            "and new['runtime'] / old['runtime'] > 1.5"
+                    }]
+                }]
+            }
+
+        # Three times slower, but on the same number of steps: not attributable, so no error.
+        with tempfile.TemporaryDirectory() as tmp:
+            self.tmp = tmp
+            run_bc = Benchcomp(config(new_steps=100))
+            run_bc()
+            self.assertEqual(run_bc.proc.returncode, 0, msg=run_bc.stderr)
+
+        # Three times slower on a different number of steps: a regression.
+        with tempfile.TemporaryDirectory() as tmp:
+            self.tmp = tmp
+            run_bc = Benchcomp(config(new_steps=500))
+            run_bc()
+            self.assertEqual(run_bc.proc.returncode, 1, msg=run_bc.stderr)
+
+
     def test_error_on_regression_visualization_success_regressed(self):
         """Ensure that benchcomp terminates with exit of 1 when the "error_on_regression" visualization is configured and one of the benchmarks' success metric has regressed"""
 
diff --git a/tools/benchcomp/test/unit/test_kani_perf_parser.py b/tools/benchcomp/test/unit/test_kani_perf_parser.py
new file mode 100644
index 000000000000..1ce44b0c687c
--- /dev/null
+++ b/tools/benchcomp/test/unit/test_kani_perf_parser.py
@@ -0,0 +1,77 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+
+import pathlib
+import tempfile
+import textwrap
+import unittest
+
+import benchcomp.parsers.kani_perf as kani_perf
+
+
+class TestKaniPerfParser(unittest.TestCase):
+    def parse(self, expected_out):
+        """Run the parser over a single fake `expected.out` and return its benchmarks"""
+
+        with tempfile.TemporaryDirectory() as tmp:
+            out_dir = pathlib.Path(tmp) / "build" / "tests" / "perf" / "demo" / "expected"
+            out_dir.mkdir(parents=True)
+            (out_dir / "expected.out").write_text(textwrap.dedent(expected_out))
+            return kani_perf.main(pathlib.Path(tmp))["benchmarks"]
+
+    def test_solver_calls_are_counted(self):
+        """CBMC solves a harness in several calls; count them and average the time over them.
+
+        `solver_runtime` sums a number of calls that is not stable across runs of the same code
+        (https://github.com/model-checking/kani/issues/4821), so the per-call time is what two
+        runs can be compared on.
+        """
+
+        benchmarks = self.parse("""\
+            Checking harness demo::check...
+            Running propositional reduction
+            Solving with CaDiCaL 3.0.0
+            20705 variables, 30763 clauses
+            Runtime Solver: 2.0s
+            Running propositional reduction
+            Solving with CaDiCaL 3.0.0
+            20706 variables, 30764 clauses
+            Runtime Solver: 4.0s
+            size of program expression: 100 steps
+            slicing removed 10 assignments
+            Generated 20 VCC(s), 7 remaining after simplification
+            Runtime Symex: 1.5s
+            Verification Time: 8.0s
+            VERIFICATION:- SUCCESSFUL
+            """)
+
+        metrics = benchmarks["demo/demo::check"]["metrics"]
+        self.assertEqual(metrics["solver_calls"], 2)
+        self.assertEqual(metrics["solver_runtime"], 6.0)
+        self.assertEqual(metrics["solver_runtime_per_call"], 3.0)
+        # The instance size is the first call's: later calls extend it incrementally.
+        self.assertEqual(metrics["solver_variables"], 20705)
+        self.assertEqual(metrics["solver_clauses"], 30763)
+        # unchanged by this addition
+        self.assertEqual(metrics["number_program_steps"], 90)
+        self.assertEqual(metrics["number_vccs"], 7)
+        self.assertTrue(metrics["success"])
+
+    def test_harness_without_solver_output(self):
+        """A harness whose properties are all decided before solving has no solver metrics"""
+
+        benchmarks = self.parse("""\
+            Checking harness demo::check...
+            size of program expression: 10 steps
+            slicing removed 2 assignments
+            Generated 4 VCC(s), 0 remaining after simplification
+            Runtime Symex: 0.1s
+            Verification Time: 0.2s
+            VERIFICATION:- SUCCESSFUL
+            """)
+
+        metrics = benchmarks["demo/demo::check"]["metrics"]
+        self.assertNotIn("solver_calls", metrics)
+        self.assertNotIn("solver_runtime_per_call", metrics)
+        self.assertNotIn("solver_variables", metrics)
diff --git a/tools/benchcomp/test/unit/test_perf_regression_config.py b/tools/benchcomp/test/unit/test_perf_regression_config.py
new file mode 100644
index 000000000000..68e1b3053abf
--- /dev/null
+++ b/tools/benchcomp/test/unit/test_perf_regression_config.py
@@ -0,0 +1,117 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+
+import pathlib
+import unittest
+
+import yaml
+
+import benchcomp.visualizers.utils as utils
+
+
+CONFIG = pathlib.Path(__file__).parents[2] / "configs" / "perf-regression.yaml"
+
+
+def solver_runtime_check():
+    """The `solver_runtime` check exactly as CI runs it"""
+
+    with open(CONFIG) as handle:
+        config = yaml.safe_load(handle)
+    for viz in config["visualize"]:
+        if viz["type"] != "error_on_regression":
+            continue
+        for check in viz["checks"]:
+            if check["metric"] == "solver_runtime":
+                return utils.SingleRegressionCheck(
+                    check["metric"], check["test"], check.get("all_metrics", False))
+    raise AssertionError("no solver_runtime check in perf-regression.yaml")
+
+
+def metrics(solver_runtime, solver_calls=2, **overrides):
+    result = {
+        "number_vccs": 2399,
+        "number_program_steps": 58765,
+        "solver_variables": 20705,
+        "solver_clauses": 30763,
+        "solver_runtime": solver_runtime,
+        "solver_calls": solver_calls,
+        "solver_runtime_per_call": solver_runtime / solver_calls,
+    }
+    result.update(overrides)
+    return result
+
+
+class TestSolverRuntimeCheck(unittest.TestCase):
+    def setUp(self):
+        self.regressed = solver_runtime_check()
+
+    def test_same_instance_noise_is_tolerated(self):
+        """The widest same-instance spread seen on `main` (2.41x) must not fail a PR"""
+
+        self.assertFalse(self.regressed(metrics(11.2), metrics(11.2 * 2.41)))
+
+    def test_same_instance_large_slowdown_is_caught(self):
+        """Identical counts do not exempt a harness: e.g. a solver-option change"""
+
+        self.assertTrue(self.regressed(metrics(12.0), metrics(12.0 * 4.5)))
+
+    def test_more_calls_at_the_same_per_call_time_is_caught(self):
+        """The total is compared, so extra calls count even if each one is no slower"""
+
+        self.assertTrue(self.regressed(
+            metrics(12.0, solver_calls=2), metrics(60.0, solver_calls=10)))
+
+    def test_changed_instance_uses_the_strict_threshold(self):
+        for key, value in (("number_vccs", 2400), ("number_program_steps", 58766),
+                           ("solver_variables", 20706), ("solver_clauses", 30764)):
+            with self.subTest(changed=key):
+                self.assertTrue(self.regressed(
+                    metrics(12.0), metrics(12.0 * 1.6, **{key: value})))
+                self.assertFalse(self.regressed(
+                    metrics(12.0), metrics(12.0 * 1.4, **{key: value})))
+
+    def test_short_runs_are_ignored(self):
+        self.assertFalse(self.regressed(
+            metrics(1.0, number_vccs=1), metrics(9.0, number_vccs=2)))
+
+    def test_harness_without_solver_output(self):
+        """All properties decided before solving: no solver metrics, no regression, no crash"""
+
+        bare = {"number_vccs": 0, "number_program_steps": 10}
+        self.assertFalse(self.regressed(bare, bare))
+        self.assertFalse(self.regressed(metrics(30.0), bare))
+        self.assertFalse(self.regressed(bare, metrics(9.0)))
+
+    def test_newly_needing_the_solver_is_caught(self):
+        """A harness that `main` decides without the solver but the change sends to it for 10s
+        or more has regressed, although there is no old solver time to take a ratio of"""
+
+        bare = {"number_vccs": 0, "number_program_steps": 10}
+        self.assertTrue(self.regressed(bare, metrics(30.0)))
+        self.assertTrue(self.regressed(metrics(0.0), metrics(30.0)))
+
+
+class TestAllMetricsChecker(unittest.TestCase):
+    def test_missing_label_metric_is_not_a_key_error(self):
+        """With `all_metrics`, `metric` only labels the warning, so a benchmark that lacks it is
+        still judged rather than aborting the whole check"""
+
+        results = {"benchmarks": {
+            "no_solver": {"variants": {
+                "old": {"metrics": {"number_vccs": 0}},
+                "new": {"metrics": {"number_vccs": 0}},
+            }},
+            "slow": {"variants": {
+                "old": {"metrics": {"solver_runtime": 10.0}},
+                "new": {"metrics": {"solver_runtime": 50.0}},
+            }},
+        }}
+        checker = utils.AnyBenchmarkRegressedChecker(
+            [["old", "new"]], "solver_runtime",
+            "lambda old, new: new.get('solver_runtime', 0) > 2 * old.get('solver_runtime', 0)",
+            all_metrics=True)
+        with self.assertLogs(level="WARNING") as logs:
+            self.assertTrue(checker(results))
+        self.assertEqual(len(logs.output), 1)
+        self.assertIn("'slow'", logs.output[0])