src/HOL/Tools/SMT/smt_systems.ML
changeset 58491 5ddbc170e46c
parent 58360 dee1fd1cc631
child 58496 2ba52ecc4996
equal deleted inserted replaced
58490:f6d99c69dae9 58491:5ddbc170e46c
   110     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
   110     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
   111   smt_options = [],
   111   smt_options = [],
   112   default_max_relevant = 120 (* FUDGE *),
   112   default_max_relevant = 120 (* FUDGE *),
   113   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
   113   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
   114     "warning : proof_done: status is still open"),
   114     "warning : proof_done: status is still open"),
   115   parse_proof = SOME VeriT_Proof_Parse.parse_proof,
   115   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   116   replay = NONE }
   116   replay = NONE }
   117 
   117 
   118 (* Z3 *)
   118 (* Z3 *)
   119 
   119 
   120 datatype z3_non_commercial =
   120 datatype z3_non_commercial =