{"abstract":"Disjoint live regions are rejected unless one is empty.","category":"Borrow checking","checks":17,"contract":"Finite lexical regions map names to sets of program-point integers. Longer region contains every point of shorter. Queries: outlives(a,b), meet(a,b), join(a,b), missing(a,b), strict(a,b), eq(a,b), disjoint(a,b), covers(a, list-of-regions), gap(a,b,c) requires a cover intersection of b,c, and choose(a,candidates) returns lexically sorted candidate regions containing a with smallest cardinality, ties lexical. Return booleans or sorted lists as appropriate.","contract_signature":"regions, op, a, b, c=None","evaluation_group":"s3-borrow-checking-region-relations","failed_approach":"The partial repair uses if op=='disjoint': return not x or not regions[b], which still violates the stipulated analysis contract.","family":"s3-borrow-checking-region-relations-nonoverlap","id":"FA-42921","implementations":{"attempt":{"sha256":"9e313c6866e0f15faa3d0ef41712e57ba2ca3be05e967b22f9fc8c806ff9bbc5","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, op, a, b, c=None):\n    x=set(regions[a])\n    if op=='outlives': return x.issuperset(regions[b])\n    if op=='meet': return sorted(x.intersection(regions[b]))\n    if op=='join': return sorted(x.union(regions[b]))\n    if op=='missing': return sorted(set(regions[b])-x)\n    if op=='strict': return x>set(regions[b])\n    if op=='eq': return x==set(regions[b])\n    if op=='disjoint': return not x or not regions[b]\n    if op=='covers': return all(x.issuperset(regions[k]) for k in b)\n    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)\n    if op=='choose':\n        candidates=[k for k in b if set(regions[k]).issuperset(x)]\n        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None\n    return None\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nr={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}\ncheck('outlives',solve(r,'outlives','a','s'),True)\ncheck('incomparable',solve(r,'outlives','a','b'),False)\ncheck('meet',solve(r,'meet','a','b'),[N+1])\ncheck('join',solve(r,'join','a','b'),[N,N+1,N+2])\ncheck('missing',solve(r,'missing','a','b'),[N+2])\ncheck('strict equal',solve(r,'strict','a','a'),False)\ncheck('strict incomparable',solve(r,'strict','aa','b'),True)\ncheck('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)\ncheck('equivalent unordered',solve(r,'eq','a','z'),True)\ncheck('equivalent distinct',solve(r,'eq','a','b'),False)\ncheck('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)\ncheck('overlap disjoint',solve(r,'disjoint','a','b'),False)\ncheck('mixed obligations',solve(r,'covers','a',['s','b']),False)\ncheck('no obligations',solve(r,'covers','a',[]),True)\ncheck('joint demand',solve(r,'gap','e','a','b'),[N+1])\ncheck('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')\ncheck('no candidate',solve(r,'choose','aa',['a','s']),None)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"b156f77818bb433ceb0223c6aea5875417702a9691af728c7f376c268f3f128b","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, op, a, b, c=None):\n    x=set(regions[a])\n    if op=='outlives': return x.issuperset(regions[b])\n    if op=='meet': return sorted(x.intersection(regions[b]))\n    if op=='join': return sorted(x.union(regions[b]))\n    if op=='missing': return sorted(set(regions[b])-x)\n    if op=='strict': return x>set(regions[b])\n    if op=='eq': return x==set(regions[b])\n    if op=='disjoint': return x!=set(regions[b])\n    if op=='covers': return all(x.issuperset(regions[k]) for k in b)\n    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)\n    if op=='choose':\n        candidates=[k for k in b if set(regions[k]).issuperset(x)]\n        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None\n    return None\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nr={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}\ncheck('outlives',solve(r,'outlives','a','s'),True)\ncheck('incomparable',solve(r,'outlives','a','b'),False)\ncheck('meet',solve(r,'meet','a','b'),[N+1])\ncheck('join',solve(r,'join','a','b'),[N,N+1,N+2])\ncheck('missing',solve(r,'missing','a','b'),[N+2])\ncheck('strict equal',solve(r,'strict','a','a'),False)\ncheck('strict incomparable',solve(r,'strict','aa','b'),True)\ncheck('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)\ncheck('equivalent unordered',solve(r,'eq','a','z'),True)\ncheck('equivalent distinct',solve(r,'eq','a','b'),False)\ncheck('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)\ncheck('overlap disjoint',solve(r,'disjoint','a','b'),False)\ncheck('mixed obligations',solve(r,'covers','a',['s','b']),False)\ncheck('no obligations',solve(r,'covers','a',[]),True)\ncheck('joint demand',solve(r,'gap','e','a','b'),[N+1])\ncheck('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')\ncheck('no candidate',solve(r,'choose','aa',['a','s']),None)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"s3-borrow-checking-region-relations-nonoverlap","generated_at":"2026-09-29T14:43:56.632501+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.","root_cause":"The static analyzer mishandles nonoverlap: disjoint live regions are rejected unless one is empty.","sha256":"c19fd321e35ce59be304ae7002d37a0e54e1b61d6a493016b0190d2c27e5d938","title":"Disjoint live regions are rejected unless one is empty · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":46.504,"exit_code":1,"observations":[{"actual":true,"check":"outlives","expected":true,"passed":true},{"actual":false,"check":"incomparable","expected":false,"passed":true},{"actual":[2],"check":"meet","expected":[2],"passed":true},{"actual":[1,2,3],"check":"join","expected":[1,2,3],"passed":true},{"actual":[3],"check":"missing","expected":[3],"passed":true},{"actual":false,"check":"strict equal","expected":false,"passed":true},{"actual":true,"check":"strict incomparable","expected":true,"passed":true},{"actual":false,"check":"strict size insufficient","expected":false,"passed":true},{"actual":true,"check":"equivalent unordered","expected":true,"passed":true},{"actual":false,"check":"equivalent distinct","expected":false,"passed":true},{"actual":false,"check":"nonempty disjoint","expected":true,"passed":false},{"actual":false,"check":"overlap disjoint","expected":false,"passed":true},{"actual":false,"check":"mixed obligations","expected":false,"passed":true},{"actual":true,"check":"no obligations","expected":true,"passed":true},{"actual":[2],"check":"joint demand","expected":[2],"passed":true},{"actual":"s","check":"choose shortest","expected":"s","passed":true},{"actual":null,"check":"no candidate","expected":null,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"outlives\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"incomparable\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"meet\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"join\", \"actual\": [1, 2, 3], \"expected\": [1, 2, 3], \"passed\": true}, {\"check\": \"missing\", \"actual\": [3], \"expected\": [3], \"passed\": true}, {\"check\": \"strict equal\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"strict incomparable\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"strict size insufficient\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"equivalent unordered\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"equivalent distinct\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"nonempty disjoint\", \"actual\": false, \"expected\": true, \"passed\": false}, {\"check\": \"overlap disjoint\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"mixed obligations\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"no obligations\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"joint demand\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"choose shortest\", \"actual\": \"s\", \"expected\": \"s\", \"passed\": true}, {\"check\": \"no candidate\", \"actual\": null, \"expected\": null, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":41.247,"exit_code":1,"observations":[{"actual":true,"check":"outlives","expected":true,"passed":true},{"actual":false,"check":"incomparable","expected":false,"passed":true},{"actual":[2],"check":"meet","expected":[2],"passed":true},{"actual":[1,2,3],"check":"join","expected":[1,2,3],"passed":true},{"actual":[3],"check":"missing","expected":[3],"passed":true},{"actual":false,"check":"strict equal","expected":false,"passed":true},{"actual":true,"check":"strict incomparable","expected":true,"passed":true},{"actual":false,"check":"strict size insufficient","expected":false,"passed":true},{"actual":true,"check":"equivalent unordered","expected":true,"passed":true},{"actual":false,"check":"equivalent distinct","expected":false,"passed":true},{"actual":true,"check":"nonempty disjoint","expected":true,"passed":true},{"actual":true,"check":"overlap disjoint","expected":false,"passed":false},{"actual":false,"check":"mixed obligations","expected":false,"passed":true},{"actual":true,"check":"no obligations","expected":true,"passed":true},{"actual":[2],"check":"joint demand","expected":[2],"passed":true},{"actual":"s","check":"choose shortest","expected":"s","passed":true},{"actual":null,"check":"no candidate","expected":null,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"outlives\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"incomparable\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"meet\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"join\", \"actual\": [1, 2, 3], \"expected\": [1, 2, 3], \"passed\": true}, {\"check\": \"missing\", \"actual\": [3], \"expected\": [3], \"passed\": true}, {\"check\": \"strict equal\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"strict incomparable\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"strict size insufficient\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"equivalent unordered\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"equivalent distinct\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"nonempty disjoint\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"overlap disjoint\", \"actual\": true, \"expected\": false, \"passed\": false}, {\"check\": \"mixed obligations\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"no obligations\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"joint demand\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"choose shortest\", \"actual\": \"s\", \"expected\": \"s\", \"passed\": true}, {\"check\": \"no candidate\", \"actual\": null, \"expected\": null, \"passed\": true}], \"passed\": false}\n"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}