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
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: