A possible bug with NARv

[huangi27]

Hello,

Thank you for the great tool. When I tried it with my models and properties (after fixing a simple bug - see the patch), I found a strange behavior: the tool outputs UNSAT for a trivially valid property y0 <= y0, regardless of whether the abstraction is turned on or not. The following steps can reproduce this behavior:

1. Put the model ACASXU_experimental_v2a_g_2.nnet at /home/artifact/Marabou/resources/nnet/acasxu
2. Apply the patch property.patch to fix a bug and add a property test
3. Run any of the following commands:
   python3 narv.py -nn g_2 -pid test -m marabou -a global -r global
python3 narv.py -nn g_2 -pid test -m marabou_with_ar -a global -r global

It would be great if you could have a look at this issue. Thank you again for your time and help :-)
ACASXU_experimental_v2a_g_2.nnet.txt
property.patch.txt
@jiaxiangliu

[jiaxiangliu]

Hi @huangi27 , thanks for your feedback and sorry for my late reply.

If the behavior remains even when the abstraction is disabled, it is probably an issue from the backend solver Marabou instead of NARv. I will try to look deeper into it and give you more information.