# HG changeset patch # User wenzelm # Date 1558962531 -7200 # Node ID c7e9d3a0a681f73781febb6e8a825bfe724d4c1a # Parent bc9d02f916c4610882cf63a9ba342fb748156384 more direct invocation of Windows exe: avoid extra bash, cygpath, exec; diff -r bc9d02f916c4 -r c7e9d3a0a681 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon May 27 14:25:00 2019 +0200 +++ b/Admin/components/components.sha1 Mon May 27 15:08:51 2019 +0200 @@ -22,6 +22,7 @@ 541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz 1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz +ffb0d4739c10eb098eb092baef13eccf94a79bad cvc4-1.5-5.tar.gz 3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz 4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz @@ -302,5 +303,6 @@ 06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz 93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz b1bc411c2083fc01577070b56b94514676f53854 z3-4.4.0pre-2.tar.gz +4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz 517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz diff -r bc9d02f916c4 -r c7e9d3a0a681 Admin/components/main --- a/Admin/components/main Mon May 27 14:25:00 2019 +0200 +++ b/Admin/components/main Mon May 27 15:08:51 2019 +0200 @@ -2,7 +2,7 @@ bash_process-1.2.3 bib2xhtml-20190409 csdp-6.x -cvc4-1.5-4 +cvc4-1.5-5 e-2.0-2 isabelle_fonts-20190409 jdk-11.0.3+7 @@ -22,4 +22,4 @@ stack-1.9.3 vampire-4.2.2 xz-java-1.8 -z3-4.4.0pre-2 +z3-4.4.0pre-3 diff -r bc9d02f916c4 -r c7e9d3a0a681 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Mon May 27 14:25:00 2019 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon May 27 15:08:51 2019 +0200 @@ -49,7 +49,8 @@ local fun make_command command options problem_path proof_path = - Bash.strings (command () @ options) ^ " " ^ File.bash_path problem_path ^ + Bash.strings (command () @ options) ^ " " ^ + Bash.string (File.platform_path problem_path) ^ " > " ^ File.bash_path proof_path ^ " 2>&1" fun with_trace ctxt msg f x =