1.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Nov 28 13:58:12 2013 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Nov 28 15:14:00 2013 +0100
1.3 @@ -31,7 +31,6 @@
1.4 (* for compatibility with "SatSolver" *)
1.5 val berkmin_exec = getenv "BERKMIN_EXE"
1.6
1.7 -(* (string * sat_solver_info) list *)
1.8 val static_list =
1.9 [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
1.10 ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
1.11 @@ -44,6 +43,7 @@
1.12 "Instance Unsatisfiable")),
1.13 ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
1.14 "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
1.15 + ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
1.16 ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
1.17 if berkmin_exec = "" then "BerkMin561"
1.18 else berkmin_exec, [], "Satisfiable !!",