diff --git a/certora_autosetup/build_systems/config_files.py b/certora_autosetup/build_systems/config_files.py
new file mode 100644
index 00000000..44eab080
--- /dev/null
+++ b/certora_autosetup/build_systems/config_files.py
@@ -0,0 +1,19 @@
+"""The filenames each build system anchors a project on.
+
+A directory holding one of these is a project root, which is all some callers need to know:
+``utils/remappings._projects_under`` recognises the other projects under a run root without
+knowing what to do with any of them. That module is imported by the managers themselves, so
+it cannot import them back — hence a leaf module both sides read the names from, rather than
+a second copy of the list.
+"""
+
+FOUNDRY_CONFIG_FILENAMES = ("foundry.toml",)
+
+HARDHAT_CONFIG_FILENAMES = ("hardhat.config.js", "hardhat.config.ts")
+
+# `truffle.js` is the v4 spelling, `truffle-config.js` everything since.
+TRUFFLE_CONFIG_FILENAMES = ("truffle-config.js", "truffle.js")
+
+BUILD_CONFIG_FILENAMES = (
+    FOUNDRY_CONFIG_FILENAMES + HARDHAT_CONFIG_FILENAMES + TRUFFLE_CONFIG_FILENAMES
+)
diff --git a/certora_autosetup/build_systems/foundry.py b/certora_autosetup/build_systems/foundry.py
index d712a5ff..be2e59f4 100644
--- a/certora_autosetup/build_systems/foundry.py
+++ b/certora_autosetup/build_systems/foundry.py
@@ -20,6 +20,7 @@
     import tomli as tomllib
 
 from certora_autosetup.build_systems.base import BuildSystemConfig
+from certora_autosetup.build_systems.config_files import FOUNDRY_CONFIG_FILENAMES
 from certora_autosetup.build_systems.manager import BuildSystemManager
 from certora_autosetup.utils.logger import logger
 from certora_autosetup.utils.remappings import build_packages_from_remapping_sources
@@ -137,7 +138,7 @@ def __init__(self, project_root: Path, scope, run_root: Optional[Path] = None):
 
     def get_config_filenames(self) -> List[str]:
         """Return list of config filenames to search for."""
-        return ["foundry.toml"]
+        return list(FOUNDRY_CONFIG_FILENAMES)
 
     def parse_config(self, config_file: Path, profile: str | None = None) -> FoundryConfig:
         """
diff --git a/certora_autosetup/build_systems/hardhat.py b/certora_autosetup/build_systems/hardhat.py
index 8c23149a..6fc4990b 100644
--- a/certora_autosetup/build_systems/hardhat.py
+++ b/certora_autosetup/build_systems/hardhat.py
@@ -13,6 +13,7 @@
 from dataclasses import dataclass
 
 from certora_autosetup.build_systems.base import BuildSystemConfig
+from certora_autosetup.build_systems.config_files import HARDHAT_CONFIG_FILENAMES
 from certora_autosetup.build_systems.manager import BuildSystemManager
 
 
@@ -91,7 +92,7 @@ def __init__(self, project_root: Path, scope, run_root: Optional[Path] = None):
 
     def get_config_filenames(self) -> List[str]:
         """Return list of config filenames to search for."""
-        return ["hardhat.config.js", "hardhat.config.ts"]
+        return list(HARDHAT_CONFIG_FILENAMES)
 
     def parse_config(self, config_file: Path, profile: str | None = None) -> HardhatConfig:
         """
diff --git a/certora_autosetup/build_systems/truffle.py b/certora_autosetup/build_systems/truffle.py
index 61ecd203..c66fb801 100644
--- a/certora_autosetup/build_systems/truffle.py
+++ b/certora_autosetup/build_systems/truffle.py
@@ -17,6 +17,7 @@
 from packaging.version import InvalidVersion, Version
 
 from certora_autosetup.build_systems.base import BuildSystemConfig
+from certora_autosetup.build_systems.config_files import TRUFFLE_CONFIG_FILENAMES
 from certora_autosetup.build_systems.manager import BuildSystemManager
 from certora_autosetup.utils.remappings import build_packages_from_remapping_sources
 
@@ -88,7 +89,7 @@ def __init__(self, project_root: Path, scope, run_root: Optional[Path] = None):
 
     def get_config_filenames(self) -> List[str]:
         """Return list of config filenames to search for."""
-        return ["truffle-config.js", "truffle.js"]
+        return list(TRUFFLE_CONFIG_FILENAMES)
 
     def get_default_artifact_dir(self) -> str:
         """Return default artifact directory name."""
diff --git a/certora_autosetup/utils/compilation_workarounds.py b/certora_autosetup/utils/compilation_workarounds.py
index 14653899..2444f6be 100644
--- a/certora_autosetup/utils/compilation_workarounds.py
+++ b/certora_autosetup/utils/compilation_workarounds.py
@@ -66,6 +66,12 @@ class UnsatisfiableSolcPinError(Exception):
     satisfies its pragma, so no substitution can make the project compile."""
 
 
+class ConflictingPragmaError(Exception):
+    """Raised when two files in one contract's compilation unit declare pragmas no single
+    compiler satisfies. ``compiler_map`` is keyed by contract, so no entry in it can give the
+    two files different compilers."""
+
+
 # The contract name is quoted by solc, so it survives the hard wrap that
 # ``_normalize_ws`` folds away; the source location that follows is optional
 # because only the diagnostic itself is guaranteed to be in the output.
@@ -83,6 +89,23 @@ class BlockedSolcPin:
     pragma_spec: str
 
 
+@dataclass(frozen=True)
+class PragmaReading:
+    """One compiler version a contract was reported to need, and the pragma it was read off.
+
+    ``file_path`` is the file that was being compiled and ``source_path`` the file solc
+    attributed the pragma to — the compilation unit spans several files, so the pragma often
+    comes from one the compiled file imports. ``source_path`` is what tells two readings of the
+    same contract apart, ``compiler_map`` being keyed by contract alone. It is None when the
+    diagnostic carried no source location.
+    """
+
+    version: str
+    file_path: str
+    source_path: Optional[str]
+    pragma_spec: str
+
+
 @dataclass(frozen=True)
 class SolcFallbackPlan:
     """Which installed compiler, if any, stands in for ``failed_solc`` at each
@@ -182,6 +205,44 @@ def _find_compiling_path_before(lines: List[str], idx: int, max_lookback: Option
     return None
 
 
+def _diagnostic_source_path(output: str, lines: List[str], start: int, idx: int) -> Optional[str]:
+    """The file solc attributes the diagnostic starting at ``output[start]`` to, or None.
+
+    solc writes the location in one of two shapes and this reads both: the short one prefixes
+    the diagnostic on its own line (``<path>:<line>:<col>: ParserError: …``), the long one puts
+    it on an ``-->`` line under it and hard-wraps a long path across the lines that follow.
+
+    ``lines`` is ``output`` split on newlines and ``idx`` the index of the line ``start`` falls
+    on, both passed in because the caller already has them.
+    """
+    line_start = output.rfind("\n", 0, start) + 1
+    prefixed = re.match(r"^\s*(.+?):\d+:\d+:\s*$", output[line_start:start])
+    if prefixed:
+        return prefixed.group(1).strip()
+
+    for j in range(idx + 1, min(idx + 10, len(lines))):
+        if "-->" not in lines[j]:
+            continue
+        path_parts = []
+        arrow_line = lines[j].split("-->", 1)
+        if len(arrow_line) > 1:
+            path_parts.append(arrow_line[1].strip())
+
+        for k in range(j + 1, min(j + 5, len(lines))):
+            stripped = lines[k].strip()
+            if not stripped or stripped == "|":
+                break
+            path_parts.append(stripped)
+            if re.search(r":\d+:\d+:\s*$", stripped):
+                break
+
+        path_match = re.search(r"^(.+?):\d+:\d+:\s*$", "".join(path_parts))
+        if path_match:
+            return path_match.group(1).strip()
+        return None
+    return None
+
+
 @dataclass
 class CompilationWorkaround:
     """Represents a compilation workaround that can be applied to fix errors."""
@@ -224,6 +285,10 @@ def __init__(
         # that failed, so it must describe *that* failure and never an earlier pass's.
         self.last_import_diagnostics: List[UnresolvedImport] = []
         self._remappings_workaround_applied = False
+        # contract name -> every compiler version mismatch reported for it in this run. A list
+        # because the test for a contradiction is pairwise and more than two passes can report
+        # the same contract.
+        self._pragma_readings: Dict[str, List[PragmaReading]] = {}
         # (consumer, lib) pairs already covered by a generated harness in this run.
         # Used as a loop guard — if the prover still reports the same pair after we
         # wrapped the consumer, the workaround stops firing to avoid spinning.
@@ -442,6 +507,10 @@ def run_compilation_with_workarounds(
         # Rebuilt from each failed output, before the workaround table runs.
         solc_fallback_plan: Optional[SolcFallbackPlan] = None
 
+        # Rebuilt from each failed output, before the workaround table runs: the reading is
+        # also what the terminal pragma-conflict check tests, so the pass detects once.
+        version_mismatch: Optional[Tuple[str, str]] = None
+
         # Initialize workarounds list
         workarounds = [
             CompilationWorkaround(
@@ -484,7 +553,9 @@ def run_compilation_with_workarounds(
             ),
             CompilationWorkaround(
                 name="compiler_version_mismatch",
-                detect_fn=lambda output: self._detect_compiler_version_mismatch(output, contracts),
+                # Detected once per pass below, because the same reading feeds the terminal
+                # check that has to run before this table.
+                detect_fn=lambda output: version_mismatch,
                 apply_fn=self._apply_compiler_version_workaround_to_config,
                 # Enabled even when a global solc is configured: the detector
                 # only fires when that compiler provably cannot parse a file
@@ -743,6 +814,7 @@ def run_compilation_with_workarounds(
             solc_fallback_plan = (
                 self._plan_solc_fallback(output, updated_config_dict, contracts) if solc_pinned else None
             )
+            version_mismatch = self._detect_compiler_version_mismatch(output, contracts)
             if solc_fallback_plan is not None and solc_fallback_plan.blocked:
                 self._finalize_compile_maps(compilation_config, updated_config_dict, config_file)
                 installed = ", ".join(binary for binary, _ in self._solc_fallback_candidates()) or "none"
@@ -753,6 +825,39 @@ def run_compilation_with_workarounds(
                     f"{installed}. Install '{solc_fallback_plan.failed_solc}' to compile this project."
                 )
 
+            # Also terminal: this contract's compilation unit spans files whose pragmas no one
+            # compiler satisfies. Pinning it to either version leaves the other file rejecting
+            # it, and compiler_map is keyed by contract, so the conf cannot express the split.
+            # The specs decide it, not the versions read off them: ">=0.7.0" followed by
+            # "=0.7.6" names two versions and one satisfiable range.
+            if version_mismatch is not None:
+                contract_name, new_version = version_mismatch
+                readings = self._pragma_readings.get(contract_name, [])
+                newest = readings[-1]
+                for earlier in readings[:-1]:
+                    # The split needs two different files that solc named. Two specs read out
+                    # of one file are that file's own business, and a diagnostic carrying no
+                    # source location names nothing to weigh against the other reading.
+                    if not (earlier.source_path and newest.source_path):
+                        continue
+                    if earlier.source_path == newest.source_path:
+                        continue
+                    # `None` is "the spec parsed into no single constraint" (a disjunction, say)
+                    # — unknown, which is not a contradiction.
+                    if pragma_admits(earlier.pragma_spec, new_version) is False:
+                        self._finalize_compile_maps(
+                            compilation_config, updated_config_dict, config_file
+                        )
+                        raise ConflictingPragmaError(
+                            f"Contract '{contract_name}' is compiled together with files whose "
+                            f"pragmas cannot be satisfied by one compiler: "
+                            f"'{earlier.source_path}' declares '{earlier.pragma_spec}' "
+                            f"(compiler {earlier.version}) while '{newest.source_path}' declares "
+                            f"'{newest.pragma_spec}' (compiler {new_version}). compiler_map is "
+                            f"keyed by contract, so it cannot give the two files different "
+                            f"compilers — the sources have to agree on a version range."
+                        )
+
             # One pass over the failed output: apply EVERY applicable workaround
             # before recompiling — one full certoraRun per pass is expensive, so
             # a pass fixes as much of this output as it can. detect_fns run
@@ -1126,31 +1231,13 @@ def _detect_compiler_version_mismatch(
             # so context searches below start from where the marker begins.
             i = output.count("\n", 0, match.start())
 
-            # Try to find file_path from preceding "Compiling ..." line
-            file_path = _find_compiling_path_before(lines, i, max_lookback=15)
+            # The file the pragma was read out of, which solc names in the diagnostic's own
+            # source location. A compilation unit spans several files, so this is often not
+            # the file being compiled but one it imports.
+            pragma_source = _diagnostic_source_path(output, lines, match.start(), i)
 
-            # Fallback: Extract file_path from arrow line if not found above
-            if not file_path:
-                for j in range(i + 1, min(i + 10, len(lines))):
-                    if "-->" in lines[j]:
-                        path_parts = []
-                        arrow_line = lines[j].split("-->", 1)
-                        if len(arrow_line) > 1:
-                            path_parts.append(arrow_line[1].strip())
-
-                        for k in range(j + 1, min(j + 5, len(lines))):
-                            stripped = lines[k].strip()
-                            if not stripped or stripped == "|":
-                                break
-                            path_parts.append(stripped)
-                            if re.search(r":\d+:\d+:\s*$", stripped):
-                                break
-
-                        full_path = "".join(path_parts)
-                        path_match = re.search(r"^(.+?):\d+:\d+:\s*$", full_path)
-                        if path_match:
-                            file_path = path_match.group(1).strip()
-                            break
+            # The file being compiled, which is what maps to a contract in the conf.
+            file_path = _find_compiling_path_before(lines, i, max_lookback=15) or pragma_source
 
             if not file_path:
                 continue
@@ -1161,12 +1248,33 @@ def _detect_compiler_version_mismatch(
                 if pragma_spec:
                     version = resolve_pragma_to_version(pragma_spec)
                     if not version:
-                        self.log(f"Could not resolve pragma '{pragma_spec}' to concrete version", "WARNING")
+                        self.log(
+                            f"Could not resolve pragma '{pragma_spec}' in '{file_path}' to a "
+                            f"concrete version",
+                            "WARNING",
+                        )
                         return None
 
                     contract_name = self._get_contract_name_from_path(file_path, contracts)
                     if contract_name:
-                        self.log(f"Detected compiler version mismatch for {contract_name}: requires {version}")
+                        # One contract can be reported twice with different versions across a
+                        # retry loop — from two files in its compilation unit, or from two
+                        # specs in one file. Naming the compiled file, the file the spec was
+                        # read out of and the raw spec tells those apart and makes the conf
+                        # entry that follows traceable to the line it came from.
+                        self.log(
+                            f"Detected compiler version mismatch for {contract_name} while "
+                            f"compiling '{file_path}': requires {version} (from "
+                            f"'{pragma_spec}' in '{pragma_source}')"
+                        )
+                        self._pragma_readings.setdefault(contract_name, []).append(
+                            PragmaReading(
+                                version=version,
+                                file_path=file_path,
+                                source_path=pragma_source,
+                                pragma_spec=pragma_spec,
+                            )
+                        )
                         return (contract_name, version)
                     else:
                         self.log(f"Warning: Could not map path '{file_path}' to contract name", "WARNING")
diff --git a/certora_autosetup/utils/remappings.py b/certora_autosetup/utils/remappings.py
index ab2e0f1b..23819ea2 100644
--- a/certora_autosetup/utils/remappings.py
+++ b/certora_autosetup/utils/remappings.py
@@ -5,6 +5,13 @@
 the same packages list — historically they diverged, which is what left the initial conf missing
 ``remappings.txt`` / auto-inferred ``lib/*`` entries and caused ``ParserError: Source "…" not
 found``. This module is the single source of truth both call.
+
+A run root often holds more than one project, and each of them declares its own import
+resolution. Every project other than the anchor therefore contributes *context-scoped* entries
+(``<project-rel-path>/:prefix=target``) next to the anchor's unscoped ones. solc matches a
+context against the importing file's source unit name and prefers the longest match, so a
+scoped entry governs the files of the project it names while the anchor's entries remain the
+default for every file no context claims.
 """
 
 import json
@@ -16,6 +23,9 @@
 
 import tomllib
 
+from certora_autosetup.build_systems.config_files import BUILD_CONFIG_FILENAMES
+from certora_autosetup.setup.solidity_utils import DEPENDENCIES
+
 # (message, level) -> None; matches BuildSystemManager.log / CompilationWorkaroundManager.log.
 LogFn = Callable[[str, str], None]
 
@@ -221,6 +231,37 @@ def build_packages_from_remapping_sources(
     2. foundry.toml — hand-curated source of truth for the build system
     3. remappings.txt — often partially auto-generated; may drift
     4. package.json — npm-style fallback
+
+    Every *other* project under ``run_root`` contributes its own resolution too, as
+    context-scoped entries (``<project-rel-path>/:prefix=target``). solc matches a context
+    against the importing file's source unit name and prefers the longest match, so such an
+    entry governs that project's files while the entries above stay the default for every file
+    no context claims (see ``_scope_other_projects``).
+    """
+    remapping_key_to_path, remapping_key_to_source = _collect_remapping_entries(
+        base_dir, log_fn, profile, run_root
+    )
+    _scope_other_projects(
+        remapping_key_to_path=remapping_key_to_path,
+        remapping_key_to_source=remapping_key_to_source,
+        base_dir=base_dir,
+        run_root=run_root,
+        log_fn=log_fn,
+    )
+    return [f"{key}={path}" for key, path in remapping_key_to_path.items()]
+
+
+def _collect_remapping_entries(
+    base_dir: Path,
+    log_fn: LogFn,
+    profile: str,
+    run_root: Optional[Path],
+) -> Tuple[Dict[str, str], Dict[str, str]]:
+    """Read one project's four remapping sources into (key -> path, key -> source) maps.
+
+    The sources, their priority and the meaning of ``profile`` and ``run_root`` are the ones
+    ``build_packages_from_remapping_sources`` documents. The maps are handed back unformatted
+    so another project's resolution can be merged into them before the list is built.
     """
     # Data collection: key -> resolved path (first source to set a key wins) and key -> source
     # (for the mismatch warning). The packages list is formatted once at the end, preserving this
@@ -336,7 +377,122 @@ def build_packages_from_remapping_sources(
                     log_fn=log_fn,
                 )
 
-    return [f"{key}={path}" for key, path in remapping_key_to_path.items()]
+    return remapping_key_to_path, remapping_key_to_source
+
+
+def _projects_under(base_dir: Path, run_root: Optional[Path]) -> List[Path]:
+    """Every project under ``run_root`` other than ``base_dir`` and its ancestors.
+
+    A project is a directory holding one of ``BUILD_CONFIG_FILENAMES``. The config is what
+    declares the project's import resolution, and it declares it whether or not the project
+    ever compiled: a sibling whose own build failed has no artifacts, and a build that failed
+    for want of the right copy of a package is exactly the case these entries answer. The walk
+    prunes hidden directories and the vendored-dependency names in ``DEPENDENCIES``, whose
+    configs belong to a dependency rather than to the repo under analysis. A project nested
+    inside another is kept: its
+    context is longer, hence more specific, which is what solc should prefer for its files.
+
+    ``base_dir``, its ancestors and the run root are excluded. An ancestor's context prefixes
+    the anchor's own source unit names as well, and being longer than the empty context it
+    would outrank the anchor's global entries for exactly the files those entries are for.
+
+    Comparison is textual (``os.path.normpath``, never ``Path.resolve``), the contract
+    ``_ancestor_roots`` documents and depends on.
+    """
+    if run_root is None:
+        return []
+
+    excluded = {os.path.normpath(root) for root in _ancestor_roots(base_dir, run_root)}
+    projects: List[Path] = []
+    for dirpath, dirnames, filenames in os.walk(str(run_root)):
+        dirnames[:] = [d for d in dirnames if not d.startswith(".") and d not in DEPENDENCIES]
+        if os.path.normpath(dirpath) in excluded:
+            continue
+        if any(config in filenames for config in BUILD_CONFIG_FILENAMES):
+            projects.append(Path(dirpath))
+    return sorted(projects, key=lambda project: os.path.relpath(project, run_root))
+
+
+def _prefixed_log(prefix: str, log_fn: LogFn) -> LogFn:
+    """A log function tagging every message with ``prefix``, so a hoist or an unresolved
+    package read out of a sibling project is attributable to that project."""
+
+    def log(message: str, level: str) -> None:
+        log_fn(f"[{prefix}] {message}", level)
+
+    return log
+
+
+def _scope_other_projects(
+    *,
+    remapping_key_to_path: Dict[str, str],
+    remapping_key_to_source: Dict[str, str],
+    base_dir: Path,
+    run_root: Optional[Path],
+    log_fn: LogFn,
+) -> None:
+    """Merge every other project's resolution in, scoped to that project's files.
+
+    Each entry is keyed ``<project-rel-path>/:prefix``, which solc applies only to files whose
+    source unit name starts with that path — so a project pinned to its own copy of a package
+    keeps it while the anchor's unscoped entry stays the default everywhere else.
+    """
+    for project in _projects_under(base_dir, run_root):
+        rel = os.path.relpath(project, run_root)
+        # Siblings are read under the default profile because the reactive rebuild in
+        # `compilation_workarounds` passes no profile; the two writers must produce the same
+        # keys, or the first workaround to fire would rebuild the conf without the scoping.
+        project_paths, _ = _collect_remapping_entries(
+            base_dir=project,
+            log_fn=_prefixed_log(rel, log_fn),
+            profile="default",
+            run_root=run_root,
+        )
+        for key, path in project_paths.items():
+            # A key that already carries a context is one the project authored. `_rebase_context`
+            # expresses such a context run-root-relative when it names a directory in the
+            # project, and leaves it as authored when it names none — so only a context that
+            # lands inside the project is taken as it stands. Anything else is composed under
+            # the project, because a context reaching outside it would outrank the anchor's
+            # shorter entries for the anchor's own files. Composing `rel` needs no rebasing,
+            # since it is run-root-relative by construction.
+            if ":" in key:
+                context, prefix = key.split(":", 1)
+                normalized = os.path.normpath(context)
+                if normalized == rel or normalized.startswith(rel + os.sep):
+                    scoped_key = key
+                else:
+                    scoped_key = f"{os.path.join(rel, context.lstrip(os.sep))}:{prefix}"
+            else:
+                scoped_key = f"{rel}/:{key}"
+                prefix = key
+            # The same target under a longer context is the same binding spelled twice.
+            if remapping_key_to_path.get(prefix) == path:
+                continue
+            if not Path(path).exists():
+                # A scoped entry outranks the global one for every file under it, so binding
+                # the prefix to a directory already known to be absent would replace a
+                # resolution that may work with one that cannot.
+                governing = remapping_key_to_path.get(prefix)
+                keeps = (
+                    f"'{prefix}={governing}' keeps governing it"
+                    if governing
+                    else "the prefix stays unmapped"
+                )
+                log_fn(
+                    f"Project '{rel}' maps '{prefix}' to {path}, which does not exist; {keeps}",
+                    "WARNING",
+                )
+                continue
+            _record_entry(
+                key=scoped_key,
+                path=path,
+                source_name=f"{rel} remapping sources",
+                remapping_key_to_path=remapping_key_to_path,
+                remapping_key_to_source=remapping_key_to_source,
+                warn_on_mismatch=False,
+                log_fn=log_fn,
+            )
 
 
 def _rebase_context(context: str, base_dir: Path, run_root: Optional[Path], log_fn: LogFn) -> str:
@@ -470,6 +626,37 @@ def _merge_remapping_entry(
         if path and not path.endswith("/"):
             path += "/"
 
+    _record_entry(
+        key=key,
+        path=path,
+        source_name=source_name,
+        remapping_key_to_path=remapping_key_to_path,
+        remapping_key_to_source=remapping_key_to_source,
+        warn_on_mismatch=warn_on_mismatch,
+        log_fn=log_fn,
+    )
+
+
+def _record_entry(
+    *,
+    key: str,
+    path: str,
+    source_name: str,
+    remapping_key_to_path: Dict[str, str],
+    remapping_key_to_source: Dict[str, str],
+    warn_on_mismatch: bool,
+    log_fn: LogFn,
+) -> None:
+    """Record an already-canonical key/path pair under the first-wins rule.
+
+    On a key conflict (already populated by an earlier-priority source):
+    - if ``warn_on_mismatch`` and the stored path differs from the new one, log a warning naming
+      the actual earlier source from ``remapping_key_to_source``;
+    - otherwise silently skip.
+
+    Both halves are taken as given, which is what lets a caller holding a key and a target
+    already in canonical form record them without composing and re-parsing an entry string.
+    """
     if key in remapping_key_to_path:
         if warn_on_mismatch and remapping_key_to_path[key] != path:
             earlier_source = remapping_key_to_source[key]
diff --git a/tests/test_compilation_workarounds.py b/tests/test_compilation_workarounds.py
index 7ab643e2..d515da79 100644
--- a/tests/test_compilation_workarounds.py
+++ b/tests/test_compilation_workarounds.py
@@ -9,6 +9,7 @@
 from certora_autosetup.utils.compilation_workarounds import (
     VIA_IR_SCENE_THRESHOLD,
     CompilationWorkaroundManager,
+    ConflictingPragmaError,
     UnimplementedContractError,
     UnsatisfiableSolcPinError,
 )
@@ -685,6 +686,145 @@ def test_detects_single_line_compiler_version_mismatch(
     assert result == ("DummyERC20Impl", "0.8.30")
 
 
+def test_the_detection_names_the_file_and_spec_it_read(
+    manager: CompilationWorkaroundManager, resolve_pragma_offline, capsys
+) -> None:
+    # The conf entry that follows is keyed by contract, while the version is read off one
+    # file's pragma. When a retry loop reports the same contract at two versions, the file
+    # and the raw spec are what tell the two detections apart.
+    manager._detect_compiler_version_mismatch(
+        SINGLE_LINE_COMPILER_VERSION_MISMATCH, MISMATCH_CONTRACTS
+    )
+    detection = [
+        line for line in capsys.readouterr().out.splitlines()
+        if "compiler version mismatch" in line
+    ]
+    assert len(detection) == 1
+    assert "^0.8.0" in detection[0]
+    assert "certora/mocks/DummyERC20Impl.sol" in detection[0]
+
+
+# A contract's compilation unit spans several files, and two of them can declare pragmas no
+# single compiler satisfies. compiler_map is keyed by contract, so the conf has no way to give
+# the two files different compilers and the run stops instead of alternating between them.
+
+PRAGMA_CONFLICT_CONTRACTS = [
+    ContractHandle(contract_name="Widget", source_file="src/Widget.sol"),
+    # Both files answer to the one conf entry, which is what makes the split inexpressible.
+    ContractHandle(contract_name="Widget", source_file="src/Dep.sol"),
+]
+
+
+def _mismatch_output(source_path: str, current: str, spec: str) -> str:
+    """A failed pass compiling ``src/Widget.sol``, whose pragma solc read out of ``source_path``.
+
+    The compiled file is the same in every output on purpose: the unit is entered through the
+    contract the conf names, and which of its files declared the offending pragma is what the
+    ``ParserError`` location says.
+    """
+    return (
+        f"Compiling src/Widget.sol...\n"
+        f"solc{current} had an error:\n"
+        f"{source_path}:2:1: ParserError: Source file requires different compiler version "
+        f"(current compiler is {current}+commit.9bfce1f6.Linux.g++)\n"
+        f"pragma solidity {spec};\n"
+    )
+
+
+@pytest.fixture
+def resolve_pragma_by_spec(monkeypatch):
+    """resolve_pragma_to_version fetches soliditylang.org; answer from the spec itself."""
+    versions = {
+        "^0.8.20": "0.8.20",
+        "=0.7.6": "0.7.6",
+        ">=0.7.0": "0.7.0",
+        "^0.6.0 || ^0.8.0": "0.8.20",
+    }
+    monkeypatch.setattr(
+        "certora_autosetup.utils.compilation_workarounds.resolve_pragma_to_version",
+        lambda spec, **kwargs: versions[spec],
+    )
+
+
+def test_two_files_pinning_incompatible_compilers_stops_the_run(
+    manager, monkeypatch, tmp_path, resolve_pragma_by_spec
+) -> None:
+    # The two passes compile the same file and differ only in which file solc read the pragma
+    # out of — the alternation this is for, and the one thing that separates the readings.
+    outputs = [
+        _mismatch_output("src/Widget.sol", "0.7.6", "^0.8.20"),
+        _mismatch_output("src/Dep.sol", "0.8.20", "=0.7.6"),
+    ]
+    assert all(output.startswith("Compiling src/Widget.sol...") for output in outputs)
+
+    with pytest.raises(ConflictingPragmaError) as raised:
+        _run_loop(manager, monkeypatch, tmp_path, outputs, PRAGMA_CONFLICT_CONTRACTS)
+
+    message = str(raised.value)
+    assert "src/Widget.sol" in message and "src/Dep.sol" in message
+    assert "^0.8.20" in message and "=0.7.6" in message
+    assert "0.8.20" in message and "0.7.6" in message
+
+
+def test_converging_pragmas_let_the_workaround_pin_the_contract(
+    manager, monkeypatch, tmp_path, resolve_pragma_by_spec
+) -> None:
+    # ">=0.7.0" then "=0.7.6" names two versions and one satisfiable range: the specs decide,
+    # not the versions read off them.
+    success, updated, _, _ = _run_loop(
+        manager,
+        monkeypatch,
+        tmp_path,
+        [
+            _mismatch_output("src/Widget.sol", "0.6.12", ">=0.7.0"),
+            _mismatch_output("src/Dep.sol", "0.7.0", "=0.7.6"),
+        ],
+        PRAGMA_CONFLICT_CONTRACTS,
+    )
+
+    assert success is True
+    # A one-contract map uniform in the end collapses back to the scalar on finalize.
+    assert updated["solc"] == "solc7.6"
+
+
+def test_two_specs_in_one_file_are_not_a_conflict(
+    manager, monkeypatch, tmp_path, resolve_pragma_by_spec
+) -> None:
+    # One file cannot be split across two compilers by any conf, so the pair is that file's own
+    # business — only a second file in the unit makes the contradiction this check is for.
+    success, _, _, _ = _run_loop(
+        manager,
+        monkeypatch,
+        tmp_path,
+        [
+            _mismatch_output("src/Widget.sol", "0.7.6", "^0.8.20"),
+            _mismatch_output("src/Widget.sol", "0.8.20", "=0.7.6"),
+        ],
+        PRAGMA_CONFLICT_CONTRACTS,
+    )
+
+    assert success is True
+
+
+def test_a_spec_that_is_not_one_constraint_is_not_a_conflict(
+    manager, monkeypatch, tmp_path, resolve_pragma_by_spec
+) -> None:
+    # A disjunction parses into no single constraint, which is unknown rather than a
+    # contradiction.
+    success, _, _, _ = _run_loop(
+        manager,
+        monkeypatch,
+        tmp_path,
+        [
+            _mismatch_output("src/Widget.sol", "0.7.6", "^0.6.0 || ^0.8.0"),
+            _mismatch_output("src/Dep.sol", "0.8.20", "=0.7.6"),
+        ],
+        PRAGMA_CONFLICT_CONTRACTS,
+    )
+
+    assert success is True
+
+
 def test_ignores_unrelated_compiler_version_mismatch(
     manager: CompilationWorkaroundManager,
 ) -> None:
@@ -1236,6 +1376,25 @@ def test_packages_come_from_the_nested_build_config_dir(tmp_path: Path, monkeypa
     assert f"@pkg/={project / 'node_modules/@pkg/artifacts/src'}/" in packages
 
 
+def test_the_rebuild_keeps_the_other_projects_scoped(tmp_path: Path, monkeypatch) -> None:
+    # The retry loop rebuilds the packages list from the same sources, so it must reproduce the
+    # context-scoped entries the initial conf carries — otherwise the first workaround to fire
+    # replaces a scoped conf with a flat one and the sibling resolves through the anchor again.
+    _no_forge(monkeypatch)
+    app = tmp_path / "app"
+    other = tmp_path / "other"
+    for project in (app, other):
+        (project / "out").mkdir(parents=True)
+        (project / "foundry.toml").write_text("[profile.default]\n")
+        (project / "remappings.txt").write_text("@pkg/contracts/=node_modules/@pkg/contracts/\n")
+        (project / "node_modules" / "@pkg" / "contracts").mkdir(parents=True)
+
+    manager = CompilationWorkaroundManager(project_root=tmp_path, build_config_dir=app)
+    packages = manager._build_packages_from_remapping_sources()
+
+    assert f"other/:@pkg/contracts/={other / 'node_modules/@pkg/contracts'}/" in packages
+
+
 def test_build_config_dir_defaults_to_project_root(tmp_path: Path, monkeypatch) -> None:
     # Root-level projects keep today's behaviour without the caller passing anything.
     _no_forge(monkeypatch)
diff --git a/tests/test_remappings.py b/tests/test_remappings.py
index 603b4156..9a7e075f 100644
--- a/tests/test_remappings.py
+++ b/tests/test_remappings.py
@@ -10,8 +10,10 @@
 package.json), and the present-forge case feeds canned output to assert priority.
 """
 
+import shutil
 import subprocess
 from pathlib import Path
+from typing import Tuple
 
 import pytest
 
@@ -693,3 +695,242 @@ def test_parse_config_emits_run_root_relative_hoisted_packages(tmp_path: Path, m
 
     # Relative (no `../`, no absolute fallback): the walk never leaves the run root.
     assert packages == ["@vault/=node_modules/@vault/core/contracts"]
+
+
+# =============================================================================
+# Several projects under one run root: context-scoped entries
+# =============================================================================
+#
+# A run root can hold more than one built project, each declaring its own resolution for the
+# same package prefix. solc matches a remapping context against the importing file's source
+# unit name and prefers the longest match, so every project other than the anchor contributes
+# `<project>/:prefix=target` entries that govern its own files, while the anchor's unscoped
+# entries stay the default for every file no context claims.
+
+_SAME_PREFIX_REMAPPING = "@pkg/contracts/=node_modules/@pkg/contracts/\n"
+
+
+def _build_project(project: Path, remappings: str = _SAME_PREFIX_REMAPPING) -> Path:
+    """A Foundry project that compiled: a config (which is how discovery recognises it), an
+    artifact dir and its own installed copy of the remapped package.
+
+    The copy is really created: an absent target keeps the base-dir path and only warns, so a
+    forgotten mkdir would let a wrong result pass for a right one.
+    """
+    (project / "out").mkdir(parents=True, exist_ok=True)
+    (project / "foundry.toml").write_text("[profile.default]\n")
+    (project / "remappings.txt").write_text(remappings)
+    (project / "node_modules" / "@pkg" / "contracts").mkdir(parents=True, exist_ok=True)
+    return project
+
+
+def _two_project_repo(tmp_path: Path) -> Tuple[Path, Path]:
+    """Two built projects side by side under the run root, both binding @pkg/contracts/ to
+    their own node_modules copy."""
+    return _build_project(tmp_path / "app"), _build_project(tmp_path / "other")
+
+
+def test_a_sibling_project_binds_the_shared_prefix_to_its_own_copy(
+    tmp_path: Path, monkeypatch
+) -> None:
+    app, other = _two_project_repo(tmp_path)
+    _no_forge(monkeypatch)
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+    )
+
+    assert _path_of(packages, "@pkg/contracts/") == str(app / "node_modules/@pkg/contracts") + "/"
+    assert (
+        _path_of(packages, "other/:@pkg/contracts/")
+        == str(other / "node_modules/@pkg/contracts") + "/"
+    )
+
+
+def test_a_sibling_target_that_is_absent_leaves_the_prefix_alone(
+    tmp_path: Path, monkeypatch
+) -> None:
+    # A scoped entry outranks the global one for every file under it, so a target already known
+    # to be missing must not replace a binding that may work.
+    app, other = _two_project_repo(tmp_path)
+    shutil.rmtree(other / "node_modules")
+    _no_forge(monkeypatch)
+    logged: list = []
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda m, level: logged.append((m, level)), run_root=tmp_path
+    )
+    anchor_only = build_packages_from_remapping_sources(base_dir=app, log_fn=lambda *_: None)
+
+    assert not [key for key in _keys(packages) if key.startswith("other/:")]
+    assert packages == anchor_only
+    warnings = [m for m, level in logged if level == "WARNING"]
+    assert any(
+        "@pkg/contracts/" in m
+        and str(other / "node_modules/@pkg/contracts") in m
+        and str(app / "node_modules/@pkg/contracts") in m
+        for m in warnings
+    ), warnings
+
+
+def test_a_projects_own_context_is_not_prefixed_twice(tmp_path: Path, monkeypatch) -> None:
+    # This project's authored context names a directory it really has, so `_rebase_context`
+    # expresses it run-root-relative and it is taken as it stands; prefixing it again would
+    # name nothing on disk.
+    app, other = _two_project_repo(tmp_path)
+    (other / "node_modules" / "dep").mkdir(parents=True)
+    (other / "node_modules" / "@pkg" / "alt").mkdir(parents=True)
+    (other / "remappings.txt").write_text(
+        "node_modules/dep/:@pkg/contracts/=node_modules/@pkg/alt/\n"
+    )
+    _no_forge(monkeypatch)
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+    )
+
+    assert (
+        _path_of(packages, "other/node_modules/dep/:@pkg/contracts/")
+        == str(other / "node_modules/@pkg/alt") + "/"
+    )
+    assert not [key for key in _keys(packages) if key.count(":") > 1]
+
+
+def test_a_sibling_context_naming_nothing_is_confined_to_the_sibling(
+    tmp_path: Path, monkeypatch
+) -> None:
+    # `_rebase_context` leaves a context alone when it names no directory in the project, so
+    # the authored spelling reaches here as it stands. Emitted verbatim it would be longer than
+    # the anchor's empty context and would govern every file whose source unit name starts with
+    # it — the anchor's own files included.
+    # The anchor sits at the run root, so its own source unit names start with `vendored/` —
+    # the very prefix the sibling's context spells.
+    app = _build_project(tmp_path)
+    other = _build_project(tmp_path / "other")
+    (app / "vendored").mkdir()
+    (other / "node_modules" / "@pkg" / "alt").mkdir(parents=True)
+    (other / "remappings.txt").write_text("vendored/:@pkg/contracts/=node_modules/@pkg/alt/\n")
+    _no_forge(monkeypatch)
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+    )
+
+    assert (
+        _path_of(packages, "other/vendored/:@pkg/contracts/")
+        == str(other / "node_modules/@pkg/alt") + "/"
+    )
+    assert _keys(packages) == {"@pkg/contracts/", "other/vendored/:@pkg/contracts/"}
+
+
+def test_the_scoped_context_keeps_its_boundary_slash(tmp_path: Path, monkeypatch) -> None:
+    # The context is a source-unit-name prefix whose boundary is the slash: without it,
+    # `other` would also claim the files of a sibling named `other-tools`.
+    app, _other = _two_project_repo(tmp_path)
+    _build_project(tmp_path / "other-tools")
+    _no_forge(monkeypatch)
+
+    keys = _keys(
+        build_packages_from_remapping_sources(
+            base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+        )
+    )
+
+    assert "other/:@pkg/contracts/" in keys
+    assert "other:@pkg/contracts/" not in keys
+    assert "other-tools/:@pkg/contracts/" in keys
+
+
+def test_single_project_packages_are_identical_with_and_without_run_root(
+    tmp_path: Path, monkeypatch
+) -> None:
+    # The ordinary repo: one project at the run root with its vendored trees. Nothing else is
+    # built under it, so the list must come out byte-identical to the no-run-root result and
+    # carry no context at all.
+    _build_project(tmp_path)
+    (tmp_path / "lib" / "widget").mkdir(parents=True)
+    _no_forge(monkeypatch)
+    (tmp_path / "remappings.txt").write_text(
+        _SAME_PREFIX_REMAPPING + "widget/=lib/widget/\n@absent/pkg/=node_modules/@absent/pkg/\n"
+    )
+
+    with_root = build_packages_from_remapping_sources(
+        base_dir=tmp_path, log_fn=lambda *_: None, run_root=tmp_path
+    )
+    without_root = build_packages_from_remapping_sources(base_dir=tmp_path, log_fn=lambda *_: None)
+
+    assert with_root == without_root
+    assert not [key for key in _keys(with_root) if ":" in key]
+
+
+def test_a_sibling_whose_build_failed_is_still_scoped(tmp_path: Path, monkeypatch) -> None:
+    # A project whose own build failed has no artifact directory, and its resolution is
+    # precisely what the failure is about — a config declares the resolution whether or not
+    # anything came of it.
+    app, _other = _two_project_repo(tmp_path)
+    unbuilt = _build_project(tmp_path / "unbuilt")
+    shutil.rmtree(unbuilt / "out")
+    _no_forge(monkeypatch)
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+    )
+
+    assert (
+        _path_of(packages, "unbuilt/:@pkg/contracts/")
+        == str(unbuilt / "node_modules/@pkg/contracts") + "/"
+    )
+
+
+def test_projects_inside_vendored_dependencies_are_never_walked(
+    tmp_path: Path, monkeypatch
+) -> None:
+    # A built project under lib/ or node_modules/ belongs to a dependency, not to the repo
+    # under analysis, and its files are not the ones the conf verifies.
+    app, _other = _two_project_repo(tmp_path)
+    _build_project(app / "lib" / "dep")
+    _build_project(tmp_path / "node_modules" / "pkg")
+    _no_forge(monkeypatch)
+
+    keys = _keys(
+        build_packages_from_remapping_sources(
+            base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+        )
+    )
+
+    assert not [key for key in keys if "lib/dep" in key or "node_modules/pkg" in key]
+
+
+def test_a_project_nested_under_the_anchor_is_scoped(tmp_path: Path, monkeypatch) -> None:
+    # Its context is longer than the anchor's globals, hence more specific — which is exactly
+    # what solc should prefer for its own files.
+    app, _other = _two_project_repo(tmp_path)
+    nested = _build_project(app / "modules" / "inner")
+    _no_forge(monkeypatch)
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+    )
+
+    assert (
+        _path_of(packages, "app/modules/inner/:@pkg/contracts/")
+        == str(nested / "node_modules/@pkg/contracts") + "/"
+    )
+
+
+def test_the_run_root_and_the_anchors_ancestors_are_never_scoped(
+    tmp_path: Path, monkeypatch
+) -> None:
+    # An ancestor's context prefixes the anchor's own source unit names too, and being longer
+    # than the empty context it would outrank the anchor's globals for exactly those files.
+    app = tmp_path / "packages" / "app"
+    for project in (tmp_path, tmp_path / "packages", app):
+        _build_project(project)
+    _no_forge(monkeypatch)
+
+    packages = build_packages_from_remapping_sources(
+        base_dir=app, log_fn=lambda *_: None, run_root=tmp_path
+    )
+
+    assert _keys(packages) == {"@pkg/contracts/"}
+    assert _path_of(packages, "@pkg/contracts/") == str(app / "node_modules/@pkg/contracts") + "/"