Commit 7e478a08 authored by Sylvain Dailler's avatar Sylvain Dailler

Added None argument to Driver.prove_task where necessary to make things

compile.
parent 51c0880b
......@@ -96,7 +96,7 @@ let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task1)
alt_ergo_driver None task1)
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@."
......@@ -106,7 +106,7 @@ let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10}
alt_ergo_driver task2)
alt_ergo_driver None task2)
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
Call_provers.print_prover_answer result1.Call_provers.pr_answer
......@@ -144,7 +144,7 @@ let result3 =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task3)
alt_ergo_driver None task3)
let () = printf "@[On task 3, alt-ergo answers %a@."
Call_provers.print_prover_result result3
......@@ -174,7 +174,7 @@ let result4 =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task4)
alt_ergo_driver None task4)
let () = printf "@[On task 4, alt-ergo answers %a@."
Call_provers.print_prover_result result4
......
......@@ -1305,10 +1305,11 @@ let why3tac ?(timelimit=timelimit) s gl =
let cp, drv = get_prover s in
let command = String.concat " " (cp.command :: cp.extra_options) in
if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
if debug then Format.printf "@[%a@]@\n---@."
(fun fmt -> Driver.print_task drv fmt None) !task;
let limit =
{ Call_provers.empty_limit with Call_provers.limit_time = timelimit } in
let call = Driver.prove_task ~command ~limit drv !task in
let call = Driver.prove_task ~command ~limit drv None !task in
wait_on_call call
with
| NotFO ->
......
......@@ -139,7 +139,7 @@ module Task =
let task_to_string t =
ignore (flush_str_formatter ());
Driver.print_task alt_ergo_driver str_formatter t;
Driver.print_task alt_ergo_driver str_formatter None t;
flush_str_formatter ()
let gen_id =
......
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