src/HOL/Tools/SMT/smt_systems.ML

   parse_proof = NONE,
   replay = NONE }
 
 end
 
+
 (* CVC4 *)
 
 val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
 
 local

     "--lang=smt2",
     "--continued-execution",
     "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
 
   fun select_class ctxt =
-    if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
-    else SMTLIB_Interface.smtlibC
+    if Config.get ctxt cvc4_extensions then
+      if Config.get ctxt SMT_Config.higher_order then
+        CVC4_Interface.hosmtlib_cvc4C
+      else
+        CVC4_Interface.smtlib_cvc4C
+    else
+      if Config.get ctxt SMT_Config.higher_order then
+        SMTLIB_Interface.hosmtlibC
+      else
+        SMTLIB_Interface.smtlibC
 in
 
 val cvc4: SMT_Solver.solver_config = {
   name = "cvc4",
   class = select_class,

   parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
   replay = NONE }
 
 end
 
+
 (* veriT *)
+
+local
+  fun select_class ctxt =
+    if Config.get ctxt SMT_Config.higher_order then
+      SMTLIB_Interface.hosmtlibC
+    else
+      SMTLIB_Interface.smtlibC
+in
 
 val veriT: SMT_Solver.solver_config = {
   name = "verit",
-  class = K SMTLIB_Interface.smtlibC,
+  class = select_class,
   avail = make_avail "VERIT",
   command = make_command "VERIT",
   options = (fn ctxt => [
     "--proof-version=1",
     "--proof-prune",

   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = NONE }
+
+end
+
 
 (* Z3 *)
 
 val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)