# HG changeset patch
# User desharna
# Date 1633594612 -7200
# Node ID 6424c54157d94cd157567438f1a376c23d625223
# Parent  253c98aa935a4f0432e63f0fec692ccb0fd271ab
added timeout to veriT

diff -r 253c98aa935a -r 6424c54157d9 src/HOL/Tools/SMT/smt_systems.ML
--- 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 = {