{"abstract":"Unreachable input becomes an unknown constant at a join.","category":"Static analysis soundness","checks":7,"contract":"Join constant states encoded as strings B (unreachable), T (unknown), or integer constants; return the least upper bound.","evaluation_group":"model-f611119fcb654a50","failed_approach":"Choosing the first non-bottom state ignores conflicting constants and later top states.","family":"z-static_analysis-constant-bottom","id":"FA-11526","implementations":{"attempt":{"sha256":"c2d60782acf70c0db370501895d72ca4f8e5dafce8489191a286953207e0faa3","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(a, b):\n    return b if a=='B' else a\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('bottom identity left',solve('B',N),N)\ncheck('bottom identity right',solve(N,'B'),N)\ncheck('different constants',solve(N,N+1),'T')\ncheck('same constant',solve(N,N),N)\ncheck('unknown absorbs right',solve(N,'T'),'T')\ncheck('both unreachable',solve('B','B'),'B')\ncheck('unknown absorbs left',solve('T',N),'T')\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":"6537eb5fc91b16f13e6f27c0074e185d6a29a9437dc7dd6dd4114186d17f1495","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(a, b):\n    return a if a==b else 'T'\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('bottom identity left',solve('B',N),N)\ncheck('bottom identity right',solve(N,'B'),N)\ncheck('different constants',solve(N,N+1),'T')\ncheck('same constant',solve(N,N),N)\ncheck('unknown absorbs right',solve(N,'T'),'T')\ncheck('both unreachable',solve('B','B'),'B')\ncheck('unknown absorbs left',solve('T',N),'T')\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"},"fixed":{"sha256":"c3ed7825da4c8765ead7c6fecc62fe59c13e900ba5c43e56f333fd60cac44f11","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(a, b):\n    if a=='B': return b\n    if b=='B': return a\n    return a if a==b else 'T'\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('bottom identity left',solve('B',N),N)\ncheck('bottom identity right',solve(N,'B'),N)\ncheck('different constants',solve(N,N+1),'T')\ncheck('same constant',solve(N,N),N)\ncheck('unknown absorbs right',solve(N,'T'),'T')\ncheck('both unreachable',solve('B','B'),'B')\ncheck('unknown absorbs left',solve('T',N),'T')\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":" 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":"z-static_analysis-constant-bottom","generated_at":"2026-09-29T14:38:48.682162+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.","repair":"Make bottom an identity, top absorbing, and merge unequal constants to top.","root_cause":"Bottom (no execution) and top (any value) are collapsed into one state.","sha256":"8607ea59d0953b1f69a60448239289471346eb28d815b84704c2807462c6c7cd","title":"Unreachable input becomes an unknown constant at a join · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":39.696,"exit_code":1,"observations":[{"actual":1,"check":"bottom identity left","expected":1,"passed":true},{"actual":1,"check":"bottom identity right","expected":1,"passed":true},{"actual":1,"check":"different constants","expected":"T","passed":false},{"actual":1,"check":"same constant","expected":1,"passed":true},{"actual":1,"check":"unknown absorbs right","expected":"T","passed":false},{"actual":"B","check":"both unreachable","expected":"B","passed":true},{"actual":"T","check":"unknown absorbs left","expected":"T","passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"bottom identity left\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"bottom identity right\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"different constants\", \"actual\": 1, \"expected\": \"T\", \"passed\": false}, {\"check\": \"same constant\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"unknown absorbs right\", \"actual\": 1, \"expected\": \"T\", \"passed\": false}, {\"check\": \"both unreachable\", \"actual\": \"B\", \"expected\": \"B\", \"passed\": true}, {\"check\": \"unknown absorbs left\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":38.363,"exit_code":1,"observations":[{"actual":"T","check":"bottom identity left","expected":1,"passed":false},{"actual":"T","check":"bottom identity right","expected":1,"passed":false},{"actual":"T","check":"different constants","expected":"T","passed":true},{"actual":1,"check":"same constant","expected":1,"passed":true},{"actual":"T","check":"unknown absorbs right","expected":"T","passed":true},{"actual":"B","check":"both unreachable","expected":"B","passed":true},{"actual":"T","check":"unknown absorbs left","expected":"T","passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"bottom identity left\", \"actual\": \"T\", \"expected\": 1, \"passed\": false}, {\"check\": \"bottom identity right\", \"actual\": \"T\", \"expected\": 1, \"passed\": false}, {\"check\": \"different constants\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}, {\"check\": \"same constant\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"unknown absorbs right\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}, {\"check\": \"both unreachable\", \"actual\": \"B\", \"expected\": \"B\", \"passed\": true}, {\"check\": \"unknown absorbs left\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":39.176,"exit_code":0,"observations":[{"actual":1,"check":"bottom identity left","expected":1,"passed":true},{"actual":1,"check":"bottom identity right","expected":1,"passed":true},{"actual":"T","check":"different constants","expected":"T","passed":true},{"actual":1,"check":"same constant","expected":1,"passed":true},{"actual":"T","check":"unknown absorbs right","expected":"T","passed":true},{"actual":"B","check":"both unreachable","expected":"B","passed":true},{"actual":"T","check":"unknown absorbs left","expected":"T","passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"bottom identity left\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"bottom identity right\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"different constants\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}, {\"check\": \"same constant\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"unknown absorbs right\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}, {\"check\": \"both unreachable\", \"actual\": \"B\", \"expected\": \"B\", \"passed\": true}, {\"check\": \"unknown absorbs left\", \"actual\": \"T\", \"expected\": \"T\", \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}