# HG changeset patch
# User webertj
# Date 1101390292 -3600
# Node ID 0dc05858a862f64e9c6a8661ddd787f18de130eb
# Parent  3e85549f25f5314de9c577126aaf1975d1d4afe6
added ZCHAFF_VERSION

diff -r 3e85549f25f5 -r 0dc05858a862 src/HOL/Tools/sat_solver.ML
--- 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)