You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: