Mmmm... the main problem I see here is that const-eval (or the interpreter) is only called to simplify expressions. For example, inside function foo, it is called to simplify the argument of the return. const-eval will not execute function foo because there is no expression calling function foo. As such, it will treat variable x in the return statement as uninterpreted.

To solve this issue, we would need some form of code analysis outside of const-eval. Another possibility would be to attempt calling functions that do not have parameters, just to check if its execution generates an error.
Probably, we will need an analysis/optimization pass after the typecheck pass, because currently, optimization and interpretation is only carried out on pieces of the code (in expressions, to be exact).

To solve this issue, we would need some form of code analysis outside of const-eval.

To solve this issue you need to partially evaluate contracts (I almost always mean partial evaluation or constant evaluation by "const-eval", sorry if that's confusing)

this fails too (explicit / 0 without "hiding" it):

contract EdgeCases {
    fun testShortCircuit(x: Int): Bool {
        return x != 0 || (x / 0 == 1);
    }

    receive () {
        self.testShortCircuit(1);
    }
}

LLM Fuzzing discovery (see #2490)

this fails too (explicit / 0 without "hiding" it):

contract EdgeCases {
fun testShortCircuit(x: Int): Bool {
return x != 0 || (x / 0 == 1);
}

receive () {
    self.testShortCircuit(1);
}

}

LLM Fuzzing discovery (see #2490)

In this one, FunC reports an error, but the program would not produce a division by zero at runtime, because testShortCircuit is called with parameter 1. However, if the parameter is 0, it would produce the division by zero at runtime.

Hence, I think that analyzing testShortCircuit in isolation should not issue an error, because it cannot determine that there is a division by zero with certainty, because the value of x is not known, and as such, one possible execution of || is safe, but the other one is not.

It will depend of what we want for the analyzer. Either: to report an error if there is a potential division by zero (as FunC does in this case), or to report an error only if there is a certain division by zero.