Unsound results for configuration

[kkaulen]

Describe the bug
Given the following configuration, the solver returns an UNSAT result for every instance. However, two of the instances are actually SAT. I also tried this config with other models and, again, every instance was found to be UNSAT.

The configuration in question:

attack:
  pgd_order: middle
bab:
  branching:
    input_split:
      catch_assertion: true
      compare_with_old_bounds: true
      enable: true
    method: sb
model:
  name: mnist_conv_big
  path: models/eran/mnist_conv_big_diffai.pth
data:
  dataset: MNIST_ERAN
  start: 0
  end: 20
solver:
  bound_prop_method: crown
specification:
  epsilon: 0.3

To Reproduce
Save the above config under ./complete_verifier/faulty_config.yaml and run python3 abcrown.py --config ./faulty_config.yaml.

System configuration:

• OS: Rocky Linux 9.4 (Blue Onyx)
• Python version: 3.11.5
• Pytorch Version: 2.5.0
• Hardware: NVIDIA H100
• Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: Yes