[exps] Add tests for arithmetic

tests/arithmetic.t

+  $ . ./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 ()

tests/dune

@@ -10,7 +10,21 @@
   (glob_files bin/*)
   filter_tmpdir.sh
   ../lib/xgboost/example/california.csv
-  ../lib/xgboost/example/california.json)
+  ../lib/xgboost/example/california.json
+  )
+ (package caisar))
+
+ (cram
+ (alias local)
+ (applies_to arithmetic)
+ (deps
+  (package caisar)
+  setup_env.sh
+  (glob_files bin/*)
+  filter_tmpdir.sh
+  ../examples/arithmetic/arithmetic.why
+  ../examples/arithmetic/FNN_s42.onnx
+  )
  (package caisar))
 
 (cram