# HG changeset patch
# User blanchet
# Date 1402478926 -7200
# Node ID 5d61d875076a90c2dd03f21a7ae3513ce64cab2d
# Parent  7ffa0f7e277531863ee1916b566cff279eef959f
rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions

diff -r 7ffa0f7e2775 -r 5d61d875076a 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=" ^