SMTChecker triggers an ICE by not reporting Arithmetic error when computing constant value fatal error caused by constant addition

[Subway2023]

Environment

• Compiler version: 0.8.27
• Target EVM version (as per compiler settings): None
• Framework/IDE (e.g. Truffle or Remix): None
• EVM execution environment / backend / blockchain client: None
• Operating system: Linux

Steps to Reproduce

// SPDX-License-Identifier: MIT
contract BugDetection {
    uint256 public storedValue;
    uint8 constant MAX_UINT8 = 255;
    function storeShiftedValue(uint256 input) public {
        // Inline assembly to manipulate bits directly
        assembly {
            let shifted := shl(2, input) // Shift left by 2, may overflow if input is not managed
            sstore(storedValue.slot, shifted) // Store the shifted value to storedValue
        }
        storedValue = computeHashWithSideEffect(uint8(storedValue % (MAX_UINT8 + 1)));
    }
    function computeHashWithSideEffect(uint8 input) internal returns (uint256) {
        // Function with potential side-effect in the expression
        uint8 interimValue = input;
        bytes32 hash = keccak256(abi.encodePacked(interimValue + modifyState()));
        return uint256(hash);
    }
    function modifyState() internal returns (uint8) {
        storedValue = storedValue + 1; // Intentional side-effect to modify state
        return 1; // Return a small constant value
    }
}

solc-0827 b.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine chc --model-checker-solvers z3   --model-checker-show-unproved 

Internal compiler error:
/solidity/libsolidity/interface/CompilerStack.cpp(502): Throw in function bool solidity::frontend::CompilerStack::analyze()
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Unreported fatal error: std::exception
[solidity::util::tag_comment*] = Unreported fatal error: std::exception

However, the program can be successfully compiled into bytecode.

[cameel]

As in #15600, the fact that this runs into Unreported fatal error is a bug in itself, and needs a fix.

Here's the underlying error that triggers it:

Unreported fatal error:
/solidity/liblangutil/ErrorReporter.cpp(143): Throw in function void solidity::langutil::ErrorReporter::fatalError(solidity::langutil::ErrorId, solidity::langutil::Error::Type, const solidity::langutil::SourceLocation&, const std::string&)
Dynamic exception type: boost::wrapexcept<solidity::langutil::FatalError>
std::exception::what: Arithmetic error when computing constant value.
[solidity::util::tag_comment*] = Arithmetic error when computing constant value.

Internal compiler error:
/solidity/libsolidity/interface/CompilerStack.cpp(516): Throw in function bool solidity::frontend::CompilerStack::analyze()
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Unreported fatal error.
[solidity::util::tag_comment*] = Unreported fatal error.

Minimized repro:

contract C {
    uint8 constant N = 255;

    function f() public {
        N + 1;
    }
}

The underlying cause looks the same as in #15600 (i.e. #15709).