Enabling smtlib2+bmc in the model-checker results in an internal compiler error.

[lum7na]

Hello! I encountered an internal compiler error when using the solc compiler version 0.8.27 to compile the following code. My compilation command was: solc-0.8.27 a.sol --model-checker-solvers smtlib2 --model-checker-engine bmc.

contract Test {

  uint256 public A;
  uint256 public constant B = 1;

  function g() public returns(uint256) {
      A >>= ((B & 0x3f) + B * 64) - 112;
      return 1;
  }
}

Output:

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

I compiled a new version of solc (71988f7) for testing, and the error persists.