arithmetic.t 1022 B
$ . ./setup_env.sh
$ caisar verify --prover PyRAT --ltag=ProverSpec --ltag=StackTrace --ltag=InterpretGoal --goal :runP1\'vc --define model_filename:FNN_s42.onnx ../examples/arithmetic/arithmetic.why
[DEBUG]{InterpretGoal} Interpreted formula for goal 'runP1'vc':
forall x:t, x1:t, x2:t.
(le ((- 5.0):t) x /\ le x (5.0:t)) /\
(le ((- 5.0):t) x1 /\ le x1 (5.0:t)) /\ le ((- 5.0):t) x2 /\ le x2 (5.0:t) ->
le (add RNE (add RNE (sub RNE (nn_onnx @@ vector x x1 x2)[0] x) x1) x2)
(0.5:t)
vector, 3
nn_onnx,
(Interpreter_types.Model
(Interpreter_types.ONNX, { Language.nn_nb_inputs = 3; nn_nb_outputs = 1;
nn_ty_elt = t;
nn_filename =
"../examples/arithmetic/FNN_s42.onnx";
nn_format = <nir> }))
[DEBUG]{ProverSpec} Prover-tailored specification:
-5.0 <= x0
x0 <= 5.0
-5.0 <= x1
x1 <= 5.0
-5.0 <= x2
x2 <= 5.0
y0 <= 0.5
Goal runP1'vc: Unknown ()