Commit 8fc6fcff authored by MARCHE Claude's avatar MARCHE Claude

fixed CHANGES

check if driver failed to load in use_api.ml
parent 75f9e888
...@@ -2,8 +2,10 @@ ...@@ -2,8 +2,10 @@
o WhyML with mutable record fields and type models o WhyML with mutable record fields and type models
o why3replayer o why3replayer
* "logic" is not a keyword anymore, use "function" and "predicate" * "parameter" keyword renamed to "val"
* new syntax for conjunction (/\) and disjunction (\/) * new syntax for conjunction (/\) and disjunction (\/)
("and" and "or" do not exist anymore)
* "logic" is not a keyword anymore, use "function" and "predicate"
* functions to create an environment are now exported from Env * functions to create an environment are now exported from Env
o [IDE] bug 12244 resolved by using Task.task_equal o [IDE] bug 12244 resolved by using Task.task_equal
o fixed Alt-ergo output: no triggers for "exists" quantifier o fixed Alt-ergo output: no triggers for "exists" quantifier
......
...@@ -89,7 +89,12 @@ let env : Env.env = ...@@ -89,7 +89,12 @@ let env : Env.env =
(* loading the Alt-Ergo driver *) (* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver = let alt_ergo_driver : Driver.driver =
try
Driver.load_driver env alt_ergo.Whyconf.driver Driver.load_driver env alt_ergo.Whyconf.driver
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
(* call Alt-Ergo *) (* call Alt-Ergo *)
let result1 : Call_provers.prover_result = let result1 : Call_provers.prover_result =
......
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