ICE in SolverInterface.cpp: Trying to create an 'equal' expression with different sorts

[haoyang9804]

Description

Reproducible Code:

contract contract0 {
  error error1();

  struct struct2 {
    mapping(int8 => int8) mapping3;
  }

  mapping(int8 => int8) internal mapping11;
  string internal var6;

  constructor() {
    int8 var8;
    (var8 *= var8);
  }

  function func7() internal {
    bool var9;
    struct2 storage struct_instance10;
    struct_instance10 = struct_instance10;
    (var9 ? (mapping11) : struct_instance10.mapping3);
  }
}

contract contract14 {
  struct struct15 {
    contract0 contract_instance16;
  }

  bool[6] internal array17;
  int8 internal var19;

  function func21() internal returns (mapping(uint64 => contract0) storage mapping22, mapping(bool => string) storage mapping25) {
    mapping22 = mapping22;
    mapping25 = mapping25;
    do {} while(!(array17[(uint128(3))]));
  }
}

Compilation Command

../AFLs/new-solidity/build/solc/solc generated_programs/program_2024-12-16_16:50:51_37.sol --asm --yul-optimizations UrInSdDjov --optimize-runs 8 --optimize-yul --optimize --model-checker-show-proved-safe --model-checker-show-unsupported --model-checker-targets overflow --model-checker-engine all --model-checker-ext-calls trusted --model-checker-invariants all --via-ir

Error message:

SMT logic error:
/solidity/libsmtutil/SolverInterface.h(393): Throw in function solidity::smtutil::Expression solidity::smtutil::operator==(solidity::smtutil::Expression, solidity::smtutil::Expression)
Dynamic exception type: boost::wrapexcept<solidity::smtutil::SMTLogicError>
std::exception::what: Trying to create an 'equal' expression with different sorts
[solidity::util::tag_comment*] = Trying to create an 'equal' expression with different sorts

Environment

• Compiler version:0.8.29-develop.2024.11.30+commit.b4ecc58b.Linux.g++