Commit 264aa6e2 authored by David Hauzar's avatar David Hauzar Committed by MARCHE Claude

Cleanup.

parent cdc3ae4c
......@@ -379,17 +379,10 @@ let detect_exec env main data acc exec_name =
| Some prover_command ->
(** create the prover config *)
let c = make_command exec_name prover_command in
let c_steps = (match data.prover_command_steps with
| None -> None
| Some prover_command_steps ->
Some (make_command exec_name prover_command_steps)) in
(*
let c_steps = (match data.prover_command_steps with
| None -> ""
| Some prover_command_steps ->
(make_command exec_name prover_command_steps)) in *)
let prover = {Wc.prover_name = data.prover_name;
prover_version = ver;
prover_altern = data.prover_altern} in
......
......@@ -208,12 +208,10 @@ exception StepsCommandNotSpecified of string
let get_complete_command pc stepslimit =
let comm = if stepslimit < 0 then pc.command
else
else
match pc.command_steps with
| None -> raise (StepsCommandNotSpecified "The solver is used with step limit and the command for running the solver with steplimit is not specified.")
| Some command_steps -> command_steps in
(* pc.command_steps in *)
String.concat " " (comm :: pc.extra_options)
let set_limits m time mem running =
......@@ -719,19 +717,9 @@ let merge_config config filename =
let debug = Debug.register_info_flag "whyconf"
~desc:"Print@ debugging@ messages@ about@ whyconf."
let debug_print_commands key prover =
Debug.dprintf debug "Prover name = %s@." key.prover_name;
Debug.dprintf debug "Prover commad = %s@." prover.command;
match prover.command_steps with
| None -> Debug.dprintf debug "Steps command not given."
| Some (comm_steps) ->Debug.dprintf debug "Prover commad steps = %s@." comm_steps
let save_config config =
let filename = config.conf_file in
if filename <> "" then begin
Debug.dprintf debug "Prover configurations:@.";
Mprover.iter debug_print_commands config.provers;
Sysutil.backup_file filename;
to_file filename config.config
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment