diff --git a/docs/TESTCOMP-CHECKLIST.md b/docs/TESTCOMP-CHECKLIST.md
index 51cb3db2e..2d75a661b 100644
--- a/docs/TESTCOMP-CHECKLIST.md
+++ b/docs/TESTCOMP-CHECKLIST.md
@@ -24,7 +24,7 @@ evidência que sustenta o estado declarado.
 | **H1.1** Emissor de test suite XML | ✅ | `modules/frontend/test_suite/`. `--generate-test-suite` emite `metadata.xml` + `testcase-N.xml` no formato de intercâmbio. 13 testes unitários + 12 asserções de integração. **Custo real muito abaixo das 2 pw estimadas**: o runtime já registrava os valores em ordem de consumo, faltava só serializar |
 | **H1.2** Conversor ktest→XML | ✅ | **Colapsou dentro do H1.1.** O log é escrito pelo binário instrumentado em tempo de execução, então já carrega os valores concretos do KLEE. Não precisou de conversor separado |
 | **H1.3** Vetores de entrada por caminho | ✅ | **Resolvido por outro caminho que o planejado.** O KLEE já grava um `.ktest` por caminho explorado, com os objetos simbólicos em ordem de consumo; `ktest_reader.cpp` os lê. A alternativa (o runtime gravar um log por estado) foi **medida e descartada**: levou um run de 1s/`FALSE` para 100s/`SUCCEEDED` errado, porque cada escrita é chamada externa que o KLEE executa concretamente. 16 testes unitários fixam o parse contra bytes montados à mão |
-| **H1.4** Empacotamento BenchExec / fm-tools | ✅ | `utils/moduleBenchExec/map2check_testcomp.py` (`BaseTool2`) + `utils/map2check-testcomp-wrapper.py`, ambos no zip de release. 15 asserções contra o benchexec real em `tests/integration/test_benchexec_toolinfo.py`. **Falta:** registrar em `fm-tools` (fora deste repositório). O `map2check.py` SV-COMP segue em `BaseTool` 1.x — obsoleto mas ainda presente no benchexec 3.35, então não está morto |
+| **H1.4** Empacotamento BenchExec / fm-tools | ✅ | Um módulo tool-info só, o `map2check.py` do BenchExec (cópia em `utils/moduleBenchExec/map2check.py`), estendido em sosy-lab/benchexec#1352; um wrapper só, `utils/map2check-wrapper.py`, que escolhe verificação ou geração de testes pelo arquivo de propriedade. 24 asserções contra o benchexec real em `tests/integration/test_benchexec_toolinfo.py`. Registro em fm-tools: !1245, arquivo em DOI 10.5281/zenodo.23672409 |
 | **H1.5** E2E no CI com TestCov | ✅ | Job `Test-Comp Validation (TestCov)`, 6/6 contra manifesto medido. Ver `tests/testcomp/` |
 
 ## H2 — Eficácia
diff --git a/tests/integration/test_benchexec_toolinfo.py b/tests/integration/test_benchexec_toolinfo.py
index 6a4472450..27177454c 100644
--- a/tests/integration/test_benchexec_toolinfo.py
+++ b/tests/integration/test_benchexec_toolinfo.py
@@ -172,8 +172,8 @@ def main():
 
     silent_tool, silent_executable = fake_tool("")
     silent_cmd = silent_tool.cmdline(silent_executable, [], task, limits)
-    check("a wrapper that does not tell its version gets no new options",
-          "--budget" not in silent_cmd, silent_cmd)
+    check("a wrapper that does not tell its version is taken as the current one",
+          "--budget" in silent_cmd, silent_cmd)
 
     # --- determine_result ----------------------------------------------------
     check("DONE as the last line is DONE",
diff --git a/utils/moduleBenchExec/map2check.py b/utils/moduleBenchExec/map2check.py
index c5a52456f..322620918 100644
--- a/utils/moduleBenchExec/map2check.py
+++ b/utils/moduleBenchExec/map2check.py
@@ -5,7 +5,6 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import functools
 import os
 import re
 
@@ -44,7 +43,11 @@ def executable(self, tool_locator):
             self._version = 6
         except ToolNotFoundException:
             executable = tool_locator.find_executable("map2check-wrapper.py")
-            self._version = 7
+            # The Python wrapper (Map2Check 7 and later) reports the version,
+            # e.g., "v9.0.0-Songbirds:2026-10-13". If it does not, assume the
+            # current version.
+            match = re.match(r"v?(\d+)\.", self._version_from_tool(executable))
+            self._version = int(match.group(1)) if match else 9
 
         return executable
 
@@ -87,7 +90,7 @@ def cmdline(self, executable, options, task, rlimits):
             )
         elif self._version > 6:
             cmd = [executable] + options + ["-p", task.property_file]
-            if _major_version(executable) >= 9:
+            if self._version >= 9:
                 data_model = get_data_model_from_task(
                     task, {ILP32: "ILP32", LP64: "LP64"}
                 )
@@ -149,11 +152,3 @@ def determine_result(self, run):
                 status = "ERROR"
 
         return status
-
-
-@functools.lru_cache
-def _major_version(executable):
-    """The major version of Map2Check, or 0 if the wrapper does not tell."""
-    version = Tool._version_from_tool(executable)
-    match = re.match(r"v?(\d+)\.", version)
-    return int(match.group(1)) if match else 0