1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Feb 18 10:26:48 2009 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Feb 24 16:12:27 2009 +0100
     1.3 @@ -914,10 +914,6 @@
     1.4    fun zchaff fm =
     1.5    let
     1.6      val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
     1.7 -    val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
     1.8 -                        (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
     1.9 -      (* both versions of zChaff appear to have the same interface, so we do *)
    1.10 -      (* not actually need to distinguish between them in the following code *)
    1.11      val serial_str = serial_string ()
    1.12      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.13      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.14 @@ -943,11 +939,12 @@
    1.15  let
    1.16    fun berkmin fm =
    1.17    let
    1.18 -    val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.19 +    val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.20      val serial_str = serial_string ()
    1.21      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.22      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.23 -    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.24 +    val exec       = getenv "BERKMIN_EXE"
    1.25 +    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.26      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.27      fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.28      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()