Test verify $ . ./setup_env.sh $ bin/pyrat.py --version PyRAT 1.1 $ caisar verify --format whyml --prover=PyRAT --ltag=NIER --onnx-out-dir="out" - 2>&1 <<EOF | ./filter_tmpdir.sh > theory NIER_to_ONNX > use ieee_float.Float64 > use bool.Bool > use int.Int > use vector.Vector > use nn.NeuralNetwork > > constant nn: nn = read_model "TestNetworkONNX.onnx" ONNX > > goal G: > forall i: vector t. > has_length i 3 -> > (0.5:t) .<= i[0] .<= (0.5:t) -> > (0.5:t) .< (nn@@i)[0] .< (0.5:t) > end > EOF [DEBUG]{NIER} Wrote NIER as ONNX in file 'out/onnx_nn.nier.onnx' Goal G: Unknown () Data should be 0.135 $ python3 bin/inspect_onnx.py Initializer name 12 has data 0.135