SMT logic error for a conditional with empty tuple types

[alex1448]

Description

The following code triggers the exception shown bellow. I tested this locally with the latest compiler version 0.8.24 and then I tested on remix for older versions. The problem seems to appear with version 0.7.5 but with a different kind of exception: SMTLogicException: out of memory. For versions >=0.8.17 the exception is: SMTLogicException: parser error (full compiler output bellow).

Steps to Reproduce

testcase.sol

// SPDX-License-Identifier: GPL-3.0

pragma solidity =0.8.24;

contract C {
    function f() public pure {
        true ? () : ();
    }
}

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

SMT logic error:
./libsmtutil/Z3Interface.cpp(179): Throw in function z3::expr solidity::smtutil::Z3Interface::toZ3Expr(const solidity::smtutil::Expression&)
Dynamic exception type: boost::wrapexcept<solidity::smtutil::SMTLogicError>
std::exception::what: parser error
[solidity::util::tag_comment*] = parser error

Environment

• Compiler version: >=0.7.5