`myth analyze`: Solidity program without assert triggers an assertion violation

[sbauer00]

Description

I have seen multiple instances where I get spurious assertion violation warnings when using myth analyze. One of the best examples is a Solidity program without any assert statements that triggers this warning when compiled with the right solc flags.

How to Reproduce

Program

pragma solidity ^0.8.19;

contract PlaceholderContract {
    function externalized_0(
        bool assert_in4,
        bool assert_in5
    ) internal returns (bool) {
        return (assert_in4 && assert_in5);
    }

    function externalized_1(
        bool assert_in4,
        bool assert_in5
    ) internal returns (bool) {
        return (externalized_0(assert_in4, assert_in5) && false);
    }

    function externalized_2() internal returns (bool) {
        return ((true ||
            ((!(!true)) ||
                (true ||
                    (true &&
                        ((!(!true)) &&
                            (((!(!false)) || (false && true)) &&
                                (true && (!false)))))))) &&
            ((false ||
                ((true || true) &&
                    ((!(!true)) && ((!(!(false && true))) && (!false))))) &&
                ((((true || (true || true)) && false) && false) ||
                    ((true || true) &&
                        ((!(!false)) &&
                            ((!(!(!(!true)))) && (!(!(!(!true))))))))));
    }

    function check_entrypoint(
        int256 assert_in0,
        int256 assert_in1,
        int256 assert_in2,
        bool assert_in3,
        bool assert_in4,
        bool assert_in5,
        bool assert_in6
    ) public {
        unchecked {
            bool assert_out1 = externalized_1(assert_in4, assert_in5);
            bool assert_out2 = (externalized_2() ||
                ((true ||
                    (((!(!true)) && (!(!true))) ||
                        (false ||
                            (true ||
                                (true &&
                                    ((!(!true)) &&
                                        ((((!(!false)) && (!false)) && true) &&
                                            ((!false) || false)))))))) &&
                    ((false ||
                        (true &&
                            ((!(!true)) &&
                                (((!(!(false && true))) && (!false)) ||
                                    false)))) &&
                        ((false && ((true || (true || true)) && false)) ||
                            ((true || true) && ((!(!false)) && (!(!true))))))));
        }
    }
}

Compile Options

solc --optimize --optimize-runs 100000 --via-ir --evm-version london --yul-optimizations "vhcTVF[ex]vg[nllvTIc]ToCxp[DpctI]:IUo" --bin-runtime

Mythril Call

$ myth analyze -c <bytecode>
==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: MAIN
Function name: fallback
PC address: 0
An assertion violation was triggered.
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
-------------------
$

Expected behavior

The analysis was completed successfully. No issues were detected.

Environment

• Mythril version: v0.24.8
• Solidity compiler and version: 0.8.29+commit.ab55807c.Darwin.appleclang
• Python version: Python 3.13.3
• OS and Version: macOS 15.5

However this is also reproducible on linux x86-64 with the same Solidity compiler and Mythril versions.

Additional Environment or Context

Bytecode for reference https://gist.github.com/sbauer00/860bad12ab2d9b7382df391e08dff962