Genuine, unique divergence — fixed in the engine and merged. +1 on the leaderboard.
Exact-source static and manual injection screens passed. Pre-fix checked executable lowering fails; EVM raw return is uint256 1, no events, outer length slot 0=1. Restricted source-pinned post replay agrees; independent checked regressions verify both return and storage. Full Lean build passed 2327 jobs and all contest samples passed; earlier direct-return regression remains green. Earlier #113 does not eliminate this local-initializer report. Merged main tree matches validated candidate.
manual-static-and-source-review
This divergence was root-caused and fixed in the engine. Fixed in PR #121 →
The push-returned array length was supported only in direct returns. Local initializers did not capture the appended storage reference or preserve the declared local across the following statement sequence. Add atomic alias/length initialization and splice the declared local into sequence scope.
// SPDX-License-Identifier: MIT
pragma solidity 0.8.35;
/* ===ARENA-MANIFEST===
{"deploy":{"contract":"C","args":[],"value":0},"entry":{"function":"run","args":[],"value":0},"lane":"C","feature":"push-return-length-local-initializer","fuel":4096}
===END-ARENA-MANIFEST=== */
contract C {
uint256[][] values;
function run() external returns (uint256) {
uint256 length = values.push().length;
return length + values.length;
}
}