{"abstract":"Widening retains an escaping lower bound.","category":"Static analysis soundness","checks":6,"contract":"Widen finite old and next integer intervals; return [lower,upper], with None representing an unbounded endpoint. Preserve each old bound unless that direction expands.","evaluation_group":"model-835f62d9697cac77","failed_approach":"Dropping both bounds whenever either grows terminates but destroys stable-bound precision.","family":"z-static_analysis-widen-direction","id":"FA-11496","implementations":{"attempt":{"sha256":"75f2fcd4a93df0740966be3e165accf338adbfeed6ab87b8fd965407a244ea8e","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(old, new):\n    return [None,None] if new[0]<old[0] or new[1]>old[1] else list(old)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('lower expands alone',solve([0,N],[-N,N]),[None,N])\ncheck('upper expands alone',solve([0,N],[0,N+1]),[0,None])\ncheck('both expand',solve([0,N],[-1,N+1]),[None,None])\ncheck('equal',solve([0,N],[0,N]),[0,N])\ncheck('narrower',solve([-N,N],[0,0]),[-N,N])\ncheck('singleton expands right',solve([N,N],[N,N+1]),[N,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":"a959b02322edb1a0aa9c72b809b0de5cf71e8ebbcc0e221d03cd945083e54c9a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(old, new):\n    return [old[0],None if new[1]>old[1] else old[1]]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('lower expands alone',solve([0,N],[-N,N]),[None,N])\ncheck('upper expands alone',solve([0,N],[0,N+1]),[0,None])\ncheck('both expand',solve([0,N],[-1,N+1]),[None,None])\ncheck('equal',solve([0,N],[0,N]),[0,N])\ncheck('narrower',solve([-N,N],[0,0]),[-N,N])\ncheck('singleton expands right',solve([N,N],[N,N+1]),[N,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"},"fixed":{"sha256":"2db15f6cd81db9f29979cfefdd54611a2e2e0f4a6869d6772405734fede27d77","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(old, new):\n    return [None if new[0]<old[0] else old[0],None if new[1]>old[1] else old[1]]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('lower expands alone',solve([0,N],[-N,N]),[None,N])\ncheck('upper expands alone',solve([0,N],[0,N+1]),[0,None])\ncheck('both expand',solve([0,N],[-1,N+1]),[None,None])\ncheck('equal',solve([0,N],[0,N]),[0,N])\ncheck('narrower',solve([-N,N],[0,0]),[-N,N])\ncheck('singleton expands right',solve([N,N],[N,N+1]),[N,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":" 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-widen-direction","generated_at":"2026-09-29T14:38:48.485168+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":"Drop each bound independently when the next interval expands beyond that old bound.","root_cause":"A loop interval widening handles growth only at its upper endpoint.","sha256":"337115f29d9dc812141d17faa2a1b5c6eb9d1a1fc33cb7b39e23c912bd8d516c","title":"Widening retains an escaping lower bound · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":38.059,"exit_code":1,"observations":[{"actual":[null,null],"check":"lower expands alone","expected":[null,1],"passed":false},{"actual":[null,null],"check":"upper expands alone","expected":[0,null],"passed":false},{"actual":[null,null],"check":"both expand","expected":[null,null],"passed":true},{"actual":[0,1],"check":"equal","expected":[0,1],"passed":true},{"actual":[-1,1],"check":"narrower","expected":[-1,1],"passed":true},{"actual":[null,null],"check":"singleton expands right","expected":[1,null],"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"lower expands alone\", \"actual\": [null, null], \"expected\": [null, 1], \"passed\": false}, {\"check\": \"upper expands alone\", \"actual\": [null, null], \"expected\": [0, null], \"passed\": false}, {\"check\": \"both expand\", \"actual\": [null, null], \"expected\": [null, null], \"passed\": true}, {\"check\": \"equal\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"narrower\", \"actual\": [-1, 1], \"expected\": [-1, 1], \"passed\": true}, {\"check\": \"singleton expands right\", \"actual\": [null, null], \"expected\": [1, null], \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":39.569,"exit_code":1,"observations":[{"actual":[0,1],"check":"lower expands alone","expected":[null,1],"passed":false},{"actual":[0,null],"check":"upper expands alone","expected":[0,null],"passed":true},{"actual":[0,null],"check":"both expand","expected":[null,null],"passed":false},{"actual":[0,1],"check":"equal","expected":[0,1],"passed":true},{"actual":[-1,1],"check":"narrower","expected":[-1,1],"passed":true},{"actual":[1,null],"check":"singleton expands right","expected":[1,null],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"lower expands alone\", \"actual\": [0, 1], \"expected\": [null, 1], \"passed\": false}, {\"check\": \"upper expands alone\", \"actual\": [0, null], \"expected\": [0, null], \"passed\": true}, {\"check\": \"both expand\", \"actual\": [0, null], \"expected\": [null, null], \"passed\": false}, {\"check\": \"equal\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"narrower\", \"actual\": [-1, 1], \"expected\": [-1, 1], \"passed\": true}, {\"check\": \"singleton expands right\", \"actual\": [1, null], \"expected\": [1, null], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":36.802,"exit_code":0,"observations":[{"actual":[null,1],"check":"lower expands alone","expected":[null,1],"passed":true},{"actual":[0,null],"check":"upper expands alone","expected":[0,null],"passed":true},{"actual":[null,null],"check":"both expand","expected":[null,null],"passed":true},{"actual":[0,1],"check":"equal","expected":[0,1],"passed":true},{"actual":[-1,1],"check":"narrower","expected":[-1,1],"passed":true},{"actual":[1,null],"check":"singleton expands right","expected":[1,null],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"lower expands alone\", \"actual\": [null, 1], \"expected\": [null, 1], \"passed\": true}, {\"check\": \"upper expands alone\", \"actual\": [0, null], \"expected\": [0, null], \"passed\": true}, {\"check\": \"both expand\", \"actual\": [null, null], \"expected\": [null, null], \"passed\": true}, {\"check\": \"equal\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"narrower\", \"actual\": [-1, 1], \"expected\": [-1, 1], \"passed\": true}, {\"check\": \"singleton expands right\", \"actual\": [1, null], \"expected\": [1, null], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}