SMT logic error from incorrect handling of fixed bytes to user defined value type conversion

[lum7na]

Hi! Compiling the following Solidity code with solc a.sol --model-checker-engine all results in a SMT logic error.

type MyBytes is bytes2;

contract C {
  MyBytes b = MyBytes.wrap("ab");
}

Output:

SMT logic error:
/solidity/libsmtutil/SolverInterface.h(393): Throw in function solidity::smtutil::Expression solidity::smtutil::operator==(Expression, 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

Both solc 0.8.29-develop.2025.2.25+commit.eb216716.Linux.g++, solc-0.8.27 and solc-0.8.28 can reproduce this bug.