diff --git a/src/HOL/Tools/SMT/smt_systems.ML b/src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML
+++ b/src/HOL/Tools/SMT/smt_systems.ML
@@ -1,212 +1,214 @@
 (*  Title:      HOL/Tools/SMT/smt_systems.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Setup SMT solvers.
 *)
 
 signature SMT_SYSTEMS =
 sig
   val cvc4_extensions: bool Config.T
   val z3_extensions: bool Config.T
 end;
 
 structure SMT_Systems: SMT_SYSTEMS =
 struct
 
 (* helper functions *)
 
 fun check_tool var () =
   (case getenv var of
     "" => NONE
-  | s => if File.is_file (Path.variable var) then SOME [s] else NONE);
+  | s =>
+      if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe)
+      then SOME [s] else NONE);
 
 fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
 
 fun make_command name () = [getenv (name ^ "_SOLVER")]
 
 fun outcome_of unsat sat unknown timeout solver_name line =
   if String.isPrefix unsat line then SMT_Solver.Unsat
   else if String.isPrefix sat line then SMT_Solver.Sat
   else if String.isPrefix unknown line then SMT_Solver.Unknown
   else if String.isPrefix timeout line then SMT_Solver.Time_Out
   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
     " option for details"))
 
 fun is_blank_or_error_line "" = true
   | is_blank_or_error_line s = String.isPrefix "(error " s
 
 fun on_first_line test_outcome solver_name lines =
   let
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
     val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines)
   in (test_outcome solver_name l, ls) end
 
 fun on_first_non_unsupported_line test_outcome solver_name lines =
   on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
 
 (* CVC3 *)
 
 local
   fun cvc3_options ctxt = [
     "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
     "-lang", "smt2",
     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
 in
 
 val cvc3: SMT_Solver.solver_config = {
   name = "cvc3",
   class = K SMTLIB_Interface.smtlibC,
   avail = make_avail "CVC3",
   command = make_command "CVC3",
   options = cvc3_options,
   smt_options = [],
   default_max_relevant = 400 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = NONE,
   replay = NONE }
 
 end
 
 
 (* CVC4 *)
 
 val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false)
 
 local
   fun cvc4_options ctxt = [
     "--no-statistics",
     "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--lang=smt2",
     "--continued-execution",
     "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
 
   fun select_class ctxt =
     if Config.get ctxt cvc4_extensions then
       if Config.get ctxt SMT_Config.higher_order then
         CVC4_Interface.hosmtlib_cvc4C
       else
         CVC4_Interface.smtlib_cvc4C
     else
       if Config.get ctxt SMT_Config.higher_order then
         SMTLIB_Interface.hosmtlibC
       else
         SMTLIB_Interface.smtlibC
 in
 
 val cvc4: SMT_Solver.solver_config = {
   name = "cvc4",
   class = select_class,
   avail = make_avail "CVC4",
   command = make_command "CVC4",
   options = cvc4_options,
   smt_options = [(":produce-unsat-cores", "true")],
   default_max_relevant = 400 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
   replay = NONE }
 
 end
 
 
 (* veriT *)
 
 local
   fun select_class ctxt =
     if Config.get ctxt SMT_Config.higher_order then
       SMTLIB_Interface.hosmtlibC
     else
       SMTLIB_Interface.smtlibC
 in
 
 val veriT: SMT_Solver.solver_config = {
   name = "verit",
   class = select_class,
   avail = is_some o check_tool "ISABELLE_VERIT",
   command = the o check_tool "ISABELLE_VERIT",
   options = (fn ctxt => [
     "--proof-with-sharing",
     "--proof-define-skolems",
     "--proof-prune",
     "--proof-merge",
     "--disable-print-success",
     "--disable-banner",
     "--max-time=" ^ string_of_int (1000 * Real.ceil (Config.get ctxt SMT_Config.timeout))] @
     Verit_Proof.veriT_current_strategy (Context.Proof ctxt)),
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }
 
 end
 
 
 (* Z3 *)
 
 val z3_extensions = Attrib.setup_config_bool \<^binding>\<open>z3_extensions\<close> (K false)
 
 local
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
      "smt.refine_inj_axioms=false",
      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
      "-smt2"]
 
   fun select_class ctxt =
     if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
 in
 
 val z3: SMT_Solver.solver_config = {
   name = "z3",
   class = select_class,
   avail = make_avail "Z3",
   command = make_command "Z3",
   options = z3_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 350 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME Z3_Replay.parse_proof,
   replay = SOME Z3_Replay.replay }
 
 end
 
 (* smt tactic *)
 val parse_smt_options =
   Scan.optional
     (Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name)) >> apfst SOME)
     (NONE, NONE)
 
 fun smt_method ((solver, stgy), thms) ctxt facts =
   let
     val default_solver = SMT_Config.solver_of ctxt
     val solver = the_default default_solver solver
     val _ = 
       if solver = "z3" andalso stgy <> NONE
       then warning ("No strategy is available for z3. Ignoring " ^ quote (the stgy)) 
       else ()
     val ctxt =
       ctxt
       |> (if stgy <> NONE then Context.proof_map (Verit_Proof.select_veriT_stgy (the stgy)) else I)
       |> Context.Proof
       |> SMT_Config.select_solver solver
       |> Context.proof_of
   in
     HEADGOAL (SOLVED' (SMT_Solver.smt_tac ctxt (thms @ facts)))
   end
 
 val _ =
   Theory.setup
     (Method.setup \<^binding>\<open>smt\<close>
       (Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method))
       "Call to the SMT solvers veriT or z3")
 
 (* overall setup *)
 
 val _ = Theory.setup (
   SMT_Solver.add_solver cvc3 #>
   SMT_Solver.add_solver cvc4 #>
   SMT_Solver.add_solver veriT #>
   SMT_Solver.add_solver z3)
 
 end;
diff --git a/src/Pure/General/path.ML b/src/Pure/General/path.ML
--- a/src/Pure/General/path.ML
+++ b/src/Pure/General/path.ML
@@ -1,293 +1,296 @@
 (*  Title:      Pure/General/path.ML
     Author:     Markus Wenzel, TU Muenchen
 
 Algebra of file-system paths: basic POSIX notation, extended by named
 roots (e.g. //foo) and variables (e.g. $BAR).
 *)
 
 signature PATH =
 sig
   eqtype T
   val is_current: T -> bool
   val current: T
   val root: T
   val named_root: string -> T
   val parent: T
   val make: string list -> T
   val basic: string -> T
   val variable: string -> T
   val has_parent: T -> bool
   val is_absolute: T -> bool
   val is_basic: T -> bool
   val starts_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
   val implode: T -> string
   val explode: string -> T
   val explode_pos: string * Position.T -> T * Position.T
   val decode: T XML.Decode.T
   val split: string -> T list
   val pretty: T -> Pretty.T
   val print: T -> string
   val dir: T -> T
   val base: T -> T
   val ext: string -> T -> T
+  val platform_exe: T -> T
   val split_ext: T -> T * string
   val exe: T -> T
   val expand: T -> T
   val file_name: T -> string
   val implode_symbolic: T -> string
   val position: T -> Position.T
   eqtype binding
   val binding: T * Position.T -> binding
   val binding0: T -> binding
   val map_binding: (T -> T) -> binding -> binding
   val dest_binding: binding -> T * Position.T
   val path_of_binding: binding -> T
   val pos_of_binding: binding -> Position.T
   val proper_binding: binding -> unit
   val implode_binding: binding -> string
   val explode_binding: string * Position.T -> binding
   val explode_binding0: string -> binding
 end;
 
 structure Path: PATH =
 struct
 
 (* path elements *)
 
 datatype elem =
   Root of string |
   Basic of string |
   Variable of string |
   Parent;
 
 local
 
 fun err_elem msg s = error (msg ^ " path element " ^ quote s);
 
 val illegal_elem = ["", "~", "~~", ".", ".."];
 val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
 
 fun check_elem s =
   if member (op =) illegal_elem s then err_elem "Illegal" s
   else
     (s, ()) |-> fold_string (fn c => fn () =>
       if ord c < 32 then
         err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s
       else if member (op =) illegal_char c then
         err_elem ("Illegal character " ^ quote c ^ " in") s
       else ());
 
 in
 
 val root_elem = Root o tap check_elem;
 val basic_elem = Basic o tap check_elem;
 val variable_elem = Variable o tap check_elem;
 
 end;
 
 
 (* type path *)
 
 datatype T = Path of elem list;    (*reversed elements*)
 
 fun rep (Path xs) = xs;
 
 fun is_current (Path []) = true
   | is_current _ = false;
 
 val current = Path [];
 val root = Path [Root ""];
 fun named_root s = Path [root_elem s];
 val make = Path o rev o map basic_elem;
 fun basic s = Path [basic_elem s];
 fun variable s = Path [variable_elem s];
 val parent = Path [Parent];
 
 fun has_parent (Path xs) = exists (fn Parent => true | _ => false) xs;
 
 fun is_absolute (Path xs) =
   (case try List.last xs of
     SOME (Root _) => true
   | _ => false);
 
 fun is_basic (Path [Basic _]) = true
   | is_basic _ = false;
 
 fun all_basic (Path elems) =
   forall (fn Basic _ => true | _ => false) elems;
 
 fun starts_basic (Path xs) =
   (case try List.last xs of
     SOME (Basic _) => true
   | _ => false);
 
 
 (* append and norm *)
 
 fun apply (y as Root _) _ = [y]
   | apply Parent (xs as (Root _ :: _)) = xs
   | apply Parent (Basic _ :: rest) = rest
   | apply y xs = y :: xs;
 
 fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
 fun appends paths = Library.foldl (uncurry append) (current, paths);
 
 fun norm elems = fold_rev apply elems [];
 
 
 (* implode *)
 
 local
 
 fun implode_elem (Root "") = ""
   | implode_elem (Root s) = "//" ^ s
   | implode_elem (Basic s) = s
   | implode_elem (Variable s) = "$" ^ s
   | implode_elem Parent = "..";
 
 in
 
 fun implode_path (Path []) = "."
   | implode_path (Path [Root ""]) = "/"
   | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs));
 
 end;
 
 
 (* explode *)
 
 fun explode_path str =
   let
     fun explode_elem s =
      (if s = ".." then Parent
       else if s = "~" then Variable "USER_HOME"
       else if s = "~~" then Variable "ISABELLE_HOME"
       else
         (case try (unprefix "$") s of
           SOME s' => variable_elem s'
         | NONE => basic_elem s))
       handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str);
 
     val (roots, raw_elems) =
       (case chop_prefix (equal "") (space_explode "/" str) |>> length of
         (0, es) => ([], es)
       | (1, es) => ([Root ""], es)
       | (_, []) => ([Root ""], [])
       | (_, e :: es) => ([root_elem e], es));
     val elems = raw_elems |> filter_out (fn c => c = "" orelse c = ".") |> map explode_elem;
 
   in Path (norm (rev elems @ roots)) end;
 
 fun explode_pos (s, pos) =
   (explode_path s handle ERROR msg => error (msg ^ Position.here pos), pos);
 
 fun split str =
   space_explode ":" str
   |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
 
 val decode = XML.Decode.string #> explode_path;
 
 
 (* print *)
 
 fun pretty path =
   let val s = implode_path path
   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
 
 val print = Pretty.unformatted_string_of o pretty;
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 
 (* base element *)
 
 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
   | split_path _ path = error ("Cannot split path into dir/base: " ^ print path);
 
 val dir = split_path #1;
 val base = split_path (fn (_, s) => Path [Basic s]);
 
 fun ext "" = I
   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
 
+val platform_exe = ML_System.platform_is_windows ? ext "exe";
+
 val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
   (case chop_suffix (fn c => c <> ".") (raw_explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
 val exe = ML_System.platform_is_windows ? ext "exe";
 
 
 (* expand variables *)
 
 fun eval (Variable s) =
       let val path = explode_path (getenv_strict s) in
         if exists (fn Variable _ => true | _ => false) (rep path) then
           error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path)
         else rep path
       end
   | eval x = [x];
 
 val expand = rep #> maps eval #> norm #> Path;
 
 val file_name = implode_path o base o expand;
 
 
 (* implode wrt. given directories *)
 
 fun implode_symbolic path =
   let
     val directories = rev (space_explode ":" (getenv "ISABELLE_DIRECTORIES"));
     val full_name = implode_path (expand path);
     fun fold_path a =
       (case try (implode_path o expand o explode_path) a of
         SOME b =>
           if full_name = b then SOME a
           else
             (case try (unprefix (b ^ "/")) full_name of
               SOME name => SOME (a ^ "/" ^ name)
             | NONE => NONE)
       | NONE => NONE);
   in
     (case get_first fold_path directories of
       SOME name => name
     | NONE => implode_path path)
   end;
 
 val position = Position.file o implode_symbolic;
 
 
 (* binding: strictly monotonic path with position *)
 
 datatype binding = Binding of T * Position.T;
 
 fun binding (path, pos) =
   if all_basic path then Binding (path, pos)
   else error ("Bad path binding: " ^ print path ^ Position.here pos);
 
 fun binding0 path = binding (path, Position.none);
 
 fun map_binding f (Binding (path, pos)) = binding (f path, pos);
 
 fun dest_binding (Binding args) = args;
 val path_of_binding = dest_binding #> #1;
 val pos_of_binding = dest_binding #> #2;
 
 fun proper_binding binding =
   if is_current (path_of_binding binding)
   then error ("Empty path" ^ Position.here (pos_of_binding binding))
   else ();
 
 val implode_binding = path_of_binding #> implode_path;
 
 val explode_binding = binding o explode_pos;
 fun explode_binding0 s = explode_binding (s, Position.none);
 
 
 (*final declarations of this structure!*)
 val implode = implode_path;
 val explode = explode_path;
 
 end;