[NN_prover] Add bounds to all inputs since nn provers requires it

    - But it is not very pretty in the debug output

src/transformations/native_nn_prover.ml

@@ -292,7 +292,31 @@ let abstract_nn_term env =
           %a" Why3.Pretty.print_ls var (Number.print_int_constant
           Number.full_support) out.old_index out.new_index (Fmt.list
           ~sep:Fmt.comma Why3.Pretty.print_term) out.old_nn_args);*)
-
+        (* Add bounds for all inputs *)
+        let task =
+          Why3.Term.Mls.fold_left
+            (fun task ls _ ->
+              let task =
+                Why3.Task.add_prop_decl task Paxiom
+                  (Why3.Decl.create_prsymbol @@ Why3.Ident.id_fresh "min_bound")
+                  (Why3.Term.ps_app th_float64.le
+                     [
+                       Utils.term_of_float env (-.Float.max_finite_value);
+                       Why3.Term.fs_app ls [] th_float64.ty;
+                     ])
+              in
+              let task =
+                Why3.Task.add_prop_decl task Paxiom
+                  (Why3.Decl.create_prsymbol @@ Why3.Ident.id_fresh "max_bound")
+                  (Why3.Term.ps_app th_float64.le
+                     [
+                       Why3.Term.fs_app ls [] th_float64.ty;
+                       Utils.term_of_float env Float.max_finite_value;
+                     ])
+              in
+              task)
+            task input_vars
+        in
         (* Add meta for outputs *)
         let task =
           Why3.Term.Mterm.fold_left