NeuralNetworkVerification/Marabou

Assertion Violation in ReluConstraint::getPossibleFixes()

OmriIsacHUJI opened this issue · 0 comments

When running some queries with --prove-unsat flag, they lead to an assertion violation in ReluConstraint::getPossibleFixes(), specifically in line 384:
ASSERT( !FloatUtils::isNegative( fValue ) );
This issues can be reproduced by querying Marabou with ACAS_XU network 3_7 property 4, with the --prove-unsat flag.

While this problem arises when using proofs, it seems to me it is not directly connected to them (fixing PL constraints is not connected to the proofs directly). Moreover, when printing the violating variable, its values are violating by a very small gap (-0.00000005). This may suggest a numerical issue.