SMTChecker：Internal compiler error

[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.