proper treatment of absolute deadline vs. relative timeout;
--- 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"
--- 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"