Why does bab return 'unknown' instead of 'unsafe' when all nodes are split?

[mathisdon]

https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/bab.py

In bab.py, in function general_bab, there is a loop over bab "rounds" (lines 295-330). In that loop, one termination condition is that all nodes have been split, in which case it returns 'unknown'. But shouldn't that be "unsafe'?, since all nodes have been split and yet it has been unable to verify the point?

You have this code inside the loop, line 319:

    result = None
    if stats.all_node_split:
        stats.all_node_split = False
        result = 'unknown'
    elif num_domains > max_domains:
        print('Maximum number of visited domains has reached.')
        result = 'unknown'
    elif time.time() - start_time > timeout:
        print('Time out!!!!!!!!')
        result = 'unknown'
    if result:
        break