diff -r 4195e75a92ef -r 478b7599a1a0 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Tue Sep 08 11:32:57 2020 +0200 +++ b/src/HOL/SMT.thy Wed Sep 30 18:37:22 2020 +0200 @@ -346,7 +346,7 @@ (given in seconds) to restrict their runtime. \ -declare [[smt_timeout = 20]] +declare [[smt_timeout = 1000000]] text \ SMT solvers apply randomized heuristics. In case a problem is not