Solidity: [SMTChecker] SMT logic error during analysis: throw in static solidity::smtutil::Expression solidity::smtutil::Expression::int2bv(solidity::smtutil::Expression, size_t)

[agroce]

Description

This contract:

pragma experimental SMTChecker;
contract Simp {
    function f3() public pure returns (bytes memory r) {
        bytes memory y = "def";
        y[0] ^ "e";
    }
}

produces:

SMT logic error during analysis:
/home/user/solidity/libsmtutil/SolverInterface.h(203): Throw in function static solidity::smtutil::Expression solidity::smtutil::Expression::int2bv(solidity::smtutil::Expression, size_t)
Dynamic exception type: boost::exception_detail::clone_impl<solidity::smtutil::SMTLogicError>
std::exception::what: 
[solidity::util::tag_comment*] = 

when compiled with solc

On master, using AFL fuzzing. Another discovery using https://github.com/agroce/afl-compiler-fuzzer.

Environment

• Compiler version: Version: 0.6.9-develop.2020.6.2+commit.17e20409.Linux.clang
• Target EVM version (as per compiler settings): N/A
• Framework/IDE (e.g. Truffle or Remix): N/A
• EVM execution environment / backend / blockchain client: N/A
• Operating system: Ubuntu 18.04 in docker

Steps to Reproduce

Above shows pretty clearly, I think.

[bshastry]

This may be a duplicate of #9087

[leonardoalt]

Let's keep both open for now and check whether the first fix fixes both.