src/HOL/Tools/SMT/smt_setup_solvers.ML

   env_var = "CVC3_SOLVER",
   is_remote = true,
   options = (fn ctxt => [
     "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
     "-lang", "smtlib", "-output-lang", "presentation"]),
-  interface = SMTLIB_Interface.interface,
+  class = SMTLIB_Interface.smtlibC,
   outcome =
     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
   cex_parser = NONE,
   reconstruct = NONE,
   default_max_relevant = 250 }

   env_var = "YICES_SOLVER",
   is_remote = false,
   options = (fn ctxt => [
     "--rand-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--smtlib"]),
-  interface = SMTLIB_Interface.interface,
+  class = SMTLIB_Interface.smtlibC,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
   reconstruct = NONE,
   default_max_relevant = 275 }
 

 fun z3 () = {
   name = "z3",
   env_var = "Z3_SOLVER",
   is_remote = true,
   options = z3_options,
-  interface = Z3_Interface.interface,
+  class = Z3_Interface.smtlib_z3C,
   outcome = z3_on_last_line,
   cex_parser = SOME Z3_Model.parse_counterex,
   reconstruct = SOME Z3_Proof_Reconstruction.reconstruct,
   default_max_relevant = 225 }