src/HOL/Tools/SMT2/smt2_systems.ML

     "-lang", "smtlib", "-output-lang", "presentation",
     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]
 in
 
 val cvc3: SMT2_Solver.solver_config = {
-  name = "cvc3_new",
+  name = "cvc3",
   class = K SMTLIB2_Interface.smtlib2C,
   avail = make_avail "CVC3_NEW",
   command = make_command "CVC3_NEW",
   options = cvc3_options,
   default_max_relevant = 400 (* FUDGE *),

 
 
 (* Yices *)
 
 val yices: SMT2_Solver.solver_config = {
-  name = "yices_new",
+  name = "yices",
   class = K SMTLIB2_Interface.smtlib2C,
   avail = make_avail "YICES_NEW",
   command = make_command "YICES_NEW",
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),

     if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C
     else SMTLIB2_Interface.smtlib2C
 in
 
 val z3: SMT2_Solver.solver_config = {
-  name = "z3_new",
+  name = "z3",
   class = select_class,
   avail = make_avail "Z3_NEW",
   command = z3_make_command "Z3_NEW",
   options = z3_options,
   default_max_relevant = 350 (* FUDGE *),