src/HOL/Tools/sat_solver.ML
changeset 15332 0dc05858a862
parent 15329 bd94b0a71dd2
child 15531 08c8dad8e399
--- a/src/HOL/Tools/sat_solver.ML	Thu Nov 25 14:38:37 2004 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Thu Nov 25 14:44:52 2004 +0100
@@ -515,13 +515,17 @@
 end;
 
 (* ------------------------------------------------------------------------- *)
-(* ZChaff, Version 2004.05.13 (http://www.princeton.edu/~chaff/zchaff.html)  *)
+(* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
 (* ------------------------------------------------------------------------- *)
 
 let
 	fun zchaff fm =
 	let
 		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
+		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
+		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
+			(* both versions of zChaff appear to have the same interface, so we do *)
+			(* not actually need to distinguish between them in the following code *)
 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
 		val outpath    = File.tmp_path (Path.unpack "result")
 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)