Skip to content
Snippets Groups Projects
Commit 951c9866 authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

minor formatting and simplifications

parent 428b5996
No related branches found
No related tags found
No related merge requests found
...@@ -119,3 +119,4 @@ ...@@ -119,3 +119,4 @@
}; };
}); });
} }
...@@ -236,7 +236,7 @@ let prove_and_print ?memlimit ?timelimit env config prover task = ...@@ -236,7 +236,7 @@ let prove_and_print ?memlimit ?timelimit env config prover task =
let def = Why3.Call_provers.empty_limit in let def = Why3.Call_provers.empty_limit in
{ {
Why3.Call_provers.limit_time = timelimit; Why3.Call_provers.limit_time = timelimit;
limit_steps = Option.value ~default:def.limit_steps None; limit_steps = def.limit_steps ;
limit_mem = memlimit; limit_mem = memlimit;
} }
in in
......
...@@ -435,7 +435,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern ...@@ -435,7 +435,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
let def = Call_provers.empty_limit in let def = Call_provers.empty_limit in
{ {
Call_provers.limit_time = timelimit; 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; Call_provers.limit_mem = memlimit;
} }
in in
...@@ -467,15 +467,14 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern ...@@ -467,15 +467,14 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
else Fmt.(any " " ++ parens string)) else Fmt.(any " " ++ parens string))
altern) altern)
in 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 = let driver =
Re__Core.replace_string re_config ~by:config_site (snd config_prover.driver) if String.equal driver driver_str
in
let driver =
if String.equal driver (snd config_prover.driver)
then Driver.load_driver_for_prover main env config_prover then Driver.load_driver_for_prover main env config_prover
else else
Driver.load_driver_file_and_extras main env ~extra_dir:None driver Driver.load_driver_file_and_extras main env ~extra_dir:None driver
config_prover.extra_drivers config_prover.extra_drivers
in in
let cwd, mstr_theory = open_file ?format env file in let cwd, mstr_theory = open_file ?format env file in
let verification_result = let verification_result =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment