# HG changeset patch
# User blanchet
# Date 1385648040 -3600
# Node ID 48dadf69c44d77f03a7107419468fdfa2d823ed2
# Parent  a8ad7f6dd217f8595f8a4d5c7f72e7a7a3c3b801
added Riss3g

diff -r a8ad7f6dd217 -r 48dadf69c44d src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Nov 28 13:58:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Nov 28 15:14:00 2013 +0100
@@ -31,7 +31,6 @@
 (* for compatibility with "SatSolver" *)
 val berkmin_exec = getenv "BERKMIN_EXE"
 
-(* (string * sat_solver_info) list *)
 val static_list =
   [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
    ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
@@ -44,6 +43,7 @@
                           "Instance Unsatisfiable")),
    ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
                         "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
+   ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
                            if berkmin_exec = "" then "BerkMin561"
                            else berkmin_exec, [], "Satisfiable          !!",