diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t
index 9bbd9c34302db2729aa58e6cd47c225b3452ef42..a4b7da5b39b81992f31c555f155e387246dbdde9 100644
--- a/tests/nier_to_onnx.t
+++ b/tests/nier_to_onnx.t
@@ -23,6 +23,32 @@ Test verify
   [DEBUG]{NIR} Wrote NIR as ONNX in file 'out/nn_onnx.nir.onnx'
   Goal G: Unknown ()
 
+Data should be 0.135
+
+  $ python3 bin/inspect_onnx.py
+  out/nn_onnx.nir.onnx has 1 input nodes
+  {'name': '0', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '1'}, {'dimValue': '1'}, {'dimValue': '1'}, {'dimValue': '3'}]}}}}
+  1 files checked
+
+  $ caisar verify --format whyml --prover=PyRAT --ltag=NIR --onnx-out-dir="out_nnet" - 2>&1 <<EOF
+  > theory NIER_to_ONNX
+  >   use ieee_float.Float64
+  >   use caisar.types.Vector
+  >   use caisar.model.Model
+  >   use caisar.model.NN
+  >
+  >   constant nn: model nn = read_model "TestNetwork.nnet"
+  >
+  >   goal G:
+  >     forall i: vector t.
+  >       has_length i 5 ->
+  >       (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_nnet/nn_onnx.nir.onnx'
+  Goal G: Unknown ()
+
 Data should be 0.135
 
   $ python3 bin/inspect_onnx.py