--- a/src/HOL/Tools/SMT/smt_systems.ML Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Thu Oct 07 10:16:52 2021 +0200
@@ -112,7 +112,10 @@
"--proof-merge",
"--disable-print-success",
"--disable-banner"] @
- Verit_Proof.veriT_current_strategy (Context.Proof ctxt)
+ Verit_Proof.veriT_current_strategy (Context.Proof ctxt) @
+ (case SMT_Config.get_timeout ctxt of
+ NONE => []
+ | SOME t => ["--max-time " ^ string_of_int (Time.toMilliseconds t)])
in
val veriT: SMT_Solver.solver_config = {