merged
authordesharna
Thu, 07 Oct 2021 16:28:17 +0200
changeset 74477 fd5f62176987
parent 74476 6424c54157d9 (diff)
parent 74475 409ca22dee4c (current diff)
child 74487 f8ad2ee7638d
merged
--- 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 = {