diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-11-29 17:50:11 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-11-29 17:50:11 +0100 |
| commit | 3642314974b3aca6eb522c37e7e4efd226e6ebc8 (patch) | |
| tree | 8fab600f98483c1f74c2629b81dbd79ab5de7858 /stm | |
| parent | a27ac0315dcbb99c64a260bac3988199a26b39cf (diff) | |
STM: cur_id must be invalid if an error occurs (fix #5191)
Line erroneously removed in 17f3346c
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 1 |
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 |