From 951c98669d7ee9b5b2c48c31125e6652d451f63b Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Fri, 12 Jul 2024 15:32:21 +0200
Subject: [PATCH] minor formatting and simplifications
---
flake.nix | 1 +
src/convert_xgboost.ml | 2 +-
src/verification.ml | 11 +++++------
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/flake.nix b/flake.nix
index 446cfa4..2d40836 100644
--- a/flake.nix
+++ b/flake.nix
@@ -119,3 +119,4 @@
};
});
}
+
diff --git a/src/convert_xgboost.ml b/src/convert_xgboost.ml
index 9ca4cd6..c9bfb87 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 2c1b3d1..cc3a089 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 =
--
GitLab