Strict inequality warning shows on specification that does not contain strict inequalities

[BenCoke12]

Specification: https://github.com/BenCoke12/monotonic-nets/blob/main/specifications/nonDual.vcl Network: https://github.com/BenCoke12/monotonic-nets/blob/main/onnx/1nYeX.onnx

Command used: vehicle verify --specification specifications/nonDual.vcl --network regression:onnx/1nYeX.onnx --verifier Marabou --verifier-location ../Marabou/build/Marabou

The verifier shows the warning even though there are no strict inequalities in the script:

Warning: While compiling property 'highInHighOut' at least one of the generated SAT problems generated was found to contain a strict inequality (i.e. constraints of the form 'x < y'). Unfortunately the Marabou query format only supports non-strict inequalities (i.e. constraints of the form 'x <= y').

In order to provide support, Vehicle has automatically converted the strict inequalities to non-strict inequalites. This is not sound, but errors will be at most the floating point epsilon used by the verifier, which is usually very small (e.g. 1e-9). However, this may lead to unexpected behaviour (e.g. loss of the law of excluded middle).

See https://github.com/vehicle-lang/vehicle/issues/74 for further details.

The counterexample generated (0.5) is also not a counterexample to the property as it would need to be a value less than 0.5 to be a counterexample.

[wenkokke]

Given the negation translation and other such steps, we probably should decorate this warning with similar information to the linearity violations.