aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index e387e6322..b4331dc46 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -896,6 +896,7 @@ end = struct (* {{{ *)
with e ->
let (e, info) = CErrors.push e in
let good_id = !cur_id in
+ cur_id := Stateid.dummy;
VCS.reached id;
let ie =
match Stateid.get info, safe_id with