Boogie: Committing my port of the SMTLib project

6 files changed, 633 insertions, 364 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 5ef78532..364fd29c 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -5,8 +5,6 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758
 EndProject

 Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Simplify", "Provers\Simplify\Simplify.sscproj", "{F75666DE-FB56-457C-8782-09BE243450FC}"

 EndProject

-Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "SMTLib", "Provers\SMTLib\SMTLib.sscproj", "{13C3A68C-462A-4CDA-A480-738046E37C5A}"

-EndProject

 Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "AIFramework", "AIFramework\AIFramework.sscproj", "{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"

 EndProject

 Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Basetypes", "Basetypes\Basetypes.sscproj", "{0C692837-77EC-415F-BF04-395E3ED06E9A}"

@@ -27,6 +25,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csp
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3", "Provers\Z3\Z3.csproj", "{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

@@ -47,16 +47,6 @@ Global
 		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET

 		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET

 		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|.NET.ActiveCfg = Debug|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|.NET.Build.0 = Debug|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Any CPU.ActiveCfg = Debug|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Mixed Platforms.Build.0 = Debug|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|.NET.ActiveCfg = Release|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|.NET.Build.0 = Release|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|Any CPU.ActiveCfg = Release|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|Mixed Platforms.ActiveCfg = Release|.NET

-		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|.NET.ActiveCfg = Debug|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|.NET.Build.0 = Debug|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|Any CPU.ActiveCfg = Debug|.NET

@@ -159,14 +149,24 @@ Global
 		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.Build.0 = Release|Any CPU

 		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|.NET.ActiveCfg = Release|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.Build.0 = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

 	EndGlobalSection

 	GlobalSection(NestedProjects) = preSolution

 		{F75666DE-FB56-457C-8782-09BE243450FC} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

-		{13C3A68C-462A-4CDA-A480-738046E37C5A} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

 		{435D5BD0-6F62-49F8-BB24-33E2257519AD} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

 		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

+		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

 	EndGlobalSection

 EndGlobal

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index c87c8fa4..a036c7e5 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -117,8 +117,8 @@
       <Project>{F75666DE-FB56-457C-8782-09BE243450FC}</Project>

       <Name>Simplify</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Provers\SMTLib\SMTLib.sscproj">

-      <Project>{13C3A68C-462A-4CDA-A480-738046E37C5A}</Project>

+    <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">

+      <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>

     </ProjectReference>

     <ProjectReference Include="..\Provers\Z3\Z3.csproj">

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index b55cc403..4b4d7431 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -8,9 +8,9 @@ using System.Collections;
 using System.Collections.Generic;

 using System.Threading;

 using System.IO;

-using ExternalProver;

+//using ExternalProver;

 using System.Diagnostics;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.VCExprAST;

@@ -22,17 +22,35 @@ namespace Microsoft.Boogie.SMTLib
 {

   public class SMTLibProcessTheoremProver : LogProverInterface

   {

-    private readonly DeclFreeProverContext! ctx;

+    private readonly DeclFreeProverContext ctx;

 

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(ctx!=null);

+      Contract.Invariant(AxBuilder != null);

+      Contract.Invariant(Namer != null);

+      Contract.Invariant(DeclCollector != null);

+      Contract.Invariant(BadBenchmarkWords != null);

+      Contract.Invariant(cce.NonNullElements(Axioms));

+      Contract.Invariant(cce.NonNullElements(TypeDecls));

+      Contract.Invariant(_backgroundPredicates != null);

+

+}

+

+    

     [NotDelayed]

-    public SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen,

-                                      DeclFreeProverContext! ctx)

+    public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,

+                                      DeclFreeProverContext ctx):base(options, "", "", "", "", gen)

     {

+      Contract.Requires(options != null);

+      Contract.Requires(gen != null);

+      Contract.Requires(ctx != null);

       InitializeGlobalInformation("UnivBackPred2.smt");

 

       this.ctx = ctx;

 

-      TypeAxiomBuilder! axBuilder;

+      TypeAxiomBuilder axBuilder;

       switch (CommandLineOptions.Clo.TypeEncodingMethod) {

         case CommandLineOptions.TypeEncoding.Arguments:

           axBuilder = new TypeAxiomBuilderArguments (gen);

@@ -46,27 +64,36 @@ namespace Microsoft.Boogie.SMTLib
       UniqueNamer namer = new UniqueNamer ();

       Namer = namer;

       this.DeclCollector = new TypeDeclCollector (namer);

-      base(options, "", "", "", "", gen);

+      

     }

     

-    public override ProverContext! Context { get {

+    public override ProverContext Context { get {

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

+

       return ctx;

     } }

 

-    private readonly TypeAxiomBuilder! AxBuilder;

-    private readonly UniqueNamer! Namer;

-    private readonly TypeDeclCollector! DeclCollector;

+    private readonly TypeAxiomBuilder AxBuilder;

+    private readonly UniqueNamer Namer;

+    private readonly TypeDeclCollector DeclCollector;

 

     private void FeedTypeDeclsToProver() {

-      foreach (string! s in DeclCollector.GetNewDeclarations())

+      foreach (string s in DeclCollector.GetNewDeclarations())

+      {

+        Contract.Assert(s!=null);

         AddTypeDecl(s);

-    }

+    }}

 

-    public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) {

-      TextWriter! output = OpenOutputFile(descriptiveName);

+    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {

+      Contract.Requires(descriptiveName != null);

+      Contract.Requires(vc != null);

+      Contract.Requires(handler != null);

+      TextWriter output = OpenOutputFile(descriptiveName);

+      Contract.Assert(output!=null);

 

-      string! name =

+      string name =

         MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName));

+      Contract.Assert(name!=null);

       WriteLineAndLog(output, "(benchmark " + name);

       WriteLineAndLog(output, _backgroundPredicates);

 

@@ -76,13 +103,16 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";

-      string! prelude = ctx.GetProverCommands(true);

+      string prelude = ctx.GetProverCommands(true);

+      Contract.Assert(prelude!=null);

       WriteLineAndLog(output, prelude);

 

-      foreach (string! s in TypeDecls) {

+      foreach (string s in TypeDecls) {

+        Contract.Assert(s!=null);

         WriteLineAndLog(output, s);

       }

-      foreach (string! s in Axioms) {

+      foreach (string s in Axioms) {

+        Contract.Assert(s!=null);

         WriteLineAndLog(output, ":assumption");

         WriteLineAndLog(output, s);

       }

@@ -95,41 +125,53 @@ namespace Microsoft.Boogie.SMTLib
 

     // certain words that should not occur in the name of a benchmark

     // because some solvers don't like them

-    private readonly static List<string!>! BadBenchmarkWords = new List<string!> ();

+    private readonly static List<string/*!>!*/> BadBenchmarkWords = new List<string/*!*/> ();

     static SMTLibProcessTheoremProver() {

       BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");

     }

 

-    private string! MakeBenchmarkNameSafe(string! name) {

+    private string MakeBenchmarkNameSafe(string name) {

+      Contract.Requires(name != null);

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

+

       for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2)

         name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i+1]);

       return name;

     }

 

-    private TextWriter! OpenOutputFile(string! descriptiveName) {

+    private TextWriter OpenOutputFile(string descriptiveName) {

+      Contract.Requires(descriptiveName != null);

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

+

         string filename = CommandLineOptions.Clo.SMTLibOutputPath;

-        filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename);

+        filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));

         return new StreamWriter(filename, false);

     }

 

-    private void WriteLineAndLog(TextWriter! output, string! msg) {

+    private void WriteLineAndLog(TextWriter output, string msg) {

+      Contract.Requires(output != null);

+      Contract.Requires(msg != null);

       LogActivity(msg);

       output.WriteLine(msg);

     }

 

     [NoDefaultContract]

-    public override Outcome CheckOutcome(ErrorHandler! handler)

-      throws UnexpectedProverOutputException; {

+    public override Outcome CheckOutcome(ErrorHandler handler)

+   {Contract.Requires(handler != null);

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       return Outcome.Undetermined;

     }

 

-    protected string! VCExpr2String(VCExpr! expr, int polarity) {

+    protected string VCExpr2String(VCExpr expr, int polarity) {

+      Contract.Requires(expr != null);

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

+

       DateTime start = DateTime.Now;

       if (CommandLineOptions.Clo.Trace)

         Console.Write("Linearising ... ");

 

       // handle the types in the VCExpr

-      TypeEraser! eraser;

+      TypeEraser eraser;

       switch (CommandLineOptions.Clo.TypeEncodingMethod) {

         case CommandLineOptions.TypeEncoding.Arguments:

           eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);

@@ -138,18 +180,24 @@ namespace Microsoft.Boogie.SMTLib
           eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);

           break;

       }

-      VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);

+      Contract.Assert(eraser!=null);

+      VCExpr exprWithoutTypes = eraser.Erase(expr, polarity);

+      Contract.Assert(exprWithoutTypes!=null);

 

-      LetBindingSorter! letSorter = new LetBindingSorter(gen);

-      VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);

-      VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);

+      LetBindingSorter letSorter = new LetBindingSorter(gen);

+      Contract.Assert(letSorter!=null);

+      VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);

+      Contract.Assert(sortedExpr!=null);

+      VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);

+      Contract.Assert(sortedAxioms!=null);

 

       DeclCollector.Collect(sortedAxioms);

       DeclCollector.Collect(sortedExpr);

       FeedTypeDeclsToProver();

 

       AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer));

-      string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer);

+      string res = SMTLibExprLineariser.ToString(sortedExpr, Namer);

+      Contract.Assert(res!=null);

 

       if (CommandLineOptions.Clo.Trace) {

         DateTime end = DateTime.Now;

@@ -161,13 +209,17 @@ namespace Microsoft.Boogie.SMTLib
 

     // the list of all known axioms, where have to be included in each

     // verification condition

-    private readonly List<string!>! Axioms = new List<string!> ();

+    private readonly List<string/*!>!*/> Axioms = new List<string/*!*/> ();

     private bool AxiomsAreSetup = false;

+    

+

+

 

     // similarly, a list of function/predicate declarations

-    private readonly List<string!>! TypeDecls = new List<string!> ();

+    private readonly List<string/*!>!*/> TypeDecls = new List<string/*!*/> ();

 

-    protected void AddAxiom(string! axiom) {

+    protected void AddAxiom(string axiom) {

+      Contract.Requires(axiom != null);

       Axioms.Add(axiom);

 //      if (thmProver != null) {

 //        LogActivity(":assume " + axiom);

@@ -175,7 +227,8 @@ namespace Microsoft.Boogie.SMTLib
 //      }

     }

 

-    protected void AddTypeDecl(string! decl) {

+    protected void AddTypeDecl(string decl) {

+      Contract.Requires(decl != null);

       TypeDecls.Add(decl);

  //     if (thmProver != null) {

  //       LogActivity(decl);

@@ -185,15 +238,15 @@ namespace Microsoft.Boogie.SMTLib
 

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

 

-    private static string! _backgroundPredicates;

+    private static string _backgroundPredicates;

 

-    static void InitializeGlobalInformation(string! backgroundPred)

-      ensures _backgroundPredicates != null;

+    static void InitializeGlobalInformation(string backgroundPred)

+    {Contract.Requires(backgroundPred != null);

+     Contract.Ensures(_backgroundPredicates != null);

       //throws ProverException, System.IO.FileNotFoundException;

-    {

       if (_backgroundPredicates == null) {

-        string! codebaseString =

-          (!) Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);

+        string codebaseString =

+          cce.NonNull(Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));

 

         // Initialize '_backgroundPredicates'

         string univBackPredPath = Path.Combine(codebaseString, backgroundPred);

@@ -208,32 +261,45 @@ namespace Microsoft.Boogie.SMTLib
   public class Factory : ProverFactory

   {

 

-    public override object! SpawnProver(ProverOptions! options, object! ctxt)

+    public override object SpawnProver(ProverOptions options, object ctxt)

     {

+    Contract.Requires(ctxt != null);

+    Contract.Requires(options != null);

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

+

       return this.SpawnProver(options,

-                              ((DeclFreeProverContext!)ctxt).ExprGen,

-                              (DeclFreeProverContext!)ctxt);

+                              cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,

+                              cce.NonNull((DeclFreeProverContext)ctxt));

     }

 

-    public override object! NewProverContext(ProverOptions! options) {

+    public override object NewProverContext(ProverOptions options) {

+      Contract.Requires(options != null);

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

+

       if (CommandLineOptions.Clo.BracketIdsInVC < 0) {

         CommandLineOptions.Clo.BracketIdsInVC = 0;

       }

 

-      VCExpressionGenerator! gen = new VCExpressionGenerator ();

-      List<string!>! proverCommands = new List<string!> ();

+      VCExpressionGenerator gen = new VCExpressionGenerator ();

+      List<string>/*!>!*/ proverCommands = new List<string/*!*/> ();

 // TODO: what is supported?

 //      proverCommands.Add("all");

 //      proverCommands.Add("simplify");

 //      proverCommands.Add("simplifyLike");

-      VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands);

+      VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);

+      Contract.Assert(genOptions!=null);

 

       return new DeclFreeProverContext(gen, genOptions);

     }

 

-    protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options,

-                                                              VCExpressionGenerator! gen,

-                                                              DeclFreeProverContext! ctx) {

+    protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options,

+                                                              VCExpressionGenerator gen,

+                                                              DeclFreeProverContext ctx) {

+      Contract.Requires(options != null);

+      Contract.Requires(gen != null);

+      Contract.Requires(ctx != null);

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

+

       return new SMTLibProcessTheoremProver(options, gen, ctx);

     }

   }

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 884f3084..37ea2536 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -1,120 +1,120 @@
-<?xml version="1.0" encoding="utf-8"?>

-<VisualStudioProject>

-  <XEN ProjectType="Local"

-     SchemaVersion="1.0"

-     Name="SMTLib"

-     ProjectGuid="13c3a68c-462a-4cda-a480-738046e37c5a"

-    >

-    <Build>

-      <Settings ApplicationIcon=""

-         AssemblyName="Provers.SMTLib"

-         OutputType="Library"

-         RootNamespace="Microsoft.Boogie.SMTLib"

-         StartupObject=""

-         StandardLibraryLocation=""

-         TargetPlatform="v2"

-         TargetPlatformLocation=""

-         ShadowedAssembly=""

-         NoStandardLibraries="False"

-        >

-        <Config Name="Debug"

-           AllowUnsafeBlocks="False"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="False"

-           ConfigurationOverrideFile=""

-           DefineConstants="DEBUG;TRACE"

-           DocumentationFile=""

-           DebugSymbols="True"

-           FileAlignment="4096"

-           IncrementalBuild="True"

-           Optimize="False"

-           OutputPath="bin\debug"

-           RegisterForComInterop="False"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="False"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-        <Config Name="Release"

-           AllowUnsafeBlocks="false"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="false"

-           ConfigurationOverrideFile=""

-           DefineConstants="TRACE"

-           DocumentationFile=""

-           DebugSymbols="false"

-           FileAlignment="4096"

-           IncrementalBuild="false"

-           Optimize="true"

-           OutputPath="bin\release"

-           RegisterForComInterop="false"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="false"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-      </Settings>

-      <References>

-        <Reference Name="System"

-             AssemblyName="System"

-             Private="false"

-             />

-        <Reference Name="System.Data"

-             AssemblyName="System.Data"

-             Private="false"

-             />

-        <Reference Name="System.Xml"

-             AssemblyName="System.Xml"

-             Private="false"

-             />

-        <Reference Name="Basetypes"

-             Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"

-             Private="true"

-             />

-        <Reference Name="Core"

-             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"

-             Private="true"

-             />

-        <Reference Name="VCExpr"

-             Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"

-             Private="true"

-             />

-        <Reference Name="VCGeneration"

-             Project="{F65666DE-FB56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-        <Reference Name="Mscorlib.Contracts"

-             AssemblyName="Mscorlib.Contracts"

-             Private="false"

-             HintPath="../../../Binaries/Mscorlib.Contracts.dll"

-             />

-        <Reference Name="Simplify"

-             Project="{F75666DE-FB56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-      </References>

-    </Build>

-    <Files>

-      <Include>

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="ProverInterface.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="SMTLibLineariser.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="TypeDeclCollector.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AssemblyInfo.ssc"

-                 />

-      </Include>

-    </Files>

-  </XEN>

-</VisualStudioProject>
\ No newline at end of file
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>9.0.30729</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>Microsoft.Boogie.SMTLib</RootNamespace>

+    <AssemblyName>Provers.SMTLib</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly>

+    </CodeContractsCustomRewriterAssembly>

+    <CodeContractsCustomRewriterClass>

+    </CodeContractsCustomRewriterClass>

+    <CodeContractsLibPaths>

+    </CodeContractsLibPaths>

+    <CodeContractsExtraRewriteOptions>

+    </CodeContractsExtraRewriteOptions>

+    <CodeContractsExtraAnalysisOptions>

+    </CodeContractsExtraAnalysisOptions>

+    <CodeContractsBaseLineFile>

+    </CodeContractsBaseLineFile>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\AIFramework\bin\debug\AIFramework.dll</HintPath>

+    </Reference>

+    <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Basetypes\bin\debug\Basetypes.dll</HintPath>

+    </Reference>

+    <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Core\bin\Debug\Core.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

+    <Reference Include="Provers.Simplify, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\Simplify\bin\debug\Provers.Simplify.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Core">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+    <Reference Include="VCExpr, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\VCExpr\bin\debug\VCExpr.dll</HintPath>

+    </Reference>

+    <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\VCGeneration\bin\debug\VCGeneration.dll</HintPath>

+    </Reference>

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="cce.cs" />

+    <Compile Include="ProverInterface.cs" />

+    <Compile Include="SMTLibLineariser.cs" />

+    <Compile Include="TypeDeclCollector.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Properties\" />

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
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);

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 08c0e6a3..a0d56601 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -7,7 +7,7 @@ using System;
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Boogie.VCExprAST;

 

 namespace Microsoft.Boogie.SMTLib

@@ -17,68 +17,93 @@ namespace Microsoft.Boogie.SMTLib
 

   public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

 

-    private readonly UniqueNamer! Namer;

+    private readonly UniqueNamer Namer;

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(Namer!=null);

+      Contract.Invariant(AllDecls != null);

+      Contract.Invariant(IncDecls != null);

+      Contract.Invariant(KnownFunctions != null);

+      Contract.Invariant(KnownVariables != null);

+}

+

 

-    public TypeDeclCollector(UniqueNamer! namer) {

+    public TypeDeclCollector(UniqueNamer namer) {

+      Contract.Requires(namer != null);

       this.Namer = namer;

     }

 

     // not used

-    protected override bool StandardResult(VCExpr! node, bool arg) {

+    protected override bool StandardResult(VCExpr node, bool arg) {

+      Contract.Requires(node != null);

       return true;

     }

 

-    private readonly List<string!>! AllDecls = new List<string!> ();

-    private readonly List<string!>! IncDecls = new List<string!> ();

+    private readonly List<string/*!>!*/> AllDecls = new List<string/*!*/> ();

+    private readonly List<string/*!>!*/> IncDecls = new List<string/*!*/> ();

+

+    private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions =

+      new Dictionary<Function/*!*/, bool> ();

+    private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =

+      new Dictionary<VCExprVar/*!*/, bool> ();

 

-    private readonly IDictionary<Function!, bool>! KnownFunctions =

-      new Dictionary<Function!, bool> ();

-    private readonly IDictionary<VCExprVar!, bool>! KnownVariables =

-      new Dictionary<VCExprVar!, bool> ();

+    public List<string/*!>!*/> AllDeclarations { get {

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

 

-    public List<string!>! AllDeclarations { get {

-      List<string!>! res = new List<string!> ();

+      List<string>/*!>!*/ res = new List<string/*!*/> ();

       res.AddRange(AllDecls);

       return res;

     } }

 

-    public List<string!>! GetNewDeclarations() {

-      List<string!>! res = new List<string!> ();

+    public List<string/*!>!*/> GetNewDeclarations() {

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

+      List<string>/*!>!*/ res = new List<string/*!*/>();

       res.AddRange(IncDecls);

       IncDecls.Clear();

       return res;

     }

 

-    private void AddDeclaration(string! decl) {

+    private void AddDeclaration(string decl) {

+      Contract.Requires(decl != null);

       AllDecls.Add(decl);

       IncDecls.Add(decl);

     }

 

-    public void Collect(VCExpr! expr) {

+    public void Collect(VCExpr expr) {

+      Contract.Requires(expr != null);

       Traverse(expr, true);

     }

 

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

 

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

+    private static string TypeToString(Type t) {

+      Contract.Requires(t != null);

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

+

       return SMTLibExprLineariser.TypeToString(t);

     }

 

-    public override bool Visit(VCExprNAry! node, bool arg) {

+    public override bool Visit(VCExprNAry node, bool arg) {

+      Contract.Requires(node != null);

       // there are a couple of cases where operators have to be

       // registered by generating appropriate statements

 

       VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

       if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

-        Function! f = op.Func;

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

-        string! decl = ":extrafuns ((" + printedName;

-

-        foreach (Variable! v in f.InParams) {

+        Function f = op.Func;

+        Contract.Assert(f!=null);

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

+        Contract.Assert(printedName!=null);

+        string decl = ":extrafuns ((" + printedName;

+

+        foreach (Variable v in f.InParams) {

+          Contract.Assert(v!=null);

           decl += " " + TypeToString(v.TypedIdent.Type);

         }

-        assert f.OutParams.Length == 1;

-        foreach (Variable! v in f.OutParams) {

+       Contract.Assert(f.OutParams.Length == 1);

+        foreach (Variable v in f.OutParams) {

+          Contract.Assert(v!=null);

           decl += " " + TypeToString(v.TypedIdent.Type);

         }

 

@@ -91,10 +116,12 @@ namespace Microsoft.Boogie.SMTLib
       return base.Visit(node, arg);

     }

 

-    public override bool Visit(VCExprVar! node, bool arg) {

+    public override bool Visit(VCExprVar node, bool arg) {

+      Contract.Requires(node != null);

       if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {

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

-        string! decl =

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

+        Contract.Assert(printedName!=null);

+        string decl =

           ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";

         AddDeclaration(decl);

         KnownVariables.Add(node, true);