Boogie: Committing my port of the SMTLib project

1 files changed, 324 insertions, 148 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7efa109f..b211b8f4 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -8,7 +8,7 @@ using System.Text;
 using System.IO;

 using System.Collections;

 using System.Collections.Generic;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

 

@@ -23,7 +23,9 @@ namespace Microsoft.Boogie.SMTLib
   public class LineariserOptions {

 

     public readonly bool AsTerm;

-    public LineariserOptions! SetAsTerm(bool newVal) {

+    public LineariserOptions SetAsTerm(bool newVal) {

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

+

       if (newVal)

         return DefaultTerm;

       else

@@ -34,57 +36,88 @@ namespace Microsoft.Boogie.SMTLib
       this.AsTerm = asTerm;

     }

 

-    public static readonly LineariserOptions! Default = new LineariserOptions (false);

-    internal static readonly LineariserOptions! DefaultTerm = new LineariserOptions (true);

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(Default!=null);

+      Contract.Invariant(DefaultTerm!=null);

+}

+

+    public static readonly LineariserOptions Default = new LineariserOptions (false);

+    internal static readonly LineariserOptions DefaultTerm = new LineariserOptions (true);

   }

 

 

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

 

   // Lineariser for expressions. The result (bool) is currently not used for anything

-  public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {

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

+

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

+    Contract.Requires(e != null);

+    Contract.Requires(namer != null);

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

 

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

       StringWriter sw = new StringWriter();

-      SMTLibExprLineariser! lin = new SMTLibExprLineariser (sw, namer);

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

+      Contract.Assert(lin!=null);

       lin.Linearise(e, LineariserOptions.Default);

-      return (!)sw.ToString();

+      return cce.NonNull(sw.ToString());

     }

 

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

 

-    private readonly TextWriter! wr;

+    private readonly TextWriter wr;

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(wr!=null);

+      Contract.Invariant(Namer != null);

+}

+

     private SMTLibOpLineariser OpLinObject = null;

-    private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {

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

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

+

       if (OpLinObject == null)

-        OpLinObject = new SMTLibOpLineariser (this, wr);

+        OpLinObject = new SMTLibOpLineariser(this, wr);

       return OpLinObject;

     } }

 

-    internal readonly UniqueNamer! Namer;

+    internal readonly UniqueNamer Namer;

 

-    public SMTLibExprLineariser(TextWriter! wr, UniqueNamer! namer) {

+    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer) {

+      Contract.Requires(wr != null);Contract.Requires(namer != null);

       this.wr = wr;

       this.Namer = namer;

     }

 

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

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

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

+      Contract.Requires(expr != null);

+      Contract.Requires(options != null);

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

     }

 

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

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

+      Contract.Requires(expr != null);

+      Contract.Requires(options != null);

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

     }

 

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

 

-    internal static string! TypeToString(Type! t) {

+    internal static string TypeToString(Type t) {

+      Contract.Requires(t != null);

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

+

       if (t.IsBool)

         return "TermBool";

       else if (t.IsInt)

         return "Int";

-      else if (t.IsBv)

-        assert false; // bitvectors are currently not handled for SMT-Lib solvers

+      else if (t.IsBv) {

+        Contract.Assert(false);

+        throw new cce.UnreachableException();

+      } // bitvectors are currently not handled for SMT-Lib solvers

       else {

         // at this point, only the types U, T should be left

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

@@ -97,7 +130,10 @@ namespace Microsoft.Boogie.SMTLib
 

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

 

-    public static string! MakeIdPrintable(string! s) {

+    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:

@@ -114,7 +150,7 @@ namespace Microsoft.Boogie.SMTLib
         break;

       }

 

-      string! newS = "";

+      string newS = "";

       foreach (char ch in s) {

         if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_')

           newS = newS + ch;

@@ -136,58 +172,64 @@ namespace Microsoft.Boogie.SMTLib
     /// <summary>

     /// The name for logical conjunction in Simplify

     /// </summary>

-    internal const string! andName = "and"; // conjunction

-    internal const string! orName = "or"; // disjunction

-    internal const string! notName = "not"; // negation

-    internal const string! impliesName = "implies"; // implication

-    internal const string! iteName = "ite"; // if-then-else

-    internal const string! iffName = "iff"; // logical equivalence

-    internal const string! eqName = "="; // equality

-    internal const string! lessName = "<";

-    internal const string! greaterName = ">"; 

-    internal const string! atmostName = "<=";

-    internal const string! atleastName = ">=";

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

-    internal const string! FALSEName = "false"; // nullary predicate that is always false

-    internal const string! subtypeName = "UOrdering2";

-    internal const string! subtypeArgsName = "UOrdering3";

-

-    internal const string! distinctName = "distinct";

-

-    internal const string! boolTrueName = "boolTrue";

-    internal const string! boolFalseName = "boolFalse";

-    internal const string! boolAndName = "boolAnd";

-    internal const string! boolOrName = "boolOr";

-    internal const string! boolNotName = "boolNot";

-    internal const string! boolIffName = "boolIff";

-    internal const string! boolImpliesName = "boolImplies";

-    internal const string! boolIteName = "ite";

-    internal const string! termUEqual = "UEqual";

-    internal const string! termTEqual = "TEqual";

-    internal const string! termIntEqual = "IntEqual";

-    internal const string! termLessName = "intLess";

-    internal const string! termGreaterName = "intGreater";

-    internal const string! termAtmostName = "intAtMost";

-    internal const string! termAtleastName = "intAtLeast";

-    internal const string! intAddName = "+";

-    internal const string! intSubName = "-";

-    internal const string! intMulName = "*";

-    internal const string! intDivName = "boogieIntDiv";

-    internal const string! intModName = "boogieIntMod";

-

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

+    internal const string andName = "and"; // conjunction

+    internal const string orName = "or"; // disjunction

+    internal const string notName = "not"; // negation

+    internal const string impliesName = "implies"; // implication

+    internal const string iteName = "ite"; // if-then-else

+    internal const string iffName = "iff"; // logical equivalence

+    internal const string eqName = "="; // equality

+    internal const string lessName = "<";

+    internal const string greaterName = ">"; 

+    internal const string atmostName = "<=";

+    internal const string atleastName = ">=";

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

+    internal const string FALSEName = "false"; // nullary predicate that is always false

+    internal const string subtypeName = "UOrdering2";

+    internal const string subtypeArgsName = "UOrdering3";

+

+    internal const string distinctName = "distinct";

+

+    internal const string boolTrueName = "boolTrue";

+    internal const string boolFalseName = "boolFalse";

+    internal const string boolAndName = "boolAnd";

+    internal const string boolOrName = "boolOr";

+    internal const string boolNotName = "boolNot";

+    internal const string boolIffName = "boolIff";

+    internal const string boolImpliesName = "boolImplies";

+    internal const string boolIteName = "ite";

+    internal const string termUEqual = "UEqual";

+    internal const string termTEqual = "TEqual";

+    internal const string termIntEqual = "IntEqual";

+    internal const string termLessName = "intLess";

+    internal const string termGreaterName = "intGreater";

+    internal const string termAtmostName = "intAtMost";

+    internal const string termAtleastName = "intAtLeast";

+    internal const string intAddName = "+";

+    internal const string intSubName = "-";

+    internal const string intMulName = "*";

+    internal const string intDivName = "boogieIntDiv";

+    internal const string intModName = "boogieIntMod";

+

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

+      Contract.Requires(x != null);

+      Contract.Requires(options != null);

       if (!options.AsTerm)

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

     }

 

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

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

+    Contract.Requires(x != null);

+    Contract.Requires(options != null);

       if (options.AsTerm)

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

     }

 

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

 

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

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

+      Contract.Requires(node != null);

+      Contract.Requires(options != null);

       if (options.AsTerm) {

 

         if (node == VCExpressionGenerator.True)

@@ -202,8 +244,10 @@ namespace Microsoft.Boogie.SMTLib
             wr.Write("({0} 0 {1})", intSubName, lit.Abs);

           else

             wr.Write(lit);

-        } else

-          assert false;

+        } else {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        }

 

       } else {

 

@@ -214,7 +258,7 @@ namespace Microsoft.Boogie.SMTLib
         else if (node is VCExprIntLit) {

           System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");

         } else

-          assert false;

+         {Contract.Assert(false);  throw new cce.UnreachableException();}

 

       }

 

@@ -223,8 +267,12 @@ namespace Microsoft.Boogie.SMTLib
 

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

 

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

-      VCExprOp! op = node.Op;

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

+      Contract.Requires(node != null);

+      Contract.Requires(options != null);

+      

+      VCExprOp op = node.Op;

+      Contract.Assert(op!=null);

 

       if (!options.AsTerm &&

           (op.Equals(VCExpressionGenerator.AndOp) ||

@@ -233,12 +281,13 @@ namespace Microsoft.Boogie.SMTLib
 

         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)) {

             wr.Write(" ");

-            Linearise((VCExpr!)enumerator.Current, options);

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

           }

         }

 

@@ -247,13 +296,16 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

-      return node.Accept<bool, LineariserOptions!>(OpLineariser, options);

+      return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);

     }

 

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

 

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

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

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

+      Contract.Requires(node != null);

+      Contract.Requires(options != null);

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

+      Contract.Assert(printedName!=null);

 

       if (options.AsTerm ||

           // formula variables are easy to identify in SMT-Lib

@@ -267,21 +319,25 @@ namespace Microsoft.Boogie.SMTLib
 

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

 

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

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

+      Contract.Requires(node != null);

+      Contract.Requires(options != null);

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

-      assert node.TypeParameters.Count == 0;

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

 

       Namer.PushScope(); try {

 

-      string! kind = node.Quan == Quantifier.ALL ? "forall" : "exists";

+      string kind = node.Quan == Quantifier.ALL ? "forall" : "exists";

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

 

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

         {

-          VCExprVar! var = node.BoundVars[i];

+          VCExprVar var = node.BoundVars[i];

+          Contract.Assert(var!=null);

           // ensure that the variable name starts with ?

-          string! printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));

-          assert printedName[0] == '?';

+          string printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));

+        Contract.Assert(printedName!=null);

+         Contract.Assert(printedName[0] == '?');

           wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));

         }

         

@@ -312,11 +368,14 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

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

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

+      Contract.Requires(options != null);

+      Contract.Requires(triggers != null);

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

       int negTriggers = 0;

       int posTriggers = 0;

-      foreach (VCTrigger! vcTrig in triggers) {

+      foreach (VCTrigger vcTrig in triggers) {

+        Contract.Assert(vcTrig!=null);

         if (vcTrig.Pos) {

           posTriggers++;

         } else {

@@ -325,10 +384,12 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       if (posTriggers > 0) {

-        foreach (VCTrigger! vcTrig in triggers) {

+        foreach (VCTrigger vcTrig in triggers) {

+          Contract.Assert(vcTrig!=null);

           if (vcTrig.Pos) {

             wr.Write(" :pat {");

-            foreach (VCExpr! e in vcTrig.Exprs) {

+            foreach (VCExpr e in vcTrig.Exprs) {

+              Contract.Assert(e!=null);

               wr.Write(" ");

               LineariseAsTerm(e, options);

             }

@@ -339,10 +400,11 @@ namespace Microsoft.Boogie.SMTLib
         // if also positive triggers are given, the SMT solver (at least Z3)

         // will ignore the negative patterns and output a warning. Therefore

         // we never specify both negative and positive triggers

-        foreach (VCTrigger! vcTrig in triggers) {

+        foreach (VCTrigger vcTrig in triggers) {

+          Contract.Assert(vcTrig!=null);

           if (!vcTrig.Pos) {

             wr.Write(" :nopat { ");

-            assert vcTrig.Exprs.Count == 1;

+           Contract.Assert(vcTrig.Exprs.Count == 1);

             wr.Write(" ");

             LineariseAsTerm(vcTrig.Exprs[0], options);

             wr.Write(" } ");

@@ -353,15 +415,18 @@ namespace Microsoft.Boogie.SMTLib
 

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

 

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

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

+      Contract.Requires(node != null);

+      Contract.Requires(options != null);

       Namer.PushScope(); try {

 

-      foreach (VCExprLetBinding! b in node) {

+      foreach (VCExprLetBinding b in node) {

+        Contract.Assert(b != null);

         bool formula = b.V.Type.IsBool;

 

         wr.Write("({0} (", formula ? "flet" : "let");

-        string! printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name));

-        assert printedName[0] == '$';

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

+       Contract.Assert(printedName[0] == '$');

         

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

         Linearise(b.E, options.SetAsTerm(!formula));

@@ -382,48 +447,77 @@ namespace Microsoft.Boogie.SMTLib
     /////////////////////////////////////////////////////////////////////////////////////

 

     // Lineariser for operator terms. The result (bool) is currently not used for anything

-    internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions!> {

-      private readonly SMTLibExprLineariser! ExprLineariser;

-      private readonly TextWriter! wr;

+    internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> {

+      private readonly SMTLibExprLineariser ExprLineariser;

+      private readonly TextWriter wr;

+      [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(wr!=null);

+        Contract.Invariant(ExprLineariser!=null);

+}

+

 

-      public SMTLibOpLineariser(SMTLibExprLineariser! ExprLineariser, TextWriter! wr) {

+      public SMTLibOpLineariser(SMTLibExprLineariser ExprLineariser, TextWriter wr) {

+        Contract.Requires(ExprLineariser != null);

+        Contract.Requires(wr != null);

         this.ExprLineariser = ExprLineariser;

         this.wr = wr;

       }

 

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

 

-      private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,

-                                    LineariserOptions! options,

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

+                                    LineariserOptions options,

                                     bool argsAsTerms) {

+      Contract.Requires(op != null);

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

+      Contract.Requires(options != null);

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

       }

 

-      private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,

-                                    LineariserOptions! options) {

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

+                                    LineariserOptions options) {

+      Contract.Requires(op != null);

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

+      Contract.Requires(options != null);

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

       }

 

-      private void WriteTermApplication(string! op, IEnumerable<VCExpr!>! args,

-                                        LineariserOptions! options) {

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

+                                        LineariserOptions options) {

+        Contract.Requires(op != null);

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

+      Contract.Requires(options != null);

         ExprLineariser.AssertAsTerm(op, options);

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

       }

 

-      private void WriteApplication(string! termOp, string! predOp,

-                                    IEnumerable<VCExpr!>! args, LineariserOptions! options) {

+      private void WriteApplication(string termOp, string predOp,

+                                    IEnumerable<VCExpr/*!>!*/> args, LineariserOptions options) {

+        Contract.Requires(predOp != null);

+        Contract.Requires(termOp != null);

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

+      Contract.Requires(options != null);

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

       }

 

-      private void WriteApplication(string! termOp, string! predOp,

-                                    IEnumerable<VCExpr!>! args, LineariserOptions! options,

+      private void WriteApplication(string termOp, string predOp,

+                                    IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,

                                     // change the AsTerm option for the arguments?

                                     bool argsAsTerms) {

-        string! opName = options.AsTerm ? termOp : predOp;

-        LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms);

+      Contract.Requires(predOp != null);

+        Contract.Requires(termOp != null);

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

+      Contract.Requires(options != null);

+        string opName = options.AsTerm ? termOp : predOp;

+        Contract.Assert(opName!=null);

+        LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);

+        Contract.Assert(newOptions!=null);

 

         bool hasArgs = false;

-        foreach (VCExpr! e in args) {

+        foreach (VCExpr e in args) {

+          Contract.Assert(e!=null);

           if (!hasArgs)

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

           wr.Write(" ");

@@ -440,8 +534,11 @@ namespace Microsoft.Boogie.SMTLib
       // 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) {

+      private void WriteApplicationTermOnly(string termOp,

+                                            IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options) {

+        Contract.Requires(termOp != null);

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

+        Contract.Requires(options != null);

         if (!options.AsTerm)

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

           // where "args" are written as terms

@@ -455,15 +552,19 @@ namespace Microsoft.Boogie.SMTLib
 

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

       

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

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

         return true;

       }

 

-      private bool PrintEq(VCExprNAry! node, LineariserOptions! options) {

+      private bool PrintEq(VCExprNAry node, LineariserOptions options) {

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

         if (options.AsTerm) {

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

-          assert node[0].Type.Equals(node[1].Type);

+         Contract.Assert(node[0].Type.Equals(node[1].Type));

           if (node[0].Type.IsBool) {

             WriteApplication(boolIffName, node, options);

           } else if (node[0].Type.IsInt) {

@@ -476,12 +577,12 @@ namespace Microsoft.Boogie.SMTLib
             } else if (t != null && t.Decl.Name.Equals("T")) {

               WriteApplication(termTEqual, node, options);

             } else {

-              assert false;   // unknown type

+             {Contract.Assert(false);  throw new cce.UnreachableException();}   // unknown type

             }

           }

         } else {

           if (node[0].Type.IsBool) {

-            assert node[1].Type.IsBool;

+           Contract.Assert(node[1].Type.IsBool);

             // use equivalence

             WriteApplication(iffName, node, options);

           } else {

@@ -493,47 +594,66 @@ namespace Microsoft.Boogie.SMTLib
         return true;        

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

         return PrintEq(node, options);

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

         wr.Write("({0} ", options.AsTerm ? boolNotName : notName);

         PrintEq(node, options);

         wr.Write(")");

         return true;

       }

 

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

-        assert options.AsTerm;

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       Contract.Assert(options.AsTerm);

         WriteApplication(boolAndName, andName, node, options);

         return true;

       }

 

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

-        assert options.AsTerm;

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

+      Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+       Contract.Assert(options.AsTerm);

         WriteApplication(boolOrName, orName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteApplication(boolImpliesName, impliesName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteApplication(boolIteName, iteName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         ExprLineariser.AssertAsFormula(distinctName, options);

         

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);

         } else {

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

-          foreach (VCExpr! e in node) {

+          foreach (VCExpr e in node) {

+            Contract.Assert(e!=null);

             wr.Write(" ");

             ExprLineariser.LineariseAsTerm(e, options);

           }

@@ -543,7 +663,10 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+        Contract.Requires(node.Length>=1);

         // VCExprLabelOp! op = (VCExprLabelOp)node.Op;

         // TODO

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

@@ -552,84 +675,137 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

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

-        assert false;      // should not occur in the output

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

+       Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+       {Contract.Assert(false);  throw new cce.UnreachableException();}      // should not occur in the output

       }

 

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

-        assert false;       // should not occur in the output

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+       {Contract.Assert(false);  throw new cce.UnreachableException();}       // should not occur in the output

       }

 

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

-        assert false;       // TODO

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+       {Contract.Assert(false);  throw new NotImplementedException();}       // TODO

       }

 

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

-        assert false;       // TODO

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+       {Contract.Assert(false);  throw new NotImplementedException();}       // TODO

       }

 

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

-        assert false;       // TODO

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+       {Contract.Assert(false);  throw new NotImplementedException();}       // TODO

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteTermApplication(intAddName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteTermApplication(intSubName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteTermApplication(intMulName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteTermApplication(intDivName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

         WriteTermApplication(intModName, node, options);

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

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

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

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

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

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

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

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

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

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

         return true;

       }

 

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

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

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

         return true;

       }

 

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

-        VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;

-        string! printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));

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

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+       

+        VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

+        Contract.Assert(op!=null);

+        string printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));

+        Contract.Assert(printedName!=null);

 

         // arguments are always terms

         WriteApplicationTermOnly(printedName, node, options);