From bce4de2f7c19fe59e650cb89a14e50a817b4b9ab Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Thu, 1 Jan 2015 21:19:23 +0100
Subject: Made invariant of class 'Trigger' robust by -replacing public field
 by private field + getter -using read-only wrappers (to avoid leaking)
 -cloning the tr list in the setter and constructor (to avoid capturing)

---
 Source/Core/StandardVisitor.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/Core/StandardVisitor.cs')

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 98ea4df3..58366051 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -526,7 +526,7 @@ namespace Microsoft.Boogie {
           node.Next = newNext;
         }
       }
-      node.Tr = this.VisitExprSeq(node.Tr);
+      node.Tr = this.VisitExprSeq(new List<Expr>(node.Tr));
       return node;
     }
     // called by default for all nullary type constructors and type variables
@@ -1072,7 +1072,7 @@ namespace Microsoft.Boogie {
           {
               this.VisitTrigger(origNext);
           }
-          this.VisitExprSeq(node.Tr);
+          node.Tr = this.VisitExprSeq(new List<Expr>(node.Tr));
           return node;
       }
       // called by default for all nullary type constructors and type variables
-- 
cgit v1.2.3