alpha-beta-crown behavior

[mhmd97z]

Hi,

I tried the following simple network to make sure I correctly understood alpha-beta-CROWN behavior.

Case 1:
(assert (or
(and (>= X_0 -1.0) (<= X_0 1.0) (>= X_1 0.5) (<= X_1 0.5) (<= Y_0 -0.6))
))
The true interval of y_0 is [-0.5, 0.5]. alpha-beta-CROWN returned safe.

Case 2:
(assert (or
(and (>= X_0 -1.0) (<= X_0 1.0) (>= X_1 0.5) (<= X_1 0.5) (>= Y_0 0.0))
))
The true interval of y_0 is [-0.5, 0.5]. alpha-beta-CROWN returned unknown.

The result of case 1 is as I expected, but I expected the result of case 2 to be unsafe as alpha-beta-crown is sound and complete. Please correct me if I am wrong but when two possible cases of the only Relu node are investigated and the corresponding bounds are calculated, I think we can give a definite response with regard to the violation or satisfaction of the defined property.

Here are the yaml config yaml.txt and the model model.txt in case you need them.

[mhmd97z]

I figured that it is needed to run the LP solver for each domain when all unstable nodes are split, but the result of BaB is not conclusive. I wanted to confirm with you batch_verification_all_node_split_LP method defined here is used for this purpose.
Thanks.