aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 8f11875b6..4eb2c4b2d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1676,9 +1676,9 @@ let async_policy () =
(!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
let delegate name =
- let time = get_hint_bp_time name in
- time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
- || !Flags.async_proofs_full
+ get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
+ || !Flags.compilation_mode = Flags.BuildVio
+ || !Flags.async_proofs_full
let collect_proof keep cur hd brkind id =
prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);