Bug with SSBP verification strategy #39
Description
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):
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.