Test verify $ chmod u+x bin/pyrat.py $ bin/pyrat.py --version PyRAT 1.1 $ PATH=$(pwd)/bin:$PATH $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh > theory PyRAT_ONNX > use ieee_float.Float64 > use bool.Bool > use int.Int > use interpretation.Vector > use interpretation.NeuralNetwork > > constant nn: nn = read_neural_network "TestNetworkONNX.onnx" ONNX > > goal G: > forall i: vector t. > has_length i 3 -> > (0.0:t) .<= i[0] .<= (0.5:t) -> > (0.0:t) .< (nn@@i)[0] .< (0.5:t) > end > EOF [DEBUG]{ProverSpec} Prover-tailored specification: 0.0 <= x0 x0 <= 0.5 0.0 < y0 and y0 < 0.5 Goal G: Unknown ()