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)

1 files changed, 3 insertions, 3 deletions

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