From 10e3dc7980ceaeb254d7ad94829fd2f2ebb2612c Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 9 Jan 2015 15:57:10 +0100
Subject: Made invariant of class 'Trigger' robust by: - making field private -
 adding getter/setter - copying incoming list - exposing read-only list (with
 help from David Rohr)

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

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

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 68de45f6..abd106a5 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -523,11 +523,11 @@ namespace Microsoft.Boogie {
       if (origNext != null) {
         Trigger newNext = this.VisitTrigger(origNext);
         if (newNext != origNext) {
-          node = new Trigger(node.tok, node.Pos, node.Tr);  // note: this creates sharing between the old and new Tr sequence
+          node = new Trigger(node.tok, node.Pos, node.Tr.ToList());
           node.Next = newNext;
         }
       }
-      node.Tr = this.VisitExprSeq(node.Tr);
+      node.Tr = this.VisitExprSeq(node.Tr.ToList());
       return node;
     }
     // called by default for all nullary type constructors and type variables
@@ -1073,7 +1073,7 @@ namespace Microsoft.Boogie {
           {
               this.VisitTrigger(origNext);
           }
-          this.VisitExprSeq(node.Tr);
+          this.VisitExprSeq(node.Tr.ToList());
           return node;
       }
       // called by default for all nullary type constructors and type variables
-- 
cgit v1.2.3