# HG changeset patch
# User wenzelm
# Date 1598100480 -7200
# Node ID 8009c4b5db5efbe219c561d589aa76f0e9c5a760
# Parent  7a213affdc10b3d742df19b202a29fda0630dd57
proper treatment of absolute deadline vs. relative timeout;

diff -r 7a213affdc10 -r 8009c4b5db5e src/HOL/Nitpick_Examples/minipick.ML
--- a/src/HOL/Nitpick_Examples/minipick.ML	Sat Aug 22 13:55:42 2020 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML	Sat Aug 22 14:48:00 2020 +0200
@@ -430,10 +430,11 @@
 fun solve_any_kodkod_problem thy problems =
   let
     val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
+    val deadline = Time.now () + timeout
     val max_threads = 1
     val max_solutions = 1
   in
-    case solve_any_problem debug overlord timeout max_threads max_solutions
+    case solve_any_problem debug overlord deadline max_threads max_solutions
                            problems of
       JavaNotFound => "unknown"
     | JavaTooOld => "unknown"
diff -r 7a213affdc10 -r 8009c4b5db5e src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sat Aug 22 13:55:42 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sat Aug 22 14:48:00 2020 +0200
@@ -211,10 +211,11 @@
 fun run_all_tests () =
   let
     val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params \<^theory> []
+    val deadline = Time.now () + timeout
     val max_threads = 1
     val max_solutions = 1
   in
-    case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions
+    case Kodkod.solve_any_problem debug overlord deadline max_threads max_solutions
                                   (map (problem_for_nut \<^context>) tests) of
       Kodkod.Normal ([], _, _) => ()
     | _ => error "Tests failed"