[Eva] Minor simplifications when using Integer.to_int[_opt].

src/plugins/value/partitioning/partition.ml

@@ -336,15 +336,11 @@ struct
 
   let eval_exp_to_int state exp =
     let _valuation, ival = evaluate_exp_to_ival state exp in
-    try
-      match Integer.to_int_opt (Ival.project_int ival) with
-      | Some i -> i
-      | None -> fail ~exp "this partitioning parameter overflows an integer"
+    try Integer.to_int (Ival.project_int ival)
     with
     | Ival.Not_Singleton_Int ->
       fail ~exp "this partitioning parameter must evaluate to a singleton"
-    | Failure _ ->
-      fail ~exp "this partitioning parameter is too big"
+    | Z.Overflow -> fail ~exp "this partitioning parameter overflows an integer"
 
   let split_by_predicate state predicate =
     let env =

src/plugins/value/partitioning/partitioning_parameters.ml

@@ -93,19 +93,11 @@ struct
         let t =
           Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
         in
-        match Logic_utils.constFoldTermToInt t with
-        | Some n ->
-          begin
-            match Integer.to_int_opt n with
-            | Some n' -> Partition.IntLimit n'
-            | None ->
-              warn "invalid loop unrolling parameter (%a); ignoring"
-                (Integer.pretty ~hexa:false) n;
-              default
-          end
-        | None   ->
-          try
-            Partition.ExpLimit (term_to_exp t)
+        let i = Logic_utils.constFoldTermToInt t in
+        match Option.bind i Integer.to_int_opt with
+        | Some n -> Partition.IntLimit n
+        | None ->
+          try Partition.ExpLimit (term_to_exp t)
           with Db.Properties.Interp.No_conversion ->
             warn "loop unrolling parameters must be valid expressions; \
                   ignoring";