Made some compatibility fixes after running the unit tests.

Added an internal non-readonly version of Lhss and Rhss to 'AssignCmd'.

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 3f3ad5ae..0284549b 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -75,8 +75,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);

       for (int i = 0; i < node.Lhss.Count; ++i) {

-        node.Lhss[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));

-        node.Rhss[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));

+        node.Lhss_NRO[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));

+        node.Rhss_NRO[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));

       }

       return node;

     }