Commit 424d9c27 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

strategies: more robust detection of prover ambiguity

parent 658992fa
......@@ -154,11 +154,11 @@ let default_strategies =
"Inline", "Inline@ function@ symbols@ once", "i",
[|"t inline_goal 1"|];
"My mini-blaster", "A@ simple@ blaster", "b",
[|"c Alt-Ergo,0.95.2 1 1000";
"c CVC4,1.4 1 1000";
[|"c Alt-Ergo,0.95.2, 1 1000";
"c CVC4,1.4, 1 1000";
"t split_goal_wp 0";
"c Alt-Ergo,0.95.2 10 4000";
"c CVC4,1.4 10 4000" |];
"c Alt-Ergo,0.95.2, 10 4000";
"c CVC4,1.4, 10 4000" |];
]
let get_strategies rc =
......
......@@ -949,10 +949,15 @@ let convert_unknown_prover =
try
let fp = Whyconf.parse_filter_prover p in
Whyconf.filter_one_prover env.whyconf fp
with Whyconf.ProverNotFound _ ->
raise
(SyntaxError
("Prover " ^ p ^ " not installed or not configured"))
with
| Whyconf.ProverNotFound _ ->
raise
(SyntaxError
("Prover " ^ p ^ " not installed or not configured"))
| Whyconf.ProverAmbiguity _ ->
raise
(SyntaxError
("Prover description " ^ p ^ " is ambiguous"))
in
let timelimit =
try int_of_string t
......
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