{"abstract":"Division strength reduction rounds negative dividends downward.","category":"Compiler transformation correctness","checks":7,"contract":"Lower signed mathematical integer division by 2**shift, shift>=0, returning truncation toward zero. No finite-width overflow is modeled.","evaluation_group":"model-f45a5e496f869e3a","failed_approach":"Adding a bias to every dividend corrupts positive nonmultiples.","family":"z-compilers-division-shift","id":"FA-11466","implementations":{"attempt":{"sha256":"bbbd376cbb180f1a62d2a4bfbb61d45b9759cc3e1857271d8d751d01a5b3a423","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(value, shift):\n    return (value + (1 << shift) - 1) >> shift\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('negative nonmultiple', solve(-(2**N+1),N), -1)\ncheck('positive nonmultiple', solve(2**N+1,N), 1)\ncheck('negative exact', solve(-2**N,N), -1)\ncheck('positive exact', solve(2**N,N), 1)\ncheck('zero', solve(0,N), 0)\ncheck('identity shift', solve(-N,0), -N)\ncheck('small negative', solve(-1,N), 0)\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":"546e69a352f42e2a86cdea85a3f41f4f19b8e58ca9ee9e813b5f025d68fd47ad","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(value, shift):\n    return value >> shift\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('negative nonmultiple', solve(-(2**N+1),N), -1)\ncheck('positive nonmultiple', solve(2**N+1,N), 1)\ncheck('negative exact', solve(-2**N,N), -1)\ncheck('positive exact', solve(2**N,N), 1)\ncheck('zero', solve(0,N), 0)\ncheck('identity shift', solve(-N,0), -N)\ncheck('small negative', solve(-1,N), 0)\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":"42913d6074f5a590d2c971c8bb7ff10282939e6cd7493bb6ba756e8bb097e65c","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(value, shift):\n    return (value + ((1 << shift) - 1 if value < 0 else 0)) >> shift\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('negative nonmultiple', solve(-(2**N+1),N), -1)\ncheck('positive nonmultiple', solve(2**N+1,N), 1)\ncheck('negative exact', solve(-2**N,N), -1)\ncheck('positive exact', solve(2**N,N), 1)\ncheck('zero', solve(0,N), 0)\ncheck('identity shift', solve(-N,0), -N)\ncheck('small negative', solve(-1,N), 0)\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-compilers-division-shift","generated_at":"2026-09-29T14:38:48.112340+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A deterministic miniature compiler-pass model; inputs are explicit IR facts, not a production compiler.","repair":"Bias negative dividends before arithmetic shifting to preserve truncation toward zero.","root_cause":"Signed truncating division by a power of two is replaced by arithmetic shift.","sha256":"ddf302cfc1296cb74c083c30e87afc70aaf99e70c1c8d86d703ca823e42031e0","title":"Division strength reduction rounds negative dividends downward · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":38.481,"exit_code":1,"observations":[{"actual":-1,"check":"negative nonmultiple","expected":-1,"passed":true},{"actual":2,"check":"positive nonmultiple","expected":1,"passed":false},{"actual":-1,"check":"negative exact","expected":-1,"passed":true},{"actual":1,"check":"positive exact","expected":1,"passed":true},{"actual":0,"check":"zero","expected":0,"passed":true},{"actual":-1,"check":"identity shift","expected":-1,"passed":true},{"actual":0,"check":"small negative","expected":0,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"negative nonmultiple\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"positive nonmultiple\", \"actual\": 2, \"expected\": 1, \"passed\": false}, {\"check\": \"negative exact\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"positive exact\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"zero\", \"actual\": 0, \"expected\": 0, \"passed\": true}, {\"check\": \"identity shift\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"small negative\", \"actual\": 0, \"expected\": 0, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":39.697,"exit_code":1,"observations":[{"actual":-2,"check":"negative nonmultiple","expected":-1,"passed":false},{"actual":1,"check":"positive nonmultiple","expected":1,"passed":true},{"actual":-1,"check":"negative exact","expected":-1,"passed":true},{"actual":1,"check":"positive exact","expected":1,"passed":true},{"actual":0,"check":"zero","expected":0,"passed":true},{"actual":-1,"check":"identity shift","expected":-1,"passed":true},{"actual":-1,"check":"small negative","expected":0,"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"negative nonmultiple\", \"actual\": -2, \"expected\": -1, \"passed\": false}, {\"check\": \"positive nonmultiple\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"negative exact\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"positive exact\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"zero\", \"actual\": 0, \"expected\": 0, \"passed\": true}, {\"check\": \"identity shift\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"small negative\", \"actual\": -1, \"expected\": 0, \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":36.934,"exit_code":0,"observations":[{"actual":-1,"check":"negative nonmultiple","expected":-1,"passed":true},{"actual":1,"check":"positive nonmultiple","expected":1,"passed":true},{"actual":-1,"check":"negative exact","expected":-1,"passed":true},{"actual":1,"check":"positive exact","expected":1,"passed":true},{"actual":0,"check":"zero","expected":0,"passed":true},{"actual":-1,"check":"identity shift","expected":-1,"passed":true},{"actual":0,"check":"small negative","expected":0,"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"negative nonmultiple\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"positive nonmultiple\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"negative exact\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"positive exact\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"zero\", \"actual\": 0, \"expected\": 0, \"passed\": true}, {\"check\": \"identity shift\", \"actual\": -1, \"expected\": -1, \"passed\": true}, {\"check\": \"small negative\", \"actual\": 0, \"expected\": 0, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}