diff --git a/flake.nix b/flake.nix index 446cfa466a483caef04d98b75dac7bbbd535986c..2d40836c459f2a9840deb95b55ddc83c9c4c0204 100644 --- a/flake.nix +++ b/flake.nix @@ -119,3 +119,4 @@ }; }); } + diff --git a/src/convert_xgboost.ml b/src/convert_xgboost.ml index 9ca4cd6056fb8ca77f1493b03a8ca8b93da6bfed..c9bfb87374c5d40eab8a79fc7d4bd3c8e9a6e800 100644 --- a/src/convert_xgboost.ml +++ b/src/convert_xgboost.ml @@ -236,7 +236,7 @@ let prove_and_print ?memlimit ?timelimit env config prover task = let def = Why3.Call_provers.empty_limit in { Why3.Call_provers.limit_time = timelimit; - limit_steps = Option.value ~default:def.limit_steps None; + limit_steps = def.limit_steps ; limit_mem = memlimit; } in diff --git a/src/verification.ml b/src/verification.ml index 2c1b3d19a324d9a24654331de0a3b57b1c4bc693..cc3a089dc70fcdc96fd28546fb6a6beca8a7a779 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -435,7 +435,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern let def = Call_provers.empty_limit in { Call_provers.limit_time = timelimit; - Call_provers.limit_steps = Option.value ~default:def.limit_steps None; + Call_provers.limit_steps = def.limit_steps; Call_provers.limit_mem = memlimit; } in @@ -467,15 +467,14 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern else Fmt.(any " " ++ parens string)) altern) in + let driver_str = snd config_prover.driver in + let driver = Re__Core.replace_string re_config ~by:config_site driver_str in let driver = - Re__Core.replace_string re_config ~by:config_site (snd config_prover.driver) - in - let driver = - if String.equal driver (snd config_prover.driver) + if String.equal driver driver_str then Driver.load_driver_for_prover main env config_prover else Driver.load_driver_file_and_extras main env ~extra_dir:None driver - config_prover.extra_drivers + config_prover.extra_drivers in let cwd, mstr_theory = open_file ?format env file in let verification_result =