From 861ec0bdbe8be5e327b5082102c646882cd23383 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 7 Feb 2015 18:40:18 +0100
Subject: STM: tolerate simple side effects in async proofs (Close: 4006)

---
 stm/stm.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index 05c59720b1..3a57d85bab 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1580,6 +1580,7 @@ let collect_proof keep cur hd brkind id =
     let view = VCS.visit id in
     match view.step with
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
+    | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
     | `Alias _ -> `Sync (no_name,None,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
-- 
cgit v1.2.3