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

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

[cameel]

Minimized repro:

contract C {
    uint256 public constant B = 1;

    function f() public {
        B - 112;
    }
}

This is yet another case similar to #15600 and #15601. Both are caused by #15709.

Note that the fact that this is an internal compiler error and not just a normal compilation error is a separate bug. After we merge #15807 the output will be a bit more informative:

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.

But ultimately it shouldn't be reported like this.