rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
authorblanchet
Wed, 11 Jun 2014 11:28:46 +0200
changeset 57210 5d61d875076a
parent 57209 7ffa0f7e2775
child 57211 cc59d49bdf64
rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jun 11 11:28:46 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jun 11 11:28:46 2014 +0200
@@ -51,8 +51,8 @@
 val cvc3: SMT2_Solver.solver_config = {
   name = "cvc3",
   class = K SMTLIB2_Interface.smtlib2C,
-  avail = make_avail "CVC3_NEW",
-  command = make_command "CVC3_NEW",
+  avail = make_avail "CVC3",
+  command = make_command "CVC3",
   options = cvc3_options,
   default_max_relevant = 400 (* FUDGE *),
   outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -67,8 +67,8 @@
 val yices: SMT2_Solver.solver_config = {
   name = "yices",
   class = K SMTLIB2_Interface.smtlib2C,
-  avail = make_avail "YICES_NEW",
-  command = make_command "YICES_NEW",
+  avail = make_avail "YICES",
+  command = make_command "YICES",
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
     "--timeout=" ^