ICE in SolverInterface: SMT assertion failed

[haoyang9804]

Description

Reproducible program

contract contract0 {
  error error1(int128 var2);

  error error3();

  mapping(bool => uint256) internal mapping4;
  bool[1] public array7;

  constructor(int128[] memory array10) {
    ((mapping4[array7[(0)]]) /= (mapping4[(bool(false))]));
  }

  function func12() internal view returns (string memory var13) {
    var13 = var13;
    (mapping4[array7[uint256(0)]] >> mapping4[true]);
    string memory var15;
    var15 = var15;
    return ((var15));
  }

  function func14() internal view {
    uint256 var16;
    do {} while(this.array7(mapping4[array7[var16]]));
    return ();
  }
}

contract contract17 {
  error error18(string var19);

  string internal var20;

  function func21(int128 var22) internal returns (address var23, uint256[] memory array24) {
    array24 = array24;
    bool var26;
    (!(var26));
  }
}

Compilation command

../AFLs/new-solidity/build/solc/solc generated_programs/program_2024-12-18_4:13:35_37.sol --storage-layout --yul-optimizations aiMEesrIOnfTlpdghjDUCvLFtm --optimize-yul --optimize-runs 6 --model-checker-engine chc --model-checker-ext-calls trusted --model-checker-invariants all --model-checker-show-unproved --via-ir

Error message:

SMT logic error:
/solidity/libsmtutil/SolverInterface.h(285): Throw in function static solidity::smtutil::Expression solidity::smtutil::Expression::int2bv(solidity::smtutil::Expression, size_t)
Dynamic exception type: boost::wrapexcept<solidity::smtutil::SMTLogicError>
std::exception::what: SMT assertion failed
[solidity::util::tag_comment*] = SMT assertion failed

Environment

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