SMTChecker: Internal compiler error in BMC analysis of loop condition

[lum7na]

Description

Hi! Solc throws an internal compiler error within UniqueErrorReporter.h when enabling model-checker. I attempted to minimize the reproduction code, but it seems that removing any single expression prevents triggering this exception.

Compile: solc-latest a.sol --model-checker-engine all

contract Test {
  function test(string memory str) private returns(string memory) {
    bytes memory s = bytes(str);
    if (s.length > 0) {
      bool b = true;
      for (uint i = 0;i < s.length; i++) {
        if (s[i] != hex"20") {
          b = false;
          break;
        }
      }
      if (b) {
        return hex"";
      } else {
        bytes memory t = new bytes(s.length);
        uint j = 0;
        for (uint i = 0;i < s.length; i++) {
          if (s[i] != hex"20") {
            j++;
          }
        }
        bytes memory r = new bytes(j);
        for (uint k = 0; 0 < ((((r[1] == hex"7e" ? j : 0) != k ? 0 : j) == 2) ? 45 : j); k++) {
          r[k] = t[k];
        }
        return string(r);
      }
    }
    return str;
  }
}

Output:

Internal compiler error:
/solidity/liblangutil/UniqueErrorReporter.h(87): Throw in function bool solidity::langutil::UniqueErrorReporter::seen(solidity::langutil::ErrorId, const solidity::langutil::SourceLocation&, const std::string&) const
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Solidity assertion failed
[solidity::util::tag_comment*] = Solidity assertion failed

Solc version: Version: 0.8.29-develop.2025.2.11+commit.c3152941.Linux.g++

[blishko]

Here is the simplified example:

contract Test {
    function loop() public {
        for (uint k = 0; (k == 0 ? true : false); k++) {
        }
    }
}

The error is triggered in the BMC analysis of the loop condition (option --model-checker-engine bmc).