Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on.

1 files changed, 355 insertions, 328 deletions

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 693fcf76..45eeda43 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -14,18 +14,17 @@ using Microsoft.Boogie.VCExprAST;
 

 // a naive method to turn VCExprs into strings that can be fed into Simplify

 

-namespace Microsoft.Boogie.VCExprAST

-{

+namespace Microsoft.Boogie.VCExprAST {

   [ContractClassFor(typeof(LineariserOptions))]

-  public abstract class LinOptContracts:LineariserOptions{

-    public LinOptContracts() : base(true) {

+  public abstract class LinOptContracts : LineariserOptions {

+    public LinOptContracts()

+      : base(true) {

     }

-    public override LineariserOptions  SetAsTerm(bool newVal)

-{

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

-  throw new NotImplementedException();

-}

-    

+    public override LineariserOptions SetAsTerm(bool newVal) {

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

+      throw new NotImplementedException();

+    }

+

   }

 

   // Options for the linearisation. Here one can choose, for instance,

@@ -36,52 +35,72 @@ namespace Microsoft.Boogie.VCExprAST
     public readonly bool AsTerm;

     public abstract LineariserOptions/*!*/ SetAsTerm(bool newVal);

 

-    public abstract bool QuantifierIds { get; }

+    public abstract bool QuantifierIds {

+      get;

+    }

 

-    public virtual bool UseWeights { get { return false; } }

+    public virtual bool UseWeights {

+      get {

+        return false;

+      }

+    }

 

-    public virtual bool InverseImplies { get { return false; } }

+    public virtual bool InverseImplies {

+      get {

+        return false;

+      }

+    }

 

     // whether to include type specifications in quantifiers

-    public abstract bool UseTypes { get; }

+    public abstract bool UseTypes {

+      get;

+    }

 

-    public virtual CommandLineOptions.BvHandling Bitvectors { get {

-      return CommandLineOptions.BvHandling.None;

-    } }

+    public virtual CommandLineOptions.BvHandling Bitvectors {

+      get {

+        return CommandLineOptions.BvHandling.None;

+      }

+    }

 

     // variables representing formulas in let-bindings have to be

     // printed in a different way than other variables

-    public virtual List<VCExprVar/*!*/>/*!*/ LetVariables { get {Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

-      return EmptyList;

-    } }

+    public virtual List<VCExprVar/*!*/>/*!*/ LetVariables {

+      get {

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

+        return EmptyList;

+      }

+    }

 

-    public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar){

-Contract.Requires(furtherVar != null);

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

+    public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar) {

+      Contract.Requires(furtherVar != null);

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

       return this;

     }

 

-	public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars){

-Contract.Requires(cce.NonNullElements(furtherVars));

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

+    public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars) {

+      Contract.Requires(cce.NonNullElements(furtherVars));

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

       return this;

     }

-    

+

     private static readonly List<VCExprVar/*!*/>/*!*/ EmptyList = new List<VCExprVar/*!*/>();

     [ContractInvariantMethod]

-void ObjectInvarinat() 

-{

-    Contract.Invariant(EmptyList!=null);

-}

+    void ObjectInvarinat() {

+      Contract.Invariant(EmptyList != null);

+    }

 

 

-    public bool NativeBv { get {

-      return Bitvectors == CommandLineOptions.BvHandling.Z3Native;

-    } }

+    public bool NativeBv {

+      get {

+        return Bitvectors == CommandLineOptions.BvHandling.Z3Native;

+      }

+    }

 

-    public bool IntBv { get {

-      return Bitvectors == CommandLineOptions.BvHandling.ToInt;

-    } }

+    public bool IntBv {

+      get {

+        return Bitvectors == CommandLineOptions.BvHandling.ToInt;

+      }

+    }

 

     ////////////////////////////////////////////////////////////////////////////////////////

 

@@ -89,23 +108,28 @@ void ObjectInvarinat()
       this.AsTerm = asTerm;

     }

 

-    public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions (false);

-    internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions (true);

+    public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions(false);

+    internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions(true);

 

     ////////////////////////////////////////////////////////////////////////////////////////

 

     private class SimplifyOptions : LineariserOptions {

-      internal SimplifyOptions(bool asTerm):base(asTerm) {

-        

+      internal SimplifyOptions(bool asTerm)

+        : base(asTerm) {

+

+      }

+      public override bool QuantifierIds {

+        get {

+          return false;

+        }

+      }

+      public override bool UseTypes {

+        get {

+          return false;

+        }

       }

-      public override bool QuantifierIds { get {

-        return false;

-      } }

-      public override bool UseTypes { get {

-        return false;

-      } }

       public override LineariserOptions SetAsTerm(bool newVal) {

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

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

         if (newVal)

           return SimplifyDefaultTerm;

         else

@@ -119,21 +143,21 @@ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
   // Lineariser for expressions. The result (bool) is currently not used for anything

   public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {

 

-    public static string ToSimplifyString(VCExpr e, UniqueNamer namer){

-Contract.Requires(namer != null);

-Contract.Requires(e != null);

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

+    public static string ToSimplifyString(VCExpr e, UniqueNamer namer) {

+      Contract.Requires(namer != null);

+      Contract.Requires(e != null);

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

       return ToString(e, LineariserOptions.SimplifyDefault, namer);

     }

 

-    public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options,UniqueNamer/*!*/ namer) {

+    public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options, UniqueNamer/*!*/ namer) {

       Contract.Requires(e != null);

       Contract.Requires(options != null);

       Contract.Requires(namer != null);

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

 

       StringWriter sw = new StringWriter();

-      SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);

+      SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser(sw, namer);

       lin.Linearise(e, options);

       return sw.ToString();

     }

@@ -141,60 +165,62 @@ Contract.Ensures(Contract.Result<string>() != null);
     ////////////////////////////////////////////////////////////////////////////////////////

 

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(wr!=null);

+    void ObjectInvariant() {

+      Contract.Invariant(wr != null);

       Contract.Invariant(Namer != null);

-}

+    }

 

     private readonly TextWriter/*!*/ wr;

     private SimplifyLikeOpLineariser OpLinObject = null;

-    private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser { get {Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>()!=null);

-      if (OpLinObject == null)

-        OpLinObject = new SimplifyLikeOpLineariser (this, wr);

-      return OpLinObject;

-    } }

+    private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser {

+      get {

+        Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);

+        if (OpLinObject == null)

+          OpLinObject = new SimplifyLikeOpLineariser(this, wr);

+        return OpLinObject;

+      }

+    }

 

     internal readonly UniqueNamer Namer;

 

-    public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer){

-Contract.Requires(namer != null);

-Contract.Requires(wr != null);

+    public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer) {

+      Contract.Requires(namer != null);

+      Contract.Requires(wr != null);

       this.wr = wr;

       this.Namer = namer;

     }

 

-    public void Linearise(VCExpr expr, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(expr != null);

+    public void Linearise(VCExpr expr, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(expr != null);

       expr.Accept<bool, LineariserOptions>(this, options);

     }

 

-    public void LineariseAsTerm(VCExpr expr, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(expr != null);

+    public void LineariseAsTerm(VCExpr expr, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(expr != null);

       Linearise(expr, options.SetAsTerm(true));

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public static string MakeIdPrintable(string s){

-Contract.Requires(s != null);

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

+    public static string MakeIdPrintable(string s) {

+      Contract.Requires(s != null);

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

       // make sure that no keywords are used as identifiers

-      switch(s) {

-      case andName:

-      case orName:

-      case notName:

-      case impliesName:

-      case iffName:

-      case eqName:

-      case neqName:

-      case distinctName:

-      case TRUEName:

-      case FALSEName:

-        s = "nonkeyword_" + s;

-        break;

+      switch (s) {

+        case andName:

+        case orName:

+        case notName:

+        case impliesName:

+        case iffName:

+        case eqName:

+        case neqName:

+        case distinctName:

+        case TRUEName:

+        case FALSEName:

+          s = "nonkeyword_" + s;

+          break;

       }

 

       if (CommandLineOptions.Clo.BracketIdsInVC == 0) {

@@ -242,29 +268,26 @@ Contract.Ensures(Contract.Result<string>() != null);
       }

     }

 

-    private static void TypeToStringHelper(Type t, StringBuilder sb)

-    {

+    private static void TypeToStringHelper(Type t, StringBuilder sb) {

       Contract.Requires(t != null);

 

       TypeSynonymAnnotation syn = t as TypeSynonymAnnotation;

       if (syn != null) {

         TypeToStringHelper(syn.ExpandedType, sb);

-      }

-      else {

+      } else {

         if (t.IsMap) {

           MapType m = t.AsMap;

           sb.Append('[');

           for (int i = 0; i < m.MapArity; ++i) {

-            if (i != 0) sb.Append(',');

+            if (i != 0)

+              sb.Append(',');

             TypeToStringHelper(m.Arguments[i], sb);

           }

           sb.Append(']');

           TypeToStringHelper(m.Result, sb);

-        }

-        else if (t.IsBool || t.IsInt || t.IsBv) {

+        } else if (t.IsBool || t.IsInt || t.IsBv) {

           sb.Append(TypeToString(t));

-        }

-        else {

+        } else {

           System.IO.StringWriter buffer = new System.IO.StringWriter();

           using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

             t.Emit(stream);

@@ -276,8 +299,7 @@ Contract.Ensures(Contract.Result<string>() != null);
     }

 

 

-    public static string TypeToString(Type t)

-    {

+    public static string TypeToString(Type t) {

       Contract.Requires(t != null);

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

 

@@ -294,39 +316,39 @@ Contract.Ensures(Contract.Result<string>() != null);
       }

     }

 

-    public static string BvConcatOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires((node.Op is VCExprBvConcatOp));

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

+    public static string BvConcatOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Op is VCExprBvConcatOp));

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

       int bits1 = node[0].Type.BvBits;

       int bits2 = node[1].Type.BvBits;

       return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]";

     }

 

-    public static string BvExtractOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires(node.Op is VCExprBvExtractOp);

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

+    public static string BvExtractOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires(node.Op is VCExprBvExtractOp);

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

       VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;

       return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";

     }

 

-    public static string StoreOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires((node.Op is VCExprStoreOp));

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

+    public static string StoreOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Op is VCExprStoreOp));

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

       return "Store_" + TypeToString(node[0].Type);

     }

 

-    public static string SelectOpName(VCExprNAry node){

-Contract.Requires(node != null);

-Contract.Requires((node.Op is VCExprSelectOp));

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

+    public static string SelectOpName(VCExprNAry node) {

+      Contract.Requires(node != null);

+      Contract.Requires((node.Op is VCExprSelectOp));

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

       return "Select_" + TypeToString(node[0].Type);

     }

-    

-    internal void WriteId(string s){

-Contract.Requires(s != null);

+

+    internal void WriteId(string s) {

+      Contract.Requires(s != null);

       wr.Write(MakeIdPrintable(s));

     }

 

@@ -343,7 +365,7 @@ Contract.Requires(s != null);
     internal const string eqName = "EQ"; // equality

     internal const string neqName = "NEQ"; // inequality

     internal const string lessName = "<";

-    internal const string greaterName = ">"; 

+    internal const string greaterName = ">";

     internal const string atmostName = "<=";

     internal const string atleastName = ">=";

     internal const string TRUEName = "TRUE"; // nullary predicate that is always true

@@ -373,25 +395,25 @@ Contract.Requires(s != null);
     internal const string intDivName = "/";

     internal const string intModName = "%";

 

-    internal void AssertAsTerm(string x, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(x != null);

+    internal void AssertAsTerm(string x, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(x != null);

       if (!options.AsTerm)

         System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");

     }

 

-    internal void AssertAsFormula(string x, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(x != null);

+    internal void AssertAsFormula(string x, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(x != null);

       if (options.AsTerm)

         System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprLiteral node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprLiteral node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       if (options.AsTerm) {

 

         if (node == VCExpressionGenerator.True)

@@ -425,9 +447,9 @@ Contract.Requires(node != null);
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprNAry node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       VCExprOp op = node.Op;

       Contract.Assert(op != null);

 

@@ -438,11 +460,11 @@ Contract.Requires(node != null);
 

         wr.Write("({0}",

                  op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);

-        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);

+        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

         Contract.Assert(enumerator != null);

         while (enumerator.MoveNext()) {

           VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

-          if (naryExpr == null ||  !naryExpr.Op.Equals(op)) {

+          if (naryExpr == null || !naryExpr.Op.Equals(op)) {

             wr.Write(" ");

             Linearise(cce.NonNull((VCExpr)enumerator.Current), options);

           }

@@ -458,24 +480,24 @@ Contract.Requires(node != null);
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprVar node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprVar node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       string printedName = Namer.GetName(node, node.Name);

       Contract.Assert(printedName != null);

 

       if (options.AsTerm ||

-          // variables for formulas bound in a let-binding are never

-          // written as an equation

+        // variables for formulas bound in a let-binding are never

+        // written as an equation

           options.LetVariables.Contains(node) ||

-          // if variables are properly typed, they cannot be written as

-          // equation either

+        // if variables are properly typed, they cannot be written as

+        // equation either

           options.UseTypes) {

         WriteId(printedName);

       } else {

         wr.Write("({0} ", eqName);

         WriteId(printedName);

-        wr.Write(" {0})", boolTrueName);        

+        wr.Write(" {0})", boolTrueName);

       }

 

       return true;

@@ -483,71 +505,71 @@ Contract.Requires(node != null);
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprQuantifier node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+    public bool Visit(VCExprQuantifier node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

       AssertAsFormula(node.Quan.ToString(), options);

       Contract.Assert(node.TypeParameters.Count == 0);

 

-      Namer.PushScope(); try {

+      Namer.PushScope();

+      try {

 

-      string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";

-      wr.Write("({0} (", kind);

+        string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";

+        wr.Write("({0} (", kind);

 

-      for (int i = 0; i < node.BoundVars.Count; i++) 

-        {

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

           VCExprVar var = node.BoundVars[i];

-        Contract.Assert(var != null);

+          Contract.Assert(var != null);

           string printedName = Namer.GetLocalName(var, var.Name);

-        Contract.Assert(printedName != null);

+          Contract.Assert(printedName != null);

           if (i != 0)

             wr.Write(" ");

           WriteId(printedName);

           if (options.UseTypes)

             wr.Write(" :TYPE {0}", TypeToString(var.Type));

         }

-      wr.Write(") ");

-        

-      WriteTriggers(node.Triggers, options);

-        

-      if (options.QuantifierIds) {

-        // only needed for Z3

-        VCQuantifierInfos infos = node.Infos;

-        Contract.Assert(infos != null);

-        if (infos.qid != null) {

-          wr.Write("(QID ");

-          wr.Write(infos.qid);

-          wr.Write(") ");

-        }

-        if (0 <= infos.uniqueId) {

-          wr.Write("(SKOLEMID ");

-          wr.Write(infos.uniqueId);

-          wr.Write(") ");

+        wr.Write(") ");

+

+        WriteTriggers(node.Triggers, options);

+

+        if (options.QuantifierIds) {

+          // only needed for Z3

+          VCQuantifierInfos infos = node.Infos;

+          Contract.Assert(infos != null);

+          if (infos.qid != null) {

+            wr.Write("(QID ");

+            wr.Write(infos.qid);

+            wr.Write(") ");

+          }

+          if (0 <= infos.uniqueId) {

+            wr.Write("(SKOLEMID ");

+            wr.Write(infos.uniqueId);

+            wr.Write(") ");

+          }

         }

-     }

 

-     if (options.UseWeights) {

-        int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);

-        if (weight != 1) {

-          wr.Write("(WEIGHT ");

-          wr.Write(weight);

-          wr.Write(") ");

+        if (options.UseWeights) {

+          int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);

+          if (weight != 1) {

+            wr.Write("(WEIGHT ");

+            wr.Write(weight);

+            wr.Write(") ");

+          }

         }

-      }

 

-      Linearise(node.Body, options);

-      wr.Write(")");

+        Linearise(node.Body, options);

+        wr.Write(")");

 

-      return true;

+        return true;

 

       } finally {

         Namer.PopScope();

       }

     }

 

-    private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(cce.NonNullElements(triggers));

+    private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options) {

+      Contract.Requires(options != null);

+      Contract.Requires(cce.NonNullElements(triggers));

       // first, count how many neg/pos triggers there are

       int negTriggers = 0;

       int posTriggers = 0;

@@ -568,7 +590,8 @@ Contract.Requires(cce.NonNullElements(triggers));
             if (vcTrig.Exprs.Count > 1) {

               wr.Write(" (MPAT");

             }

-            foreach (VCExpr e in vcTrig.Exprs) {Contract.Assert(e != null);

+            foreach (VCExpr e in vcTrig.Exprs) {

+              Contract.Assert(e != null);

               wr.Write(" ");

               LineariseAsTerm(e, options);

             }

@@ -598,37 +621,39 @@ Contract.Requires(cce.NonNullElements(triggers));
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprLet node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

-      Namer.PushScope(); try {

+    public bool Visit(VCExprLet node, LineariserOptions options) {

+      //Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      Namer.PushScope();

+      try {

 

-      wr.Write("(LET (");

+        wr.Write("(LET (");

 

-      LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);

+        LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);

         Contract.Assert(optionsWithVars != null);

-	  

-      string s = "(";

-      foreach (VCExprLetBinding b in node) {Contract.Assert(b != null);

-        wr.Write(s);

-        string printedName = Namer.GetLocalName(b.V, b.V.Name);

-

-        bool formula = b.V.Type.IsBool;

-        if (formula)

-          wr.Write("FORMULA ");

-        else

-          wr.Write("TERM ");

-        WriteId(printedName);

-        wr.Write(" ");

-        Linearise(b.E, optionsWithVars.SetAsTerm(!formula));

+

+        string s = "(";

+        foreach (VCExprLetBinding b in node) {

+          Contract.Assert(b != null);

+          wr.Write(s);

+          string printedName = Namer.GetLocalName(b.V, b.V.Name);

+

+          bool formula = b.V.Type.IsBool;

+          if (formula)

+            wr.Write("FORMULA ");

+          else

+            wr.Write("TERM ");

+          WriteId(printedName);

+          wr.Write(" ");

+          Linearise(b.E, optionsWithVars.SetAsTerm(!formula));

+          wr.Write(")");

+          s = " (";

+        }

+        wr.Write(") ");

+        Linearise(node.Body, optionsWithVars);

         wr.Write(")");

-        s = " (";

-      }

-      wr.Write(") ");

-      Linearise(node.Body, optionsWithVars);

-      wr.Write(")");

 

-      return true;

+        return true;

 

       } finally {

         Namer.PopScope();

@@ -648,50 +673,50 @@ Contract.Requires(node != null);
       private readonly SimplifyLikeExprLineariser/*!*/ ExprLineariser;

       private readonly TextWriter/*!*/ wr;

 

-      public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr){

-Contract.Requires(wr != null);

-Contract.Requires(ExprLineariser != null);

+      public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr) {

+        Contract.Requires(wr != null);

+        Contract.Requires(ExprLineariser != null);

         this.ExprLineariser = ExprLineariser;

         this.wr = wr;

       }

 

       ///////////////////////////////////////////////////////////////////////////////////

 

-      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){

-Contract.Requires(options != null);

-Contract.Requires(op != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms) {

+        Contract.Requires(options != null);

+        Contract.Requires(op != null);

+        Contract.Requires(cce.NonNullElements(args));

         WriteApplication(op, op, args, options, argsAsTerms);

       }

 

-      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(op != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(op != null);

+        Contract.Requires(cce.NonNullElements(args));

         WriteApplication(op, op, args, options, options.AsTerm);

       }

 

-      private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(op != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(op != null);

+        Contract.Requires(cce.NonNullElements(args));

         ExprLineariser.AssertAsTerm(op, options);

         WriteApplication(op, op, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(predOp != null);

-Contract.Requires(termOp != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(predOp != null);

+        Contract.Requires(termOp != null);

+        Contract.Requires(cce.NonNullElements(args));

         WriteApplication(termOp, predOp, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){

-Contract.Requires(options != null);

-Contract.Requires(predOp != null);

-Contract.Requires(termOp != null);

-Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?

+      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms) {

+        Contract.Requires(options != null);

+        Contract.Requires(predOp != null);

+        Contract.Requires(termOp != null);

+        Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?

         wr.Write("({0}", options.AsTerm ? termOp : predOp);

 

         LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);

@@ -701,17 +726,17 @@ Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the
           wr.Write(" ");

           ExprLineariser.Linearise(e, newOptions);

         }

-        

+

         wr.Write(")");

       }

 

       // write an application that can only be a term.

       // if the expression is supposed to be printed as a formula,

       // it is turned into an equation (EQ (f args) |@true|)

-      private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(termOp != null);

-Contract.Requires(cce.NonNullElements(args));

+      private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {

+        Contract.Requires(options != null);

+        Contract.Requires(termOp != null);

+        Contract.Requires(cce.NonNullElements(args));

         if (!options.AsTerm)

           // Write: (EQ (f args) |@true|)

           // where "args" are written as terms

@@ -724,17 +749,17 @@ Contract.Requires(cce.NonNullElements(args));
       }

 

       ///////////////////////////////////////////////////////////////////////////////////

-      

-      public bool VisitNotOp     (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+

+      public bool VisitNotOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(boolNotName, notName, node, options);      // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitEqOp      (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitEqOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (options.AsTerm) {

           // use equality on terms, also if the arguments have type bool

           WriteApplication(termEqName, node, options);

@@ -753,9 +778,9 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitNeqOp     (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitNeqOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (options.AsTerm) {

           // use equality on terms, also if the arguments have type bool

           WriteApplication(termNeqName, node, options);

@@ -771,29 +796,29 @@ Contract.Requires(node != null);
             WriteApplication(neqName, node, options, true);

           }

         }

-        

+

         return true;

       }

 

-      public bool VisitAndOp     (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitAndOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         Contract.Assert(options.AsTerm);

         WriteApplication(boolAndName, andName, node, options);        // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitOrOp      (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitOrOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         Contract.Assert(options.AsTerm);

         WriteApplication(boolOrName, orName, node, options);        // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitImpliesOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (options.AsTerm) {

           wr.Write("({0} ({1} ", boolOrName, boolNotName);

           ExprLineariser.Linearise(node[0], options);

@@ -807,16 +832,16 @@ Contract.Requires(node != null);
           ExprLineariser.Linearise(node[0], options);

           wr.Write("))");

         } else {

-          WriteApplication(impliesName, node, options);          

+          WriteApplication(impliesName, node, options);

         }

         return true;

       }

 

-      public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitDistinctOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         ExprLineariser.AssertAsFormula(distinctName, options);

-        

+

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);

         } else {

@@ -832,19 +857,20 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitLabelOp   (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitLabelOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         VCExprLabelOp op = (VCExprLabelOp)node.Op;

         Contract.Assert(op != null);

         wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));

-        ExprLineariser.Linearise(node[0], options); wr.Write(")");

+        ExprLineariser.Linearise(node[0], options);

+        wr.Write(")");

         return true;

       }

 

-      public bool VisitSelectOp  (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitSelectOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         wr.Write("(" + SelectOpName(node));

         foreach (VCExpr/*!*/ e in node) {

           Contract.Assert(e != null);

@@ -855,9 +881,9 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitStoreOp   (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitStoreOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         wr.Write("(" + StoreOpName(node));

         foreach (VCExpr e in node) {

           Contract.Assert(e != null);

@@ -868,31 +894,31 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitBvOp      (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitBvOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);

         return true;

       }

 

-      public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(BvExtractOpName(node), node, options);

         return true;

       }

 

-      public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitBvConcatOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(BvConcatOpName(node), node, options);

         return true;

       }

 

-      public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

-        

+      public bool VisitIfThenElseOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+

         wr.Write("(ITE ");

         ExprLineariser.Linearise(node[0], options.SetAsTerm(false));

         wr.Write(" ");

@@ -905,8 +931,8 @@ Contract.Requires(node != null);
       }

 

       public bool VisitCustomOp(VCExprNAry/*!*/ node, LineariserOptions/*!*/ options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

         VCExprCustomOp op = (VCExprCustomOp)node.Op;

         wr.Write("({0}", op.Name);

         foreach (VCExpr arg in node) {

@@ -917,9 +943,9 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitAddOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitAddOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         if (CommandLineOptions.Clo.ReflectAdd) {

           WriteTermApplication(intAddNameReflect, node, options);

         } else {

@@ -928,79 +954,79 @@ Contract.Requires(node != null);
         return true;

       }

 

-      public bool VisitSubOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitSubOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intSubName, node, options);

         return true;

       }

 

-      public bool VisitMulOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitMulOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intMulName, node, options);

         return true;

       }

 

-      public bool VisitDivOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitDivOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intDivName, node, options);

         return true;

       }

 

-      public bool VisitModOp           (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitModOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteTermApplication(intModName, node, options);

         return true;

       }

 

-      public bool VisitLtOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitLtOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termLessName, lessName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitLeOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitLeOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termAtmostName, atmostName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitGtOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitGtOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termGreaterName, greaterName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitGeOp            (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitGeOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(termAtleastName, atleastName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitSubtypeOp       (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitSubtypeOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(subtypeName, node, options, true);               // arguments are always terms

         return true;

       }

 

-      public bool VisitSubtype3Op       (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitSubtype3Op(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         WriteApplication(subtypeArgsName, node, options, true);               // arguments are always terms

         return true;

       }

 

-      public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options){

-Contract.Requires(options != null);

-Contract.Requires(node != null);

+      public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op != null);

         string funcName = op.Func.Name;

@@ -1008,7 +1034,8 @@ Contract.Requires(node != null);
         string bvzName = op.Func.FindStringAttribute("external");

         string printedName = ExprLineariser.Namer.GetName(op.Func, funcName);

         Contract.Assert(printedName != null);

-        if (bvzName != null) printedName = bvzName;

+        if (bvzName != null)

+          printedName = bvzName;

 

         if (options.UseTypes) {

           // we use term notation for arguments whose type is not bool, and

@@ -1022,7 +1049,7 @@ Contract.Requires(node != null);
             wr.Write(" ");

             ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

           }

-        

+

           wr.Write(")");

         } else {

           // arguments are always terms

@@ -1031,7 +1058,7 @@ Contract.Requires(node != null);
         }

         return true;

       }

-      

+

     }

   }