Description
The verification strategy occasionally crashes when verifying certain networks with specific properties. The error is triggered by an assert / raise Exception in algorithms.py (lines 390–400). According to the comments in the code, this branch should never be reached, but in practice it is.
Relevant code section (algorithms.py, 390–400):
"""
else:
# There is no more refinement to do, i.e., all neurons have been fixed.
# We can end up here because the bounds might not be aware that all neurons have been fixed.
# So there can be some over-approximation.
# We should detect and throw more exact intersection check
input_num_bounds = nn_bounds.numeric_pre_bounds[self.network.get_first_node().identifier]
self.logger.info(f"\tBranch {current_star.fixed_neurons} is inconsistent with bounds, "
f"input {input_num_bounds.get_lower()} {input_num_bounds.get_upper()}")
raise Exception("This point should not be reachable")
"""
Observed behavior
The verifier crashes with Exception("This point should not be reachable").
This happens only for some network/property pairs.
For example, with the attached network and property (rename .txt to .onnx and .vnnlib respectively):
30.txt
sample_0006_label_4_eps_0.030.txt
Steps to reproduce
Load the attached network and property.
Run the verification strategy sslbp
Observe the crash in algorithms.py.
Description
The verification strategy occasionally crashes when verifying certain networks with specific properties. The error is triggered by an assert / raise Exception in algorithms.py (lines 390–400). According to the comments in the code, this branch should never be reached, but in practice it is.
Relevant code section (algorithms.py, 390–400):
"""
else:
# There is no more refinement to do, i.e., all neurons have been fixed.
# We can end up here because the bounds might not be aware that all neurons have been fixed.
# So there can be some over-approximation.
# We should detect and throw more exact intersection check
input_num_bounds = nn_bounds.numeric_pre_bounds[self.network.get_first_node().identifier]
"""
Observed behavior
The verifier crashes with Exception("This point should not be reachable").
This happens only for some network/property pairs.
For example, with the attached network and property (rename .txt to .onnx and .vnnlib respectively):
30.txt
sample_0006_label_4_eps_0.030.txt
Steps to reproduce
Load the attached network and property.
Run the verification strategy sslbp
Observe the crash in algorithms.py.