diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml index 9dc56a4aa9d5e088f2cc6580bb72f6b49f2aa622..78b80a60185f378f23fe8626a61d5e9f8bb729a0 100644 --- a/src/plugins/value/partitioning/partition.ml +++ b/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 = diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml index 567f2b5f2cb64bb356516463eabb68910ddbb627..1c8dae31e042b527e8e036cf404045966d193176 100644 --- a/src/plugins/value/partitioning/partitioning_parameters.ml +++ b/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";