# HG changeset patch
# User blanchet
# Date 1317038623 -7200
# Node ID eb7a797ade0f225f55de97b16a0655cd33d4e25e
# Parent  91d1a932fc18facfba69b122fe123fa95ee3186d
put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes

diff -r 91d1a932fc18 -r eb7a797ade0f src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 26 11:41:52 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 26 14:03:43 2011 +0200
@@ -31,12 +31,12 @@
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
+  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+                           "UNSAT")),
+   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
    ("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
-   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
-                           "UNSAT")),
-   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),