--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 12 17:02:02 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 12 17:02:03 2014 +0200
@@ -28,7 +28,6 @@
open Sledgehammer
(* val cvc3N = "cvc3" *)
-val yicesN = "yices"
val z3N = "z3"
val runN = "run"
@@ -204,15 +203,13 @@
end
fun remotify_prover_if_not_installed ctxt name =
- if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
- SOME name
- else
- remotify_prover_if_supported_and_not_already_remote ctxt name
+ if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
+ else remotify_prover_if_supported_and_not_already_remote ctxt name
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put E first. *)
fun default_provers_param_value mode ctxt =
- [eN, spassN, z3N, e_sineN, vampireN, yicesN]
+ [eN, spassN, z3N, e_sineN, vampireN]
|> map_filter (remotify_prover_if_not_installed ctxt)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))