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 BitwiseSolver {
    uint256 constant largeConstant = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
    event LogResult(uint256 result);
    constructor() {
        executeOperations(99);
    }
    function executeOperations(uint256 input) public {
        uint256 result = (input | largeConstant) & ~largeConstant;
        result = performShift(result + input);
        emit LogResult(result);
    }
    function performShift(uint256 value) internal pure returns (uint256) {
        for (uint8 i = 0; i < 256; i++) {
            value ^= (1 << i);
            if (i == 0) break;   // Ensures loop runs only once
        }
        return 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.