Michele Alberti authored 10 months ago and Aymeric Varasse committed 9 months ago

Add also a test for it (copy the one for Marabou).

François Bobot authored 11 months ago and Michele Alberti committed 9 months ago

   So an invariant for normal formula is that application of nn are always of the shape `nn@@vv[cst]`

François Bobot authored 11 months ago and Michele Alberti committed 9 months ago

    But (y * 56) + 12 < 34 is not handled

Once negated, consider the conjunctive normal form (CNF) of the goal if it is
not printable as is. This prevents failures on formula which are OK besides
their form. Indeed, CNF is logically equivalent to the original formula.

     when $CAISAR_ONNX_OUTPUT_DIR is specified