aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 96a11d306d..693c673b40 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1554,6 +1554,7 @@ let async_policy () =
let delegate name =
let time = get_hint_bp_time name in
time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
+ || !Flags.async_proofs_full
let collect_proof keep cur hd brkind id =
prerr_endline ("Collecting proof ending at "^Stateid.to_string id);