# HG changeset patch
# User desharna
# Date 1633616897 -7200
# Node ID fd5f62176987041396115c9a8554c8f5458089b2
# Parent  6424c54157d94cd157567438f1a376c23d625223# Parent  409ca22dee4c6f0f485fc30661671254f4a72360
merged

diff -r 409ca22dee4c -r fd5f62176987 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Oct 06 14:19:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Oct 07 16:28:17 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 = {