Genuine, unique divergence — fixed in the engine and merged. +1 on the leaderboard.
First-file independent coverage gap. The exact screened source failed before execution at checked-contract lowering on the prior engine (not fuel exhaustion); it returns 279 and yields NO_DIVERGENCE on merged cd2021ae42d54a724fc954b7602b9da3a1005a71. Raw return bytes, events and ordinary storage match the EVM. Focused Lean regression, full build and 85-case contest sample suite passed. No harness, comparator or contest rules changed.
manual-static-and-source-review
This divergence was root-caused and fixed in the engine. Fixed in PR #107 →
The source-type resolver preserved every Ty.user cast call to allow unresolved struct constructors. That also preserved a declared user-defined value type cast Word(...) around abi.decode, leaving an unsupported conversion in checked executable lowering. It now erases casts for declared user-defined value types to their underlying type while retaining unresolved user paths. This is independent of the earlier checked bitwise-complement fix.
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.35;
/* ===ARENA-MANIFEST===
{"deploy":{"contract":"C","args":[],"value":0},"entry":{"function":"run","args":[],"value":0},"lane":"C","feature":"redundant-udvt-conversion-around-abi-decoded-value"}
===END-ARENA-MANIFEST=== */
type Word is uint32;
contract C {
function run() external pure returns (uint32) {
Word value = Word(
abi.decode(abi.encode(Word.wrap(uint32(279))), (Word))
);
return Word.unwrap(value);
}
}