SMT logic error for mapping index access with a string literal

[alex1448]

Description

The following code triggers the exception shown bellow. I tested this locally with compiler version 0.8.23 and later I tested on remix for older versions. I found that the problem starts to appear with version 0.8.20 (just like with issue #14791).

Steps to Reproduce

testcase.sol

// SPDX-License-Identifier: GPL-3.0

pragma solidity =0.8.23;

contract C {
    mapping(bytes14 => bytes15) internal v;

    function f() public payable {
      delete v["A"];

      // delete v[bytes14("A")];  // this is ok
      // v["A"];  // this is ok
    }
}

solc testcase.sol --model-checker-engine all

SMT logic error:
./libsmtutil/SolverInterface.h(238): Throw in function static solidity::smtutil::Expression solidity::smtutil::Expression::store(solidity::smtutil::Expression, solidity::smtutil::Expression, solidity::smtutil::Expression)
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.20

[alex1448]

I think this issue still remains for other types. The following causes the same exception.

// SPDX-License-Identifier: GPL-3.0

pragma solidity =0.8.25;

contract C {
    mapping(int => int) v;

    function f() public {
      delete v[0];
    }
}

[r0qs]

I can confirm that the issue persists, so I'm reopening it.