Return statement in @Pure functions

[etiennebirling]

Hello
it seems that Nagini tolerates some pure functions for which not all path end with a return statement. While I initially suspected that it would be part of the features, I think I finally found some inconsistent behavior.
For instance:

• Nagini complains that the return statement is missing here:

@Pure
def purefunction(i: int) -> int:
    y = 18
    if(i > 0):
        y = y + 1
        return 3
    elif(i < 0):
        return 0
    else:
        y = y * 2
        
@ContractOnly
def compare3(b: int) -> int:
    Requires(purefunction(1) == 3)
    Ensures(Result() > 13)

• But not here:

@Pure
def purefunction(i: int) -> int:
    y = 18
    if(i > 0):
        y = y + 1
    elif(i < 0):
        return 0
    else:
        y = y * 2
        return 3

@ContractOnly
def compare3(b: int) -> int:
    Requires(purefunction(1) == 3)
    Ensures(Result() > 13)

Any idea of what this can be?