SMTChecker: ICE when passing a string literal to ecrecover()

[Jizhou-Chen]

Description

Error:

SMT logic error:
/solidity/libsmtutil/Z3Interface.cpp(276): Throw in function z3::expr solidity::smtutil::Z3Interface::toZ3Expr(const solidity::smtutil::Expression&)
Dynamic exception type: boost::wrapexcept<solidity::smtutil::SMTLogicError>
std::exception::what: Sort mismatch at argument #3 for function (declare-fun ecrecover_input_type (Int Int Int Int) ecrecover_input_type) supplied sort is bytes_tuple
[solidity::util::tag_comment*] = Sort mismatch at argument #3 for function (declare-fun ecrecover_input_type (Int Int Int Int) ecrecover_input_type) supplied sort is bytes_tuple

Note: This bug was found in #11587 (comment) and marked as done in May, 2024. However, it still exists in the latest release (v0.8.28), hence this report.

Environment

• Compiler version: Version: 0.8.28-develop.2025.1.19+commit.7893614a.mod.Linux.g++
• Compilation pipeline (legacy, IR, EOF):
• Target EVM version (as per compiler settings):
• Framework/IDE (e.g. Foundry, Hardhat, Remix):
• EVM execution environment / backend / blockchain client:
• Operating system: Ubuntu 22.04

Steps to Reproduce

poc.sol (fuzzer-generated):

pragma experimental SMTChecker;

contract C {
	function foo() internal { 2; }
	function s(bytes memory b0) public pure {
		bytes memory b1 = b0;
		bytes32 s0 = sha256(b0);
		bytes32 s1 = sha256(b1);
		assert(s0 == s1);
	}
	function r(bytes memory b0) public pure {
		bytes memory b1 = b0;
		bytes32 r0 = ripemd160(b0);
		bytes32 r1 = ripemd160(b1);
		assert(r0 == r1);
	}
	function e(bytes32 h0, uint8 v0, bytes32 r0, bytes32 s0) public pure {
		(bytes32 h1, uint8 v1, bytes32 r1, bytes32 s1) = (h0, v0, r0, s0);
		address a0 = ecrecover(h0, v0, "t", s0);
		address a1 = ecrecover(h1, v1, r1, s1);
		assert(a0 == a1);
	}
}

To reproduce:
solc --bin -o poc poc.sol

[Jizhou-Chen]

Note: This bug is also gone with the latest develop commit: 0.8.29-develop.2025.1.21+commit.ed71f949.mod.Linux.g++.

[blishko]

This example does not crash anymore on current develop, but the SMT encoding is still incorrect.
I have a fix for that prepared.

[cameel]

I can confirm as well that this does happen on 0.8.28 but not on current develop.

For the record, the ICE is triggered by simply passing in a string literal to ecrecover(). This is a more compact repro:

contract C {
    function f() public pure {
        ecrecover(0, 0, "", 0);
    }
}

BTW, please remember to update the titles of such issues after they're triaged and the cause is known. Having actually relevant info there makes life much easier when searching for stuff (even if the issue is closed or unimportant - it at least makes that clear without having to open it :)).