[Bug report]: Input pixels out of bound (violating constraints)

[paulsushmita]

Hi, there!

I was trying to reproduce some results from the VeriX project and started off with the MNIST script. However, I find that all of the pixels that result in a SAT response violate the bound constraints.

The output and experimentation results are detailed in an issue with Marabou that I just raised, since Marabou is the tool used in VeriX. The example detailed in the referred issue is the one from VeriX/mnist.py.

Looking forward to a response. Please feel free to let me know what is going wrong or if I could do something that could possibly fix the issue.

Best,
Sushmita

[paulsushmita]

Just realised there's an existing issue reported already! Just so you know, I have tested with various versions of Marabou, as mentioned in the Marabou GitHub issue referred in the previous comment:

Marabou installation via pip (v2.0.0) as well as GitHub's latest version, August '24 and April '24 versions.