Merging changes from 0biha/BoogieInvariantFixesIIIa

7 files changed, 385 insertions, 101 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7622cbdf..07448087 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -88,6 +88,7 @@ namespace Microsoft.Boogie {
   using System.Collections;

   using System.Diagnostics;

   using System.Collections.Generic;

+  using System.Collections.ObjectModel;

   using System.Diagnostics.Contracts;

   using Microsoft.Boogie.AbstractInterpretation;

   using Microsoft.Boogie.GraphUtil;

@@ -308,10 +309,18 @@ namespace Microsoft.Boogie {
     }

   }

 

-  // TODO: Ideally, this would use generics.

-  public interface IPotentialErrorNode {

-    object ErrorData {

+  public interface IPotentialErrorNode<out TGet>

+  {

+    TGet ErrorData

+    {

       get;

+    }

+  }

+

+  public interface IPotentialErrorNode<out TGet, in TSet> : IPotentialErrorNode<TGet>

+  {

+    new TSet ErrorData

+    {

       set;

     }

   }

@@ -321,7 +330,7 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(this.topLevelDeclarations));

-      Contract.Invariant(globalVariablesCache == null || cce.NonNullElements(globalVariablesCache));

+      Contract.Invariant(cce.NonNullElements(this.globalVariablesCache, true));

     }

     

     public Program()

@@ -673,18 +682,17 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private List<GlobalVariable/*!*/> globalVariablesCache = null;

-    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables

+    private IEnumerable<GlobalVariable/*!*/> globalVariablesCache = null;

+    public List<GlobalVariable/*!*/>/*!*/ GlobalVariables

     {

       get

       {

-        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<GlobalVariable>>()));

+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));

 

         if (globalVariablesCache == null)

-        {

-          globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>().ToList();

-        }

-        return globalVariablesCache;

+          globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>();

+

+        return new List<GlobalVariable>(globalVariablesCache);

       }

     }

 

@@ -1954,13 +1962,13 @@ namespace Microsoft.Boogie {
     // the <:-parents of the value of this constant. If the field is

     // null, no information about the parents is provided, which means

     // that the parental situation is unconstrained.

-    public readonly List<ConstantParent/*!*/> Parents;

+    public readonly ReadOnlyCollection<ConstantParent/*!*/> Parents;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(Parents, true));

     }

 

-

     // if true, it is assumed that the immediate <:-children of the

     // value of this constant are completely specified

     public readonly bool ChildrenComplete;

@@ -1987,16 +1995,16 @@ namespace Microsoft.Boogie {
     }

     public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent,

                     bool unique,

-                    List<ConstantParent/*!*/> parents, bool childrenComplete,

+                    IEnumerable<ConstantParent/*!*/> parents, bool childrenComplete,

                     QKeyValue kv)

       : base(tok, typedIdent, kv) {

       Contract.Requires(tok != null);

       Contract.Requires(typedIdent != null);

-      Contract.Requires(parents == null || cce.NonNullElements(parents));

+      Contract.Requires(cce.NonNullElements(parents, true));

       Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);

       Contract.Requires(typedIdent.WhereExpr == null);

       this.Unique = unique;

-      this.Parents = parents;

+      this.Parents = parents == null ? null : new ReadOnlyCollection<ConstantParent>(parents.ToList());

       this.ChildrenComplete = childrenComplete;

     }

     public override bool IsMutable {

@@ -2231,13 +2239,37 @@ namespace Microsoft.Boogie {
 

   public abstract class DeclWithFormals : NamedDeclaration {

     public List<TypeVariable>/*!*/ TypeParameters;

-    public /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ InParams, OutParams;

+

+    private /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ inParams, outParams;

+

+    public List<Variable>/*!*/ InParams {

+      get {

+        Contract.Ensures(Contract.Result<List<Variable>>() != null);

+        return this.inParams;

+      }

+      set {

+        Contract.Requires(value != null);

+        this.inParams = value;

+      }

+    }

+

+    public List<Variable>/*!*/ OutParams

+    {

+      get {

+        Contract.Ensures(Contract.Result<List<Variable>>() != null);

+        return this.outParams;

+      }

+      set {

+        Contract.Requires(value != null);

+        this.outParams = value;

+      }

+    }

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(TypeParameters != null);

-      Contract.Invariant(InParams != null);

-      Contract.Invariant(OutParams != null);

+      Contract.Invariant(this.inParams != null);

+      Contract.Invariant(this.outParams != null);

     }

 

     public DeclWithFormals(IToken tok, string name, List<TypeVariable> typeParams,

@@ -2249,16 +2281,16 @@ namespace Microsoft.Boogie {
       Contract.Requires(name != null);

       Contract.Requires(tok != null);

       this.TypeParameters = typeParams;

-      this.InParams = inParams;

-      this.OutParams = outParams;

+      this.inParams = inParams;

+      this.outParams = outParams;

     }

 

     protected DeclWithFormals(DeclWithFormals that)

       : base(that.tok, cce.NonNull(that.Name)) {

       Contract.Requires(that != null);

       this.TypeParameters = that.TypeParameters;

-      this.InParams = that.InParams;

-      this.OutParams = that.OutParams;

+      this.inParams = cce.NonNull(that.InParams);

+      this.outParams = cce.NonNull(that.OutParams);

     }

 

     public byte[] MD5Checksum_;

@@ -2753,7 +2785,7 @@ namespace Microsoft.Boogie {
       : base(tok, name, args, result) { }

   }

 

-  public class Requires : Absy, IPotentialErrorNode {

+  public class Requires : Absy, IPotentialErrorNode<string, string> {

     public readonly bool Free;

     

     private Expr/*!*/ _condition;

@@ -2773,13 +2805,12 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(this._condition != null);

-      Contract.Invariant(errorData == null || errorData is string);

     }

 

 

     // TODO: convert to use generics

-    private object errorData;

-    public object ErrorData {

+    private string errorData;

+    public string ErrorData {

       get {

         return errorData;

       }

@@ -2866,7 +2897,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class Ensures : Absy, IPotentialErrorNode {

+  public class Ensures : Absy, IPotentialErrorNode<string, string> {

     public readonly bool Free;

 

     private Expr/*!*/ _condition;

@@ -2885,14 +2916,13 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(this._condition != null); 

-      Contract.Invariant(errorData == null || errorData is string);

     }

 

     public string Comment;

 

     // TODO: convert to use generics

-    private object errorData;

-    public object ErrorData {

+    private string errorData;

+    public string ErrorData {

       get {

         return errorData;

       }

@@ -4212,24 +4242,42 @@ namespace Microsoft.Boogie {
     }

   }

   public class AtomicRE : RE {

-    public Block/*!*/ b;

+    private Block/*!*/ _b;

+

+    public Block b

+    {

+      get

+      {

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

+        return this._b;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._b = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(b != null);

+      Contract.Invariant(this._b != null);

     }

 

     public AtomicRE(Block block) {

       Contract.Requires(block != null);

-      b = block;

+      this._b = block;

     }

+

     public override void Resolve(ResolutionContext rc) {

       //Contract.Requires(rc != null);

       b.Resolve(rc);

     }

+

     public override void Typecheck(TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       b.Typecheck(tc);

     }

+

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

       b.Emit(stream, level);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 900d1c7a..11c3670e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -24,19 +24,77 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(tok != null);

-      Contract.Invariant(Anonymous || LabelName != null);

-      Contract.Invariant(ec == null || tc == null);

-      Contract.Invariant(simpleCmds != null);

+      Contract.Invariant(Anonymous || this.labelName != null);

+      Contract.Invariant(this._ec == null || this._tc == null);

+      Contract.Invariant(this._simpleCmds != null);

     }

 

     public readonly IToken/*!*/ tok;

-    public string LabelName;

+

     public readonly bool Anonymous;

 

+    private string labelName;

+

+    public string LabelName

+    {

+      get

+      {

+        Contract.Ensures(Anonymous || Contract.Result<string>() != null);

+        return this.labelName;

+      }

+      set

+      {

+        Contract.Requires(Anonymous || value != null);

+        this.labelName = value;

+      }

+    }

+

     [Rep]

-    public List<Cmd>/*!*/ simpleCmds;

-    public StructuredCmd ec;

-    public TransferCmd tc;

+    private List<Cmd>/*!*/ _simpleCmds;

+

+    public List<Cmd>/*!*/ simpleCmds

+    {

+      get

+      {

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

+        return this._simpleCmds;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._simpleCmds = value;

+      }

+    }

+

+    private StructuredCmd _ec;

+

+    public StructuredCmd ec

+    {

+      get

+      {

+        return this._ec;

+      }

+      set

+      {

+        Contract.Requires(value == null || this.tc == null);

+        this._ec = value;

+      }

+    }

+

+    private TransferCmd _tc;

+

+    public TransferCmd tc

+    {

+      get

+      {

+        return this._tc;

+      }

+      set

+      {

+        Contract.Requires(value == null || this.ec == null);

+        this._tc = value;

+      }

+    }

 

     public BigBlock successorBigBlock;  // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized)

 

@@ -45,11 +103,11 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);

       Contract.Requires(ec == null || tc == null);

       this.tok = tok;

-      this.LabelName = labelName;

       this.Anonymous = labelName == null;

-      this.simpleCmds = simpleCmds;

-      this.ec = ec;

-      this.tc = tc;

+      this.labelName = labelName;

+      this._simpleCmds = simpleCmds;

+      this._ec = ec;

+      this._tc = tc;

     }

 

     public void Emit(TokenTextWriter stream, int level) {

@@ -647,15 +705,30 @@ namespace Microsoft.Boogie {
 

   [ContractClass(typeof(StructuredCmdContracts))]

   public abstract class StructuredCmd {

-    public IToken/*!*/ tok;

+    private IToken/*!*/ _tok;

+

+    public IToken/*!*/ tok

+    {

+      get

+      {

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

+        return this._tok;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._tok = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(tok != null);

+      Contract.Invariant(this._tok != null);

     }

 

     public StructuredCmd(IToken tok) {

       Contract.Requires(tok != null);

-      this.tok = tok;

+      this._tok = tok;

     }

 

     public abstract void Emit(TokenTextWriter/*!*/ stream, int level);

@@ -673,16 +746,58 @@ namespace Microsoft.Boogie {
 

   public class IfCmd : StructuredCmd {

     public Expr Guard;

-    public StmtList/*!*/ thn;

-    public IfCmd elseIf;

-    public StmtList elseBlock;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(thn != null);

-      Contract.Invariant(elseIf == null || elseBlock == null);

+

+    private StmtList/*!*/ _thn;

+    

+    public StmtList/*!*/ thn

+    {

+      get

+      {

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

+        return this._thn;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._thn = value;

+      }

+    }

+

+    private IfCmd _elseIf;

+

+    public IfCmd elseIf

+    {

+      get

+      {

+        return this._elseIf;

+      }

+      set

+      {

+        Contract.Requires(value == null || this.elseBlock == null);

+        this._elseIf = value;

+      }

     }

 

+    private StmtList _elseBlock;

 

+    public StmtList elseBlock

+    {

+      get

+      {

+        return this._elseBlock;

+      }

+      set

+      {

+        Contract.Requires(value == null || this.elseIf == null);

+        this._elseBlock = value;

+      }

+    }

+

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(this._thn != null);

+      Contract.Invariant(this._elseIf == null || this._elseBlock == null);

+    }

 

     public IfCmd(IToken/*!*/ tok, Expr guard, StmtList/*!*/ thn, IfCmd elseIf, StmtList elseBlock)

       : base(tok) {

@@ -690,9 +805,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(thn != null);

       Contract.Requires(elseIf == null || elseBlock == null);

       this.Guard = guard;

-      this.thn = thn;

-      this.elseIf = elseIf;

-      this.elseBlock = elseBlock;

+      this._thn = thn;

+      this._elseIf = elseIf;

+      this._elseBlock = elseBlock;

     }

 

     public override void Emit(TokenTextWriter stream, int level) {

@@ -796,10 +911,40 @@ namespace Microsoft.Boogie {
   //---------------------------------------------------------------------

   // Block

   public sealed class Block : Absy {

-    public string/*!*/ Label;  // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal

+    private string/*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal

+

+    public string/*!*/ Label

+    {

+      get

+      {

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

+        return this.label;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this.label = value;

+      }

+    }

+

     [Rep]

     [ElementsPeer]

-    public List<Cmd>/*!*/ Cmds;

+    public List<Cmd>/*!*/ cmds;

+

+    public List<Cmd>/*!*/ Cmds

+    {

+      get

+      {

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

+        return this.cmds;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this.cmds = value;

+      }

+    }

+

     [Rep]  //PM: needed to verify Traverse.Visit

     public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)

 

@@ -829,8 +974,8 @@ namespace Microsoft.Boogie {
     public HashSet<Variable/*!*/> liveVarsBefore;

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Label != null);

-      Contract.Invariant(Cmds != null);

+      Contract.Invariant(this.label != null);

+      Contract.Invariant(this.cmds != null);

       Contract.Invariant(cce.NonNullElements(liveVarsBefore, true));

     }

 

@@ -851,8 +996,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(label != null);

       Contract.Requires(cmds != null);

       Contract.Requires(tok != null);

-      this.Label = label;

-      this.Cmds = cmds;

+      this.label = label;

+      this.cmds = cmds;

       this.TransferCmd = transferCmd;

       this.Predecessors = new List<Block>();

       this.liveVarsBefore = null;

@@ -1997,7 +2142,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class ParCallCmd : CallCommonality, IPotentialErrorNode

+  public class ParCallCmd : CallCommonality, IPotentialErrorNode<object, object>

   {

       public List<CallCmd> CallCmds;

       public ParCallCmd(IToken tok, List<CallCmd> callCmds)

@@ -2086,7 +2231,8 @@ namespace Microsoft.Boogie {
       }

   }

 

-  public class CallCmd : CallCommonality, IPotentialErrorNode {

+  public class CallCmd : CallCommonality, IPotentialErrorNode<object, object>

+  {

     public string/*!*/ callee { get; set; }

     public Procedure Proc;

     public LocalVariable AssignedAssumptionVariable;

@@ -2720,38 +2866,69 @@ namespace Microsoft.Boogie {
   }

 

   public class ListOfMiningStrategies : MiningStrategy {

-    public List<MiningStrategy>/*!*/ msList;

+

+    private List<MiningStrategy>/*!*/ _msList;

+

+    public List<MiningStrategy>/*!*/ msList

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<List<MiningStrategy>>() != null);

+        return this._msList;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._msList = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(msList != null);

+      Contract.Invariant(this._msList != null);

     }

 

-

     public ListOfMiningStrategies(List<MiningStrategy> l) {

       Contract.Requires(l != null);

-      this.msList = l;

+      this._msList = l;

     }

   }

 

   public class EEDTemplate : MiningStrategy {

-    public string/*!*/ reason;

+    private string/*!*/ _reason;

+

+    public string/*!*/ reason

+    {

+      get

+      {

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

+        return this._reason;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._reason = value;

+      }

+    }

+

     public List<Expr/*!*/>/*!*/ exprList;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(reason != null);

+      Contract.Invariant(this._reason != null);

       Contract.Invariant(cce.NonNullElements(exprList));

     }

 

-

     public EEDTemplate(string reason, List<Expr/*!*/>/*!*/ exprList) {

       Contract.Requires(reason != null);

       Contract.Requires(cce.NonNullElements(exprList));

-      this.reason = reason;

+      this._reason = reason;

       this.exprList = exprList;

     }

   }

 

-  public class AssertCmd : PredicateCmd, IPotentialErrorNode {

+  public class AssertCmd : PredicateCmd, IPotentialErrorNode<object, object>

+  {

     public Expr OrigExpr;

     public Dictionary<Variable, Expr> IncarnationMap;

 

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 8918115b..e2113ab5 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2530,16 +2530,30 @@ namespace Microsoft.Boogie {
 

   public class IfThenElse : IAppliable {

 

-    public IToken/*!*/ tok;

+    private IToken/*!*/ _tok;

+

+    public IToken/*!*/ tok

+    {

+      get

+      {

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

+        return this._tok;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._tok = value;

+      }

+    }

+    

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(tok != null);

+      Contract.Invariant(this._tok != null);

     }

 

-

     public IfThenElse(IToken tok) {

       Contract.Requires(tok != null);

-      this.tok = tok;

+      this._tok = tok;

     }

 

     public string/*!*/ FunctionName {

@@ -2566,7 +2580,7 @@ namespace Microsoft.Boogie {
     public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

       //Contract.Requires(args != null);

-      stream.SetToken(ref this.tok);

+      stream.SetToken(this);

       Contract.Assert(args.Count == 3);

       stream.push();

       stream.Write("(if ");     

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9cbadc80..00a38d23 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -389,32 +389,43 @@ namespace Microsoft.Boogie {
   public class Trigger : Absy {

     public readonly bool Pos;

     [Rep]

-    public List<Expr>/*!*/ Tr;

+    private List<Expr>/*!*/ tr;

+

+    public IList<Expr>/*!*/ Tr

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<IList<Expr>>() != null);

+        Contract.Ensures(Contract.Result<IList<Expr>>().Count >= 1);

+        Contract.Ensures(this.Pos || Contract.Result<IList<Expr>>().Count == 1);

+        return this.tr.AsReadOnly();

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        Contract.Requires(value.Count >= 1);

+        Contract.Requires(this.Pos || value.Count == 1);

+        this.tr = new List<Expr>(value);

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Tr != null);

-      Contract.Invariant(1 <= Tr.Count);

-      Contract.Invariant(Pos || Tr.Count == 1);

+      Contract.Invariant(this.tr != null);

+      Contract.Invariant(this.tr.Count >= 1);

+      Contract.Invariant(Pos || this.tr.Count == 1);

     }

 

     public Trigger Next;

 

-    public Trigger(IToken tok, bool pos, List<Expr> tr)

-      : this(tok, pos, tr, null) {

-      Contract.Requires(tr != null);

-      Contract.Requires(tok != null);

-      Contract.Requires(1 <= tr.Count);

-      Contract.Requires(pos || tr.Count == 1);

-    }

-

-    public Trigger(IToken/*!*/ tok, bool pos, List<Expr>/*!*/ tr, Trigger next)

+    public Trigger(IToken/*!*/ tok, bool pos, IList<Expr>/*!*/ tr, Trigger next = null)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(tr != null);

-      Contract.Requires(1 <= tr.Count);

+      Contract.Requires(tr.Count >= 1);

       Contract.Requires(pos || tr.Count == 1);

       this.Pos = pos;

-      this.Tr = tr;

+      this.tr = new List<Expr>(tr);

       this.Next = next;

     }

 

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 6bed4e75..4ca08072 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -218,6 +218,7 @@ namespace Microsoft.Boogie {
       /// </summary>

       public bool GetNumericArgument(ref int arg, int limit) {

         Contract.Requires(this.i < args.Length);

+        Contract.Ensures(Math.Min(arg, 0) <= Contract.ValueAtReturn(out arg) && Contract.ValueAtReturn(out arg) < limit);

         //modifies nextIndex, encounteredErrors, Console.Error.*;

         int a = arg;

         if (!GetNumericArgument(ref a)) {

@@ -236,6 +237,7 @@ namespace Microsoft.Boogie {
       /// Otherwise, emit an error message, leave "arg" unchanged, and return "false".

       /// </summary>

       public bool GetNumericArgument(ref double arg) {

+        Contract.Ensures(Contract.ValueAtReturn(out arg) >= 0);

         //modifies nextIndex, encounteredErrors, Console.Error.*;

         if (this.ConfirmArgumentCount(1)) {

           try {

@@ -508,7 +510,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);

       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);

       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);

-      Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC < 2);

+      Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1);

       Contract.Invariant(cce.NonNullElements(ProverOptions));

     }

 

@@ -543,7 +545,21 @@ namespace Microsoft.Boogie {
     public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically

     public bool DoModSetAnalysis = false;

     public bool UseAbstractInterpretation = true;          // true iff the user want to use abstract interpretation

-    public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator

+    private int  /*0..9*/stepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator

+

+    public int StepsBeforeWidening

+    {

+      get

+      {

+        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= 9);

+        return this.stepsBeforeWidening;

+      }

+      set

+      {

+        Contract.Requires(0 <= value && value <= 9);

+        this.stepsBeforeWidening = value;

+      }

+    }

 

     public string OwickiGriesDesugaredOutputFile = null;

     public bool TrustAtomicityTypes = false;

@@ -575,7 +591,19 @@ namespace Microsoft.Boogie {
     [Peer]

     public List<string/*!*/>/*!*/ ProverOptions = new List<string/*!*/>();

 

-    public int BracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes

+    private int bracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes

+

+    public int BracketIdsInVC {

+      get {

+        Contract.Ensures(-1 <= Contract.Result<int>() && Contract.Result<int>() <= 1);

+        return this.bracketIdsInVC;

+      }

+      set {

+        Contract.Requires(-1 <= value && value <= 1);

+        this.bracketIdsInVC = value;

+      }

+    }

+

     public bool CausalImplies = false;

 

     public int SimplifyProverMatchDepth = -1;  // -1 means not specified

@@ -1296,7 +1324,7 @@ namespace Microsoft.Boogie {
           return true;

 

         case "vcBrackets":

-          ps.GetNumericArgument(ref BracketIdsInVC, 2);

+          ps.GetNumericArgument(ref bracketIdsInVC, 2);

           return true;

 

         case "proverMemoryLimit": {

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

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index b28ac042..73008742 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -229,6 +229,12 @@ namespace Microsoft.Boogie {
       this.SetToken(t => absy.tok = t);

     }

 

+    public void SetToken(IfThenElse expr)

+    {

+      Contract.Requires(expr != null);

+      this.SetToken(t => expr.tok = t);

+    }

+

     public void SetToken(Action<IToken> setter) {

       Contract.Requires(setter != null);

       if (this.setTokens) {