# HG changeset patch
# User blanchet
# Date 1297791178 -3600
# Node ID 26dab6eca1c23119a482f7ae819969a2382951e6
# Parent  d323edd12b501165d6a9071f455e3080308cc592
make experimental "Z3 ATP" work on Linux as well

diff -r d323edd12b50 -r 26dab6eca1c2 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 15 10:03:10 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 15 18:32:58 2011 +0100
@@ -237,7 +237,7 @@
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn timeout => fn _ =>
-     "MBQI=true /p /t:" ^ string_of_int (to_secs 0 timeout),
+     "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
    has_incomplete_mode = false,
    proof_delims = [],
    known_failures =