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)

1 files changed, 2 insertions, 2 deletions

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