Initial set of files.

author: mikebarnett <unknown> 2009-07-15 21:03:41 +0000
committer: mikebarnett <unknown> 2009-07-15 21:03:41 +0000
commit: ce1c2de044c91624370411e23acab13b0381949b (patch)
tree: 592539996fe08050ead5ee210c973801611dde40 /Source/Provers
13 files changed, 4327 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.ssc b/Source/Provers/SMTLib/ProverInterface.ssc
new file mode 100644
index 00000000..b55cc403
--- /dev/null
+++ b/Source/Provers/SMTLib/ProverInterface.ssc
@@ -0,0 +1,240 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using ExternalProver;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Clustering;
+using Microsoft.Boogie.TypeErasure;
+using Microsoft.Boogie.Simplify;
+
+namespace Microsoft.Boogie.SMTLib
+{
+  public class SMTLibProcessTheoremProver : LogProverInterface
+  {
+    private readonly DeclFreeProverContext! ctx;
+
+    [NotDelayed]
+    public SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen,
+                                      DeclFreeProverContext! ctx)
+    {
+      InitializeGlobalInformation("UnivBackPred2.smt");
+
+      this.ctx = ctx;
+
+      TypeAxiomBuilder! axBuilder;
+      switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+        case CommandLineOptions.TypeEncoding.Arguments:
+          axBuilder = new TypeAxiomBuilderArguments (gen);
+          break;
+        default:
+          axBuilder = new TypeAxiomBuilderPremisses (gen);
+          break;
+      }
+      axBuilder.Setup();
+      AxBuilder = axBuilder;
+      UniqueNamer namer = new UniqueNamer ();
+      Namer = namer;
+      this.DeclCollector = new TypeDeclCollector (namer);
+      base(options, "", "", "", "", gen);
+    }
+    
+    public override ProverContext! Context { get {
+      return ctx;
+    } }
+
+    private readonly TypeAxiomBuilder! AxBuilder;
+    private readonly UniqueNamer! Namer;
+    private readonly TypeDeclCollector! DeclCollector;
+
+    private void FeedTypeDeclsToProver() {
+      foreach (string! s in DeclCollector.GetNewDeclarations())
+        AddTypeDecl(s);
+    }
+
+    public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) {
+      TextWriter! output = OpenOutputFile(descriptiveName);
+
+      string! name =
+        MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName));
+      WriteLineAndLog(output, "(benchmark " + name);
+      WriteLineAndLog(output, _backgroundPredicates);
+
+      if (!AxiomsAreSetup) {
+        AddAxiom(VCExpr2String(ctx.Axioms, -1));
+        AxiomsAreSetup = true;
+      }
+
+      string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";
+      string! prelude = ctx.GetProverCommands(true);
+      WriteLineAndLog(output, prelude);
+
+      foreach (string! s in TypeDecls) {
+        WriteLineAndLog(output, s);
+      }
+      foreach (string! s in Axioms) {
+        WriteLineAndLog(output, ":assumption");
+        WriteLineAndLog(output, s);
+      }
+
+      WriteLineAndLog(output, vcString);
+      WriteLineAndLog(output, ")");
+
+      output.Close();
+    }
+
+    // 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!> ();
+    static SMTLibProcessTheoremProver() {
+      BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");
+    }
+
+    private string! MakeBenchmarkNameSafe(string! name) {
+      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) {
+        string filename = CommandLineOptions.Clo.SMTLibOutputPath;
+        filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename);
+        return new StreamWriter(filename, false);
+    }
+
+    private void WriteLineAndLog(TextWriter! output, string! msg) {
+      LogActivity(msg);
+      output.WriteLine(msg);
+    }
+
+    [NoDefaultContract]
+    public override Outcome CheckOutcome(ErrorHandler! handler)
+      throws UnexpectedProverOutputException; {
+      return Outcome.Undetermined;
+    }
+
+    protected string! VCExpr2String(VCExpr! expr, int polarity) {
+      DateTime start = DateTime.Now;
+      if (CommandLineOptions.Clo.Trace)
+        Console.Write("Linearising ... ");
+
+      // handle the types in the VCExpr
+      TypeEraser! eraser;
+      switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+        case CommandLineOptions.TypeEncoding.Arguments:
+          eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);
+          break;
+        default:
+          eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);
+          break;
+      }
+      VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);
+
+      LetBindingSorter! letSorter = new LetBindingSorter(gen);
+      VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
+      VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+
+      DeclCollector.Collect(sortedAxioms);
+      DeclCollector.Collect(sortedExpr);
+      FeedTypeDeclsToProver();
+
+      AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer));
+      string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer);
+
+      if (CommandLineOptions.Clo.Trace) {
+        DateTime end = DateTime.Now;
+        TimeSpan elapsed = end - start;
+        Console.WriteLine("finished   [{0} s]  ", elapsed.TotalSeconds);
+      }
+      return res;
+    }
+
+    // the list of all known axioms, where have to be included in each
+    // verification condition
+    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!> ();
+
+    protected void AddAxiom(string! axiom) {
+      Axioms.Add(axiom);
+//      if (thmProver != null) {
+//        LogActivity(":assume " + axiom);
+//        thmProver.AddAxioms(axiom);
+//      }
+    }
+
+    protected void AddTypeDecl(string! decl) {
+      TypeDecls.Add(decl);
+ //     if (thmProver != null) {
+ //       LogActivity(decl);
+ //       thmProver.Feed(decl, 0);
+ //     }
+    }
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    private static string! _backgroundPredicates;
+
+    static void InitializeGlobalInformation(string! backgroundPred)
+      ensures _backgroundPredicates != null;
+      //throws ProverException, System.IO.FileNotFoundException;
+    {
+      if (_backgroundPredicates == null) {
+        string! codebaseString =
+          (!) Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+
+        // Initialize '_backgroundPredicates'
+        string univBackPredPath = Path.Combine(codebaseString, backgroundPred);
+        using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
+        {
+          _backgroundPredicates = reader.ReadToEnd();
+        }
+      }
+    }
+  }
+
+  public class Factory : ProverFactory
+  {
+
+    public override object! SpawnProver(ProverOptions! options, object! ctxt)
+    {
+      return this.SpawnProver(options,
+                              ((DeclFreeProverContext!)ctxt).ExprGen,
+                              (DeclFreeProverContext!)ctxt);
+    }
+
+    public override object! NewProverContext(ProverOptions! options) {
+      if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+        CommandLineOptions.Clo.BracketIdsInVC = 0;
+      }
+
+      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);
+
+      return new DeclFreeProverContext(gen, genOptions);
+    }
+
+    protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options,
+                                                              VCExpressionGenerator! gen,
+                                                              DeclFreeProverContext! ctx) {
+      return new SMTLibProcessTheoremProver(options, gen, ctx);
+    }
+  }
+}
diff --git a/Source/Provers/SMTLib/SMTLib.sscproj b/Source/Provers/SMTLib/SMTLib.sscproj
new file mode 100644
index 00000000..d618b0dd
--- /dev/null
+++ b/Source/Provers/SMTLib/SMTLib.sscproj
@@ -0,0 +1,116 @@
+<?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"
+                 />
+      </Include>
+    </Files>
+  </XEN>
+</VisualStudioProject>
+\ No newline at end of file
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.ssc b/Source/Provers/SMTLib/SMTLibLineariser.ssc
new file mode 100644
index 00000000..cbf69107
--- /dev/null
+++ b/Source/Provers/SMTLib/SMTLibLineariser.ssc
@@ -0,0 +1,635 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+// Method to turn VCExprs into strings that can be fed into SMT
+// solvers. This is currently quite similar to the
+// SimplifyLikeLineariser (but the code is independent)
+
+namespace Microsoft.Boogie.SMTLib
+{
+
+  // Options for the linearisation
+  public class LineariserOptions {
+
+    public readonly bool AsTerm;
+    public LineariserOptions! SetAsTerm(bool newVal) {
+      if (newVal)
+        return DefaultTerm;
+      else
+        return Default;
+    }
+
+    internal LineariserOptions(bool asTerm) {
+      this.AsTerm = asTerm;
+    }
+
+    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 static string! ToString(VCExpr! e, UniqueNamer! namer) {
+      StringWriter sw = new StringWriter();
+      SMTLibExprLineariser! lin = new SMTLibExprLineariser (sw, namer);
+      lin.Linearise(e, LineariserOptions.Default);
+      return (!)sw.ToString();
+    }
+
+    ////////////////////////////////////////////////////////////////////////////////////////
+
+    private readonly TextWriter! wr;
+    private SMTLibOpLineariser OpLinObject = null;
+    private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {
+      if (OpLinObject == null)
+        OpLinObject = new SMTLibOpLineariser (this, wr);
+      return OpLinObject;
+    } }
+
+    internal readonly UniqueNamer! Namer;
+
+    public SMTLibExprLineariser(TextWriter! wr, UniqueNamer! namer) {
+      this.wr = wr;
+      this.Namer = namer;
+    }
+
+    public void Linearise(VCExpr! expr, LineariserOptions! options) {
+      expr.Accept<bool, LineariserOptions!>(this, options);
+    }
+
+    public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) {
+      Linearise(expr, options.SetAsTerm(true));
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    internal static string! TypeToString(Type! t) {
+      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 {
+        // at this point, only the types U, T should be left
+        System.IO.StringWriter buffer = new System.IO.StringWriter();
+        using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+          t.Emit(stream);
+        }
+        return "boogie" + buffer.ToString();
+      }
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    public static string! MakeIdPrintable(string! s) {
+      // make sure that no keywords are used as identifiers
+      switch(s) {
+      case andName:
+      case orName:
+      case notName:
+      case impliesName:
+      case iffName:
+      case eqName:
+      case distinctName:
+      case TRUEName:
+      case FALSEName:
+      case "Array":
+        s = "nonkeyword_" + s;
+        break;
+      }
+
+      string! newS = "";
+      foreach (char ch in s) {
+        if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_')
+          newS = newS + ch;
+        else
+          // replace everything else with a .
+          newS = newS + '.';
+      }
+
+      // ensure that the first character is not . or _ (some SMT-solvers do
+      // not like that, e.g., yices and cvc3)
+      if (newS[0] == '.' || newS[0] == '_')
+        newS = "x" + newS;
+
+      return newS;
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    /// <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! 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! 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) {
+      if (!options.AsTerm)
+        System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
+    }
+
+    internal void AssertAsFormula(string! x, LineariserOptions! options) {
+      if (options.AsTerm)
+        System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    public bool Visit(VCExprLiteral! node, LineariserOptions! options) {
+      if (options.AsTerm) {
+
+        if (node == VCExpressionGenerator.True)
+          wr.Write("{0}", boolTrueName);
+        else if (node == VCExpressionGenerator.False)
+          wr.Write("{0}", boolFalseName);
+        else if (node is VCExprIntLit) {
+          // some SMT-solvers do not understand negative literals
+          // (e.g., yices)
+          BigNum lit = ((VCExprIntLit)node).Val;
+          if (lit.IsNegative)
+            wr.Write("({0} 0 {1})", intSubName, lit.Abs);
+          else
+            wr.Write(lit);
+        } else
+          assert false;
+
+      } else {
+
+        if (node == VCExpressionGenerator.True)
+          wr.Write("{0}", TRUEName);
+        else if (node == VCExpressionGenerator.False)
+          wr.Write("{0}", FALSEName);
+        else if (node is VCExprIntLit) {
+          System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
+        } else
+          assert false;
+
+      }
+
+      return true;
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    public bool Visit(VCExprNAry! node, LineariserOptions! options) {
+      VCExprOp! op = node.Op;
+
+      if (!options.AsTerm &&
+          (op.Equals(VCExpressionGenerator.AndOp) ||
+           op.Equals(VCExpressionGenerator.OrOp))) {
+        // handle these operators without recursion
+
+        wr.Write("({0}",
+                 op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
+        IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+        while (enumerator.MoveNext()) {
+          VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+          if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+            wr.Write(" ");
+            Linearise((VCExpr!)enumerator.Current, options);
+          }
+        }
+
+        wr.Write(")");
+
+        return true;
+      }
+
+      return node.Accept<bool, LineariserOptions!>(OpLineariser, options);
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    public bool Visit(VCExprVar! node, LineariserOptions! options) {
+      string! printedName = Namer.GetName(node, MakeIdPrintable(node.Name));
+
+      if (options.AsTerm ||
+          // formula variables are easy to identify in SMT-Lib
+          printedName[0] == '$')
+        wr.Write("{0}", printedName);
+      else
+        wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName);
+
+      return true;
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    public bool Visit(VCExprQuantifier! node, LineariserOptions! options) {
+      AssertAsFormula(node.Quan.ToString(), options);
+      assert node.TypeParameters.Count == 0;
+
+      Namer.PushScope(); try {
+
+      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];
+          // ensure that the variable name starts with ?
+          string! printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));
+          assert printedName[0] == '?';
+          wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));
+        }
+        
+      /*      if (options.QuantifierIds) {
+        // only needed for Z3
+        VCQuantifierInfos! infos = node.Infos;
+        if (infos.qid != null) {
+          wr.Write("(QID ");
+          wr.Write(infos.qid);
+          wr.Write(") ");
+        }
+        if (0 <= infos.uniqueId) {
+          wr.Write("(SKOLEMID ");
+          wr.Write(infos.uniqueId);
+          wr.Write(") ");
+        }
+        } */
+
+      Linearise(node.Body, options);
+
+      WriteTriggers(node.Triggers, options);        
+      wr.Write(")");
+
+      return true;
+
+      } finally {
+        Namer.PopScope();
+      }
+    }
+
+    private void WriteTriggers(List<VCTrigger!>! triggers, LineariserOptions! options) {
+      // first, count how many neg/pos triggers there are
+      int negTriggers = 0;
+      int posTriggers = 0;
+      foreach (VCTrigger! vcTrig in triggers) {
+        if (vcTrig.Pos) {
+          posTriggers++;
+        } else {
+          negTriggers++;
+        }
+      }
+
+      if (posTriggers > 0) {
+        foreach (VCTrigger! vcTrig in triggers) {
+          if (vcTrig.Pos) {
+            wr.Write(" :pat {");
+            foreach (VCExpr! e in vcTrig.Exprs) {
+              wr.Write(" ");
+              LineariseAsTerm(e, options);
+            }
+            wr.Write(" } ");
+          }
+        }
+      } else if (negTriggers > 0) {
+        // 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) {
+          if (!vcTrig.Pos) {
+            wr.Write(" :nopat { ");
+            assert vcTrig.Exprs.Count == 1;
+            wr.Write(" ");
+            LineariseAsTerm(vcTrig.Exprs[0], options);
+            wr.Write(" } ");
+          }
+        }
+      }
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    public bool Visit(VCExprLet! node, LineariserOptions! options) {
+      Namer.PushScope(); try {
+
+      foreach (VCExprLetBinding! b in node) {
+        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] == '$';
+        
+        wr.Write("{0} ", printedName);
+        Linearise(b.E, options.SetAsTerm(!formula));
+        wr.Write(") ");
+      }
+      Linearise(node.Body, options);
+
+      for (int i = 0; i < node.Length; ++i)
+        wr.Write(")");
+
+      return true;
+
+      } finally {
+        Namer.PopScope();
+      }
+    }
+
+    /////////////////////////////////////////////////////////////////////////////////////
+
+    // 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;
+
+      public SMTLibOpLineariser(SMTLibExprLineariser! ExprLineariser, TextWriter! wr) {
+        this.ExprLineariser = ExprLineariser;
+        this.wr = wr;
+      }
+
+      ///////////////////////////////////////////////////////////////////////////////////
+
+      private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+                                    LineariserOptions! options,
+                                    bool argsAsTerms) {
+        WriteApplication(op, op, args, options, argsAsTerms);
+      }
+
+      private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+                                    LineariserOptions! options) {
+        WriteApplication(op, op, args, options, options.AsTerm);
+      }
+
+      private void WriteTermApplication(string! op, IEnumerable<VCExpr!>! args,
+                                        LineariserOptions! options) {
+        ExprLineariser.AssertAsTerm(op, options);
+        WriteApplication(op, op, args, options, options.AsTerm);
+      }
+
+      private void WriteApplication(string! termOp, string! predOp,
+                                    IEnumerable<VCExpr!>! args, LineariserOptions! options) {
+        WriteApplication(termOp, predOp, args, options, options.AsTerm);
+      }
+
+      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);
+
+        bool hasArgs = false;
+        foreach (VCExpr! e in args) {
+          if (!hasArgs)
+            wr.Write("({0}", opName);
+          wr.Write(" ");
+          ExprLineariser.Linearise(e, newOptions);
+          hasArgs = true;
+        }
+        
+        if (hasArgs)
+          wr.Write(")");
+        else
+          wr.Write("{0}", opName);
+      }
+
+      // 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) {
+        if (!options.AsTerm)
+          // Write: (EQ (f args) |@true|)
+          // where "args" are written as terms
+          wr.Write("({0} ", eqName);
+
+        WriteApplication(termOp, args, options, true);
+
+        if (!options.AsTerm)
+          wr.Write(" {0})", boolTrueName);
+      }
+
+      ///////////////////////////////////////////////////////////////////////////////////
+      
+      public bool VisitNotOp      (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(boolNotName, notName, node, options);      // arguments can be both terms and formulas
+        return true;
+      }
+
+      private bool PrintEq(VCExprNAry! node, LineariserOptions! options) {
+        if (options.AsTerm) {
+          // use equality on terms, also if the arguments have type bool
+          assert node[0].Type.Equals(node[1].Type);
+          if (node[0].Type.IsBool) {
+            WriteApplication(boolIffName, node, options);
+          } else if (node[0].Type.IsInt) {
+            WriteApplication(termIntEqual, node, options);
+          } else {
+            // TODO: make this less hackish
+            CtorType t = node[0].Type as CtorType;
+            if (t != null && t.Decl.Name.Equals("U")) {
+              WriteApplication(termUEqual, node, options);
+            } else if (t != null && t.Decl.Name.Equals("T")) {
+              WriteApplication(termTEqual, node, options);
+            } else {
+              assert false;   // unknown type
+            }
+          }
+        } else {
+          if (node[0].Type.IsBool) {
+            assert node[1].Type.IsBool;
+            // use equivalence
+            WriteApplication(iffName, node, options);
+          } else {
+            // use equality and write the arguments as terms
+            WriteApplication(eqName, node, options, true);
+          }
+        }
+
+        return true;        
+      }
+
+      public bool VisitEqOp       (VCExprNAry! node, LineariserOptions! options) {
+        return PrintEq(node, options);
+      }
+
+      public bool VisitNeqOp      (VCExprNAry! node, LineariserOptions! options) {
+        wr.Write("({0} ", options.AsTerm ? boolNotName : notName);
+        PrintEq(node, options);
+        wr.Write(")");
+        return true;
+      }
+
+      public bool VisitAndOp      (VCExprNAry! node, LineariserOptions! options) {
+        assert options.AsTerm;
+        WriteApplication(boolAndName, andName, node, options);
+        return true;
+      }
+
+      public bool VisitOrOp       (VCExprNAry! node, LineariserOptions! options) {
+        assert options.AsTerm;
+        WriteApplication(boolOrName, orName, node, options);
+        return true;
+      }
+
+      public bool VisitImpliesOp  (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(boolImpliesName, impliesName, node, options);
+        return true;
+      }
+
+      public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {
+        ExprLineariser.AssertAsFormula(distinctName, options);
+        
+        if (node.Length < 2) {
+          ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+        } else {
+          wr.Write("({0}", distinctName);
+          foreach (VCExpr! e in node) {
+            wr.Write(" ");
+            ExprLineariser.LineariseAsTerm(e, options);
+          }
+          wr.Write(")");
+        }
+
+        return true;
+      }
+
+      public bool VisitLabelOp    (VCExprNAry! node, LineariserOptions! options) {
+        // VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+        // TODO
+        //        wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
+        ExprLineariser.Linearise(node[0], options);
+        //        wr.Write(")");
+        return true;
+      }
+
+      public bool VisitSelectOp   (VCExprNAry! node, LineariserOptions! options) {
+        assert false;      // should not occur in the output
+      }
+
+      public bool VisitStoreOp    (VCExprNAry! node, LineariserOptions! options) {
+        assert false;       // should not occur in the output
+      }
+
+      public bool VisitBvOp       (VCExprNAry! node, LineariserOptions! options) {
+        assert false;       // TODO
+      }
+
+      public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) {
+        assert false;       // TODO
+      }
+
+      public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) {
+        assert false;       // TODO
+      }
+
+      public bool VisitAddOp            (VCExprNAry! node, LineariserOptions! options) {
+        WriteTermApplication(intAddName, node, options);
+        return true;
+      }
+
+      public bool VisitSubOp            (VCExprNAry! node, LineariserOptions! options) {
+        WriteTermApplication(intSubName, node, options);
+        return true;
+      }
+
+      public bool VisitMulOp            (VCExprNAry! node, LineariserOptions! options) {
+        WriteTermApplication(intMulName, node, options);
+        return true;
+      }
+
+      public bool VisitDivOp            (VCExprNAry! node, LineariserOptions! options) {
+        WriteTermApplication(intDivName, node, options);
+        return true;
+      }
+
+      public bool VisitModOp            (VCExprNAry! node, LineariserOptions! options) {
+        WriteTermApplication(intModName, node, options);
+        return true;
+      }
+
+      public bool VisitLtOp             (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(termLessName, lessName, node, options, true);  // arguments are always terms
+        return true;
+      }
+
+      public bool VisitLeOp             (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(termAtmostName, atmostName, node, options, true);  // arguments are always terms
+        return true;
+      }
+
+      public bool VisitGtOp             (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(termGreaterName, greaterName, node, options, true);  // arguments are always terms
+        return true;
+      }
+
+      public bool VisitGeOp             (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(termAtleastName, atleastName, node, options, true);  // arguments are always terms
+        return true;
+      }
+
+      public bool VisitSubtypeOp        (VCExprNAry! node, LineariserOptions! options) {
+        WriteApplication(subtypeName, node, options, true);               // arguments are always terms
+        return true;
+      }
+
+      public bool VisitSubtype3Op        (VCExprNAry! node, LineariserOptions! options) {
+        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));
+
+        // arguments are always terms
+        WriteApplicationTermOnly(printedName, node, options);
+        return true;
+      }
+      
+    }
+  }
+
+}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.ssc b/Source/Provers/SMTLib/TypeDeclCollector.ssc
new file mode 100644
index 00000000..08c0e6a3
--- /dev/null
+++ b/Source/Provers/SMTLib/TypeDeclCollector.ssc
@@ -0,0 +1,107 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.SMTLib
+{
+  // Visitor for collecting the occurring function symbols in a VCExpr,
+  // and for creating the corresponding declarations
+
+  public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+
+    private readonly UniqueNamer! Namer;
+
+    public TypeDeclCollector(UniqueNamer! namer) {
+      this.Namer = namer;
+    }
+
+    // not used
+    protected override bool StandardResult(VCExpr! node, bool arg) {
+      return true;
+    }
+
+    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> ();
+
+    public List<string!>! AllDeclarations { get {
+      List<string!>! res = new List<string!> ();
+      res.AddRange(AllDecls);
+      return res;
+    } }
+
+    public List<string!>! GetNewDeclarations() {
+      List<string!>! res = new List<string!> ();
+      res.AddRange(IncDecls);
+      IncDecls.Clear();
+      return res;
+    }
+
+    private void AddDeclaration(string! decl) {
+      AllDecls.Add(decl);
+      IncDecls.Add(decl);
+    }
+
+    public void Collect(VCExpr! expr) {
+      Traverse(expr, true);
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+
+    private static string! TypeToString(Type! t) {
+      return SMTLibExprLineariser.TypeToString(t);
+    }
+
+    public override bool Visit(VCExprNAry! node, bool arg) {
+      // 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) {
+          decl += " " + TypeToString(v.TypedIdent.Type);
+        }
+        assert f.OutParams.Length == 1;
+        foreach (Variable! v in f.OutParams) {
+          decl += " " + TypeToString(v.TypedIdent.Type);
+        }
+
+        decl += "))";
+        
+        AddDeclaration(decl);
+        KnownFunctions.Add(f, true);
+      }
+
+      return base.Visit(node, arg);
+    }
+
+    public override bool Visit(VCExprVar! node, bool arg) {
+      if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
+        string! printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name));
+        string! decl =
+          ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";
+        AddDeclaration(decl);
+        KnownVariables.Add(node, true);
+      }
+
+      return base.Visit(node, arg);
+    }
+  }
+
+}
+\ No newline at end of file
diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.ssc b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc
new file mode 100644
index 00000000..8443d950
--- /dev/null
+++ b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc
@@ -0,0 +1,183 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Simplify
+{
+  // Simplify does not understand the LET operator, so we have to replace
+  // it with implications (previously, this was done in the VCExprGenerator), or
+  // we have to apply the let as a substitution (in the case of terms)
+
+  // This visitor expects that let-bindings are sorted, so that bound
+  // variables only occur after their declaration
+
+  public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
+
+    public Let2ImpliesMutator(VCExpressionGenerator! gen) {
+      base(gen);
+    }
+
+    public VCExpr! Mutate(VCExpr! expr) {
+      return Mutate(expr, new VCExprSubstitution ());
+    }
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    private int polarity = 1;  // 1 for positive, -1 for negative, 0 for both
+
+    // we also track which variables occur in positive, negative, or
+    // in both positions (to decide whether implications or equations
+    // have to be used to define such a variable)
+    private enum OccurrenceTypes { None, Pos, Neg, PosNeg };
+    private OccurrenceTypes Union(OccurrenceTypes o1, OccurrenceTypes o2) {
+      switch(o1) {
+      case OccurrenceTypes.None: return o2;
+      case OccurrenceTypes.Pos:
+        switch(o2) {
+        case OccurrenceTypes.None:
+        case OccurrenceTypes.Pos:
+          return OccurrenceTypes.Pos;
+        default:
+          return OccurrenceTypes.PosNeg;
+        }
+      case OccurrenceTypes.Neg:
+        switch(o2) {
+        case OccurrenceTypes.None:
+        case OccurrenceTypes.Neg:
+          return OccurrenceTypes.Neg;
+        default:
+          return OccurrenceTypes.PosNeg;
+        }
+      default:
+        return OccurrenceTypes.PosNeg;
+      }
+    }
+
+    private IDictionary<VCExprVar!, OccurrenceTypes>! VarOccurrences =
+      new Dictionary<VCExprVar!, OccurrenceTypes>();
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    public override VCExpr! Visit(VCExprVar! node,
+                                  VCExprSubstitution! substitution) {
+      VCExpr! res = base.Visit(node, substitution);
+
+      VCExprVar resAsVar = res as VCExprVar;
+      if (resAsVar != null) {
+        OccurrenceTypes occ;
+        if (polarity > 0)
+          occ = OccurrenceTypes.Pos;
+        else if (polarity < 0)
+          occ = OccurrenceTypes.Neg;
+        else
+          occ = OccurrenceTypes.PosNeg;
+
+        OccurrenceTypes oldOcc;
+        if (VarOccurrences.TryGetValue(resAsVar, out oldOcc))
+          occ = Union(occ, oldOcc);
+        VarOccurrences[resAsVar] = occ;
+      }
+
+      return res;
+    }
+
+    public override VCExpr! Visit(VCExprNAry! node,
+                                  VCExprSubstitution! substitution) {
+      // track the polarity to ensure that no implications are introduced
+      // in negative positions
+      // UGLY: the code for tracking polarities should be factored out
+      // (similar code is used in the TypeEraser)
+
+      VCExpr! res;
+      if (node.Op.Equals(VCExpressionGenerator.NotOp)) {
+        polarity = -polarity;
+        res = base.Visit(node, substitution);
+        polarity = -polarity;
+      } else if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
+        polarity = -polarity;
+        VCExpr! newArg0 = Mutate(node[0], substitution);
+        polarity = -polarity;
+        VCExpr! newArg1 = Mutate(node[1], substitution);
+
+        res = Gen.Implies(newArg0, newArg1);
+      } else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
+                 !node.Op.Equals(VCExpressionGenerator.OrOp) &&
+                 !(node.Op is VCExprLabelOp)) {
+        // standard is to set the polarity to 0 (fits most operators)
+        int oldPolarity = polarity;
+        polarity = 0;
+        res = base.Visit(node, substitution);
+        polarity = oldPolarity;
+      } else {
+        res = base.Visit(node, substitution);
+      }
+
+      return res;
+    }
+
+    public override VCExpr! Visit(VCExprLet! originalNode,
+                                  VCExprSubstitution! substitution) {
+      // first sort the bindings to be able to apply substitutions
+      LetBindingSorter! letSorter = new LetBindingSorter (Gen);
+      VCExpr! newNode = letSorter.Mutate(originalNode, true);
+      VCExprLet node = newNode as VCExprLet;
+
+      if (node == null)
+        // it can happen that the complete let-expressions gets eliminated by the
+        // sorter, which also checks whether let-bindings are actually used
+        return newNode;
+
+      substitution.PushScope(); try {
+
+      // the bindings that remain and that are later handled using an implication
+      List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!> ();
+
+      foreach (VCExprLetBinding! binding in node) {
+        // in all cases we apply the substitution up to this point
+        // to the bound formula
+        VCExpr! newE = Mutate(binding.E, substitution);
+
+        if (binding.V.Type.IsBool) {
+          // a bound formula is handled using an implication; we introduce
+          // a fresh variable to avoid clashes
+          assert polarity > 0;
+
+          VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
+          substitution[binding.V] = newVar;
+
+          bindings.Add(Gen.LetBinding(newVar, newE));
+        } else {
+          // a bound term is substituted
+          substitution[binding.V] = newE;
+        }
+      }
+
+      VCExpr! newBody = Mutate(node.Body, substitution);
+
+      // Depending on the places where the variable occurs, we would
+      // have to introduce implications or equations to define the
+      // bound variables. For the time being, we just assert that all
+      // occurrences are positive
+      foreach (VCExprLetBinding! b in bindings) {
+        OccurrenceTypes occ;
+        if (VarOccurrences.TryGetValue(b.V, out occ))
+          assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;
+      }
+
+      return Gen.Implies(Gen.AsImplications(bindings), newBody);
+
+      } finally {
+        substitution.PopScope();
+      }
+    }
+  }
+
+}
+\ No newline at end of file
diff --git a/Source/Provers/Simplify/Prover.ssc b/Source/Provers/Simplify/Prover.ssc
new file mode 100644
index 00000000..f89d6a42
--- /dev/null
+++ b/Source/Provers/Simplify/Prover.ssc
@@ -0,0 +1,606 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+
+// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
+namespace Microsoft.Boogie.Simplify
+{
+  /// <summary>
+  /// An interface to Simplify theorem prover.
+  /// </summary>
+  public abstract class ProverProcess 
+  {
+    [Rep]
+    protected readonly Process! simplify;
+    
+    [Rep] readonly TextReader! fromSimplify;
+    [Rep] readonly TextWriter! toSimplify;
+    [Rep] readonly TextReader! fromStdError;
+
+    protected bool readTimedOut;
+    
+    int nFormulasChecked = 0;
+    public int NumFormulasChecked {
+      get { return nFormulasChecked; }
+    }
+    
+    // Note: In the Everett build (.NET framework < 2.0), Process.PeakVirtualMemorySize64
+    // is not defined, but rather a version that returns an 'int' rather than a 'long'.
+    public long PeakVirtualMemorySize {
+      [NoDefaultContract]
+      get
+        requires IsPeerConsistent;
+        modifies this.*;
+      {
+        expose (this) {
+          simplify.Refresh();
+#if WHIDBEY
+            return simplify.PeakVirtualMemorySize64;
+#else
+            return simplify.PeakPagedMemorySize64;
+#endif
+        }
+      }
+    }
+    
+    public bool HasExited {
+      get { return simplify.HasExited; }
+    }
+    
+    public ProverProcess(ProcessStartInfo! psi, string! proverPath)
+    { // throws ProverException
+      try 
+      {
+        Process simplify = Process.Start(psi);
+        this.simplify = simplify;
+        fromSimplify = simplify.StandardOutput;
+        toSimplify = simplify.StandardInput;
+        fromStdError = simplify.StandardError;
+      } 
+      catch (System.ComponentModel.Win32Exception e)
+      {
+        throw new ProverException(string.Format("Unable to start the process {0}: {1}", proverPath, e.Message));
+      }
+      // base();
+    }
+
+    public abstract string! OptionComments();
+    [Pure(false)]
+    public virtual IEnumerable<string!>! ParameterSettings { get { yield break; } }
+    
+    public void Close()
+      modifies this.*; 
+    {
+      expose (this) {
+        toSimplify.Flush();
+        if (this.simplify != null) 
+        {
+          if (!simplify.HasExited)
+          {
+            this.Kill();
+          }
+          simplify.Close();
+        }
+      }
+    }
+    
+    [NoDefaultContract]  // this method assumes nothing about the object, other than that it has been constructed (which means simplify!=null)
+    [Verify(false)]  // The call simplify.Kill will require simplify.IsPeerConsistent, but since we don't know the state of "this" and "simplify", we cannot afford the run-time check that an assume statement here would impose
+    public void Kill() {
+      try { 
+        if (CommandLineOptions.Clo.ProverShutdownLimit > 0) { 
+          toSimplify.Close(); 
+          for (int i = 0; !simplify.HasExited && i <= CommandLineOptions.Clo.ProverShutdownLimit * 1000; i += 100)
+          {		
+            System.Threading.Thread.Sleep(100); 
+          } 
+        }
+        if (!simplify.HasExited) { simplify.Kill(); }
+      } catch (InvalidOperationException) { /* already exited */ }
+        catch (System.ComponentModel.Win32Exception) { /* already exiting */ }
+    }
+
+    public static void ReportWarning(string! w)
+      modifies Console.Out.*, Console.Error.*;
+    {
+      switch (CommandLineOptions.Clo.PrintProverWarnings) {
+        case CommandLineOptions.ProverWarnings.None:
+          break;
+        case CommandLineOptions.ProverWarnings.Stdout:
+          Console.WriteLine("Prover warning: " + w);
+          break;
+        case CommandLineOptions.ProverWarnings.Stderr:
+          Console.Error.WriteLine("Prover warning: " + w);
+          break;
+        default:
+          assume false;  // unexpected case
+      }
+    }
+    
+    public virtual void AddAxioms(string! s) 
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+      throws UnexpectedProverOutputException;
+    {
+      expose (this) {
+        toSimplify.Write("(BG_PUSH ");
+        toSimplify.Write(s);
+        toSimplify.WriteLine(")");
+      }
+    }
+
+    public virtual void Feed(string! s, int statementCount) 
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+      throws UnexpectedProverOutputException;
+    {
+      expose (this) {
+        toSimplify.Write(s);
+      }
+    }
+
+    public virtual void PopAxioms() 
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+      throws UnexpectedProverOutputException;
+    {
+      expose (this) {
+        toSimplify.WriteLine("(BG_POP)");
+      }
+    }
+
+    public void ToFlush()
+      modifies this.*;
+    {
+      expose (this) {
+        toSimplify.Flush();
+      }
+    }
+
+    public enum ProverOutcome { Valid, NotValid, TimeOut, OutOfMemory, Inconclusive }
+    
+    /// <summary>
+    /// Passes the formula to Simplify.
+    /// </summary>
+    public void BeginCheck(string! descriptiveName, string! formula)
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+    {
+      DoBeginCheck(descriptiveName, formula);
+      nFormulasChecked++;
+    }
+    
+    /// <summary>
+    /// Reports the outcome of formula checking.  If the outcome is Invalid,
+    /// then the "handler" is invoked with each counterexample.
+    /// </summary>
+    public abstract ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
+      modifies this.**;
+      modifies Console.Out.*, Console.Error.*;
+      modifies handler.*;
+      throws UnexpectedProverOutputException;
+    
+    protected abstract void DoBeginCheck(string! descriptiveName, string! formula)
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+
+    /// <summary>
+    /// Returns an array of the labels in "labels", with "|" brackets (if any)
+    /// stripped off.
+    /// Assumes that every label begins with "|+" or "|@", or just "+" or "@",
+    /// and ends with "|" if it started with one, and that these "|" brackets are
+    /// the only "|"s in "labels".
+    /// </summary>
+    protected static List<string!>! ParseLabels(string! labels) 
+    {
+      List<string!> list = new List<string!>();
+      int j = 0;
+      while (true)
+        // invariant: j is the number of characters of "labels" consumed so far
+        // invariant: an even number of '|' characters remain in "labels"
+        invariant 0 <= j && j <= labels.Length;
+      {
+        j = labels.IndexOfAny(new char[]{'|', '+', '@'}, j);
+        if (j < 0) {
+          // no more labels
+          return list;
+        }
+        char ch = labels[j];
+        if (ch == '|') {
+          j++;  // skip the '|'
+          assume j < labels.Length;  // there should now be a '+' or '@'
+          ch = labels[j];
+        }
+        assume ch == '+' || ch == '@';
+        j++;  // skip the '+' or '@'
+        int k = labels.IndexOfAny(new char[]{'|', ' ', ')'}, j);
+        assume j+2 <= k;
+        string s = labels.Substring(j, k-j);
+        list.Add(s);
+        j = k+1;
+      }
+    }
+
+    [Rep] char[] expectBuffer = null;
+
+    /// <summary>
+    /// Expects s[0]==ch and the next s.Length-1 characters of the input to be s[1,..]
+    /// If not, more characters may be read from "fromSimplify" to provide additional context
+    /// for the UnexpectedProverOutputException exception that will be thrown.
+    /// </summary>
+    protected void Expect(int ch, string! s) 
+      requires 1 <= s.Length;
+      modifies this.*;
+      throws UnexpectedProverOutputException;
+    { 
+      if (ch == -1) {
+        // a return of -1 from FromReadChar means that there is no StdOutput
+        // to treat this we can return the error message we get from Z3 on StdError and then
+        // declare this case to be inconclusive 
+        string str = FromStdErrorAll();
+        if (str == "") {
+          throw new ProverDiedException();
+        } else {
+          throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + str + "<<<end>>>");
+        }
+      }
+        
+      string badInputPrefix;
+      if (ch != s[0]) 
+      {
+        badInputPrefix = Char.ToString((char)ch);
+      } 
+      else 
+      {
+        int len = s.Length - 1;
+        if (expectBuffer == null || expectBuffer.Length < len) 
+        {
+          expose (this) {
+            expectBuffer = new char[len];
+          }
+        }
+        try 
+        {
+          string s0;
+          expose (this) {
+            fromSimplify.ReadBlock(expectBuffer, 0, len);
+            s0 = new string(expectBuffer, 0, len);
+          }
+          string s1 = s.Substring(1, len);
+          if (s0.CompareTo(s1) == 0) 
+          {
+            badInputPrefix = null;  // no error
+          } 
+          else 
+          {
+            badInputPrefix = (char)ch + s0;
+          }
+        } 
+        catch (IOException) 
+        {
+          throw new UnexpectedProverOutputException("Expected \"" + s + "\", encountered IO exception.");
+        }
+      }
+
+      if (badInputPrefix != null) 
+      {
+        // Read the rest of the available input, without blocking!
+        // Despite the confusing documentation for the Read method, it seems
+        // that Read does block.  It if didn't, I would have written:
+        //    string remaining = "";
+        //    char[] buf = new char[1024];
+        //    while (true) {
+        //        int len = fromSimplify.Read(buf, 0, buf.Length);
+        //        remaining += new String(buf, 0, len);
+        //        if (len != buf.Length) {
+        //            break;
+        //        }
+        //    }
+        // But instead, I'll just hope that one line of input is available and read
+        // it.
+        string remaining = fromSimplify.ReadLine() + "\r\n";
+        throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + badInputPrefix + remaining + "<<<end>>>");
+      }
+    }
+    
+    protected int FromReadChar()
+      modifies this.*;
+    {
+      expose (this) {
+        return fromSimplify.Read();
+      }
+    }
+
+    private void KillProver(object state)
+    {
+      expose (this) {
+        this.readTimedOut = true;
+        simplify.Kill();
+      }
+    }
+    
+    protected int FromReadChar(int timeout)
+      requires -1 <= timeout;
+      modifies this.*;
+    {
+      expose (this) {
+        this.readTimedOut = false;
+        System.Threading.Timer t = new System.Threading.Timer(this.KillProver, null, timeout, System.Threading.Timeout.Infinite);
+        int ch = fromSimplify.Read();
+        t.Change(System.Threading.Timeout.Infinite, System.Threading.Timeout.Infinite);
+        t.Dispose();
+        return ch;
+      }
+    }
+    
+    protected string! FromReadLine()
+      modifies this.*;
+    {
+      expose (this) {
+        string s = fromSimplify.ReadLine();
+        if (s == null) {
+          // this is what ReadLine returns if all characters have been read
+          s = "";
+        }
+        return s;
+      }
+    }
+    
+    protected string! FromStdErrorAll ()
+      modifies this.*;
+    {
+      expose (this) {
+        if (fromStdError != null) {
+          string s = fromStdError.ReadToEnd();
+          if (s == null) {
+            // this is what ReadLine returns if all characters have been read
+            s = "";
+          }
+          return s;
+        }
+        // there is no StdErrorReader available
+        else {
+          return "";
+        }
+      }
+    }
+    
+    protected void ToWriteLine(string! s)
+      modifies this.*;
+    {
+      expose (this) {
+        toSimplify.WriteLine(s);
+      }
+    }
+  }
+ 
+  // derived by Z3ProverProcess
+  public class SimplifyProverProcess : ProverProcess {
+    public SimplifyProverProcess(string! proverPath, bool dummy)
+    { // throws ProverException
+      ProcessStartInfo psi = new ProcessStartInfo(proverPath, "-labelsonly");
+      psi.CreateNoWindow = true;
+      psi.UseShellExecute = false;
+      psi.RedirectStandardInput = true;
+      psi.RedirectStandardOutput = true;
+      psi.RedirectStandardError = true;
+      assume psi.EnvironmentVariables != null;  // by inspecting the code through Reflector; the documentation says this property is "null by default", whatever that means  --KRML
+      if (0 <= CommandLineOptions.Clo.ProverKillTime) {
+        psi.EnvironmentVariables["PROVER_KILL_TIME"] = CommandLineOptions.Clo.ProverKillTime.ToString();
+      }
+      if (0 <= CommandLineOptions.Clo.SimplifyProverMatchDepth) {
+        psi.EnvironmentVariables["PROVER_MATCH_DEPTH"] = CommandLineOptions.Clo.SimplifyProverMatchDepth.ToString();
+      }
+      if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+        psi.EnvironmentVariables["PROVER_CC_LIMIT"] = CommandLineOptions.Clo.ProverCCLimit.ToString();
+      }
+      
+      base(psi, proverPath);
+    }
+
+    public override string! OptionComments()
+    {
+      // would we want the timeout stuff here?
+      return "";
+    }
+
+    [NotDelayed]
+    // TODO it complains about things not beeing peer consistent upon call to EatPrompt()
+    // not sure what is it about... --micmo
+    [Verify(false)] 
+    public SimplifyProverProcess(string! proverPath)
+      modifies Console.Out.*, Console.Error.*;
+      throws UnexpectedProverOutputException;
+    {
+      this(proverPath, true);
+      EatPrompt();
+    }
+
+    private void EatPrompt() 
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+      throws UnexpectedProverOutputException;
+    {
+      // skips text matching the regular expression: (white space)* ">\t"
+      ToFlush();
+
+      int ch = 0;
+      do {
+        ch = FromReadChar();
+      } while (Char.IsWhiteSpace((char)ch));
+      
+      while (ch == 'W') {
+        ch = ConsumeWarnings(ch);
+      }
+      
+      Expect(ch, ">\t");
+    }
+    
+    public override void AddAxioms(string! s) 
+      throws UnexpectedProverOutputException;
+    {
+      //ToWriteLine("(PROMPT_OFF)");
+      base.AddAxioms(s);
+      //ToWriteLine("(PROMPT_ON)");
+      EatPrompt();
+    }
+    
+    public override void Feed(string! s, int statementCount) 
+      throws UnexpectedProverOutputException;
+    {
+      //ToWriteLine("(PROMPT_OFF)");
+      base.Feed(s, statementCount);
+      //ToWriteLine("(PROMPT_ON)");
+      for (int i = 0; i < statementCount; i++) {
+        EatPrompt();
+      }
+    }
+    
+    public override void PopAxioms() 
+      throws UnexpectedProverOutputException;
+    {
+      base.PopAxioms();
+      EatPrompt();
+    }
+
+    protected override void DoBeginCheck(string! descriptiveName, string! formula)
+    {
+      //simplify.Refresh();
+      //this.Comment("@@@@ Virtual Memory:  " + simplify.PeakVirtualMemorySize64);
+      //this.Comment("@@@@ Working Set:  " + simplify.PeakWorkingSet64);
+      //this.Comment("@@@@ Paged Memory:  " + simplify.PeakPagedMemorySize64);
+    
+      ToWriteLine(formula);
+      ToFlush();
+    }
+
+    public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
+      throws UnexpectedProverOutputException;
+    {
+      ProverOutcome outcome;
+
+      if (this.simplify == null) {
+        return ProverOutcome.Inconclusive;
+      }
+      
+      int ch = FromReadChar();
+      while (ch == 'W') 
+      {
+        ch = ConsumeWarnings(ch);
+      }
+      if (ch == 'E')
+      {
+        Expect(ch, "Exceeded PROVER_KILL_TIME -- discontinuing search for counterexamples.");
+        FromReadLine();
+        ch = FromReadChar();
+        if (ch == '\n')
+        {
+          ch = FromReadChar();
+        }
+        Expect(ch, "  labels:");
+        FromReadLine();
+        ch = FromReadChar();
+        ch = FromReadChar();
+        ch = FromReadChar();
+        FromReadLine();
+        ch = FromReadChar();
+        ch = FromReadChar();
+        ch = FromReadChar();
+        return ProverOutcome.TimeOut;
+      }
+      if ('0' <= ch && ch <= '9') 
+      {
+        // Valid!
+        do {
+          ch = FromReadChar();
+        } while ('0' <= ch && ch <= '9');
+        Expect(ch, ": Valid.");
+        outcome = ProverOutcome.Valid;
+        ToWriteLine(String.Format(";   FORMULA {0} IS VALID!", NumFormulasChecked + 1 /*Simplify starts at 1*/));
+      } 
+      else 
+      {
+        // now we expect one or more counterexample contexts, each proving a list of labels
+        do {
+          List<string!> labels = ReadLabels(ch);
+          handler.OnModel(labels, null);
+          ch = FromReadChar();
+        } while (ch == 'C');
+        // now we expect "<N>: Invalid" where <N> is some number
+        while ('0' <= ch && ch <= '9') 
+        {
+          ch = FromReadChar();
+        }
+        Expect(ch, ": Invalid.");
+        outcome = ProverOutcome.NotValid;
+        ToWriteLine(String.Format(";   FORMULA {0} IS INVALID", NumFormulasChecked + 1 /*Simplify starts at 1*/));
+      }
+
+      EatPrompt();
+      return outcome;
+    }
+
+    List<string!>! ReadLabels(int ch) 
+      modifies this.*;
+      throws UnexpectedProverOutputException;
+    {
+      Expect(ch, "Counterexample:\n");  // FIX! ?  Is there a problem with \r\n here?
+      ch = FromReadChar();
+      List<string!> theLabels;
+      if (ch == ' ') 
+      {
+        // there are labels
+        Expect(ch, "  labels: ");
+        string labels = FromReadLine();  // reads "(A B C ...)\n"
+        theLabels = ParseLabels(labels);
+        ch = FromReadChar();
+      }
+      else
+      {
+        theLabels = new List<string!>();
+      }
+      Expect(ch, "\n");  // empty line
+
+      return theLabels;
+    }
+    
+    int ConsumeWarnings(int ch)
+      requires ch == 'W';
+      modifies this.*;
+      modifies Console.Out.*, Console.Error.*;
+      throws UnexpectedProverOutputException;
+    {
+      Expect(ch, "Warning: ");
+      string w = FromReadLine();
+      if (w.StartsWith("triggerless quantifier body")) {
+        FromReadLine();  // blank line
+        w = "triggerless quantifier body: " + FromReadLine();  // expression (body)
+        FromReadLine();  // blank line
+        FromReadLine();  // "with X pattern variable(s)...
+        FromReadLine();  // blank line
+        FromReadLine();  // expression (entire quantifier)
+      }
+      ReportWarning(w);
+      ch = FromReadChar();
+      if (ch == '\n') 
+      {
+        // make up for a poorly designed ReadLine routine (only the first
+        // character of the DOS end-of-line sequence "\r\n" is read)
+        ch = FromReadChar();
+      }
+      return ch;
+    }
+  }
+  
+}
+
diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc
new file mode 100644
index 00000000..df7f86d6
--- /dev/null
+++ b/Source/Provers/Simplify/ProverInterface.ssc
@@ -0,0 +1,633 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.TypeErasure;
+
+namespace Microsoft.Boogie.Simplify
+{
+  public abstract class LogProverInterface : ProverInterface
+  {
+    [NotDelayed]
+    protected LogProverInterface(ProverOptions! options,
+        string! openComment, string! closeComment,
+        string! openActivity, string! closeActivity,
+        VCExpressionGenerator! gen)
+      ensures this.gen == gen;
+    {
+      if (options.SeparateLogFiles) {
+        this.commonPrefix = new List<string!> ();
+      } else {
+        this.logFileWriter = options.OpenLog(null);
+      }
+      this.openCommentString = openComment;
+      this.closeCommentString = closeComment;
+      this.openActivityString = openActivity;
+      this.closeActivityString = closeActivity;
+      this.gen = gen;
+      this.options = options;
+      base();
+
+      if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {
+        // Emit version comment in the log
+        LogCommonComment(CommandLineOptions.Clo.Version);
+        LogCommonComment(CommandLineOptions.Clo.Environment);
+      }
+    }
+    
+    [StrictReadonly][Additive]
+    protected readonly VCExpressionGenerator! gen;
+
+    private TextWriter/*?*/ logFileWriter;
+    [Microsoft.Contracts.StrictReadonly]
+    private readonly string! openCommentString;
+    [Microsoft.Contracts.StrictReadonly]
+    private readonly string! closeCommentString;
+    [Microsoft.Contracts.StrictReadonly]
+    private readonly string! openActivityString;
+    [Microsoft.Contracts.StrictReadonly]
+    private readonly string! closeActivityString;
+    [Microsoft.Contracts.StrictReadonly]
+    protected readonly ProverOptions! options;
+    [Microsoft.Contracts.StrictReadonly]
+    private readonly List<string!>/*?*/ commonPrefix;
+
+    public void LogActivity(string! s) {
+      LogActivity(s, false);
+    }
+
+    public void LogCommon(string! s) {
+      LogActivity(s, true);
+    }
+
+    private void LogActivity(string! s, bool common) {
+      assume common || !options.SeparateLogFiles || logFileWriter != null;
+      if (logFileWriter != null) {
+        logFileWriter.Write(openActivityString);
+        logFileWriter.Write(s);
+        logFileWriter.WriteLine(closeActivityString);
+        logFileWriter.Flush();
+      }
+      if (common && commonPrefix != null) {
+        commonPrefix.Add(openActivityString + s + closeActivityString);
+      }
+    }
+
+    /// <summary>
+    /// Write "comment" to logfile, if any, formatted as a comment for the theorem prover at hand.
+    /// Assumes that "comment" does not contain any characters that would prematurely terminate
+    /// the comment (like, perhaps, a newline or "*/").
+    /// </summary>    
+    public override void LogComment(string! comment)
+    {
+      LogComment(comment, false);
+    }
+
+    public void LogCommonComment(string! comment)
+    {
+      LogComment(comment, true);
+    }
+
+    private void LogComment(string! comment, bool common)
+    {
+      assume common || !options.SeparateLogFiles || logFileWriter != null;
+      if (logFileWriter != null) {
+        logFileWriter.Write(openCommentString);
+        logFileWriter.Write(comment);
+        logFileWriter.WriteLine(closeCommentString);
+        logFileWriter.Flush();
+      }
+      if (common && commonPrefix != null) {
+        commonPrefix.Add(openCommentString + comment + closeCommentString);
+      }
+    }
+
+    public virtual void NewProblem(string! descName)
+    {
+      if (commonPrefix != null) {
+        if (logFileWriter != null) {
+          logFileWriter.Close();
+        }
+        logFileWriter = options.OpenLog(descName);
+        if (logFileWriter != null) {
+          foreach (string! s in commonPrefix)
+            logFileWriter.WriteLine(s);
+        }
+      }
+      LogComment("Proof obligation: " + descName);
+    }
+
+    public override void Close() {
+      if (logFileWriter != null) {
+        logFileWriter.Close();
+        logFileWriter = null;
+      }
+    }
+
+    public override VCExpressionGenerator! VCExprGen
+    {
+      get { return this.gen; }
+    }
+  }
+  
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+
+  public abstract class ProcessTheoremProver : LogProverInterface
+  {
+    private static string! _proverPath;
+
+    protected AxiomVCExprTranslator! vcExprTranslator { get {
+      return (AxiomVCExprTranslator!)ctx.exprTranslator;
+    } }
+
+    protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator();
+
+    protected void FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {
+      if (thmProver == null)
+        return;
+      foreach (string! s in vcExprTranslator.NewTypeDecls) {
+        LogCommon(s);
+        thmProver.Feed(s, 0);
+      }
+      foreach (string! s in vcExprTranslator.NewAxioms) {
+        LogBgPush(s);
+        thmProver.AddAxioms(s);
+      }
+    }
+
+    protected static string! CodebaseString() {
+      return Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+    }
+
+    private static IDictionary<string!, string!>! BackgroundPredicates =
+      new Dictionary<string!, string!> ();
+
+    protected static string! GetBackgroundPredicate(string! filename) {
+      string res;
+      if (!BackgroundPredicates.TryGetValue(filename, out res)) {
+        // do we have to lock/synchronise anything?
+        string univBackPredPath = Path.Combine(CodebaseString(), filename);
+        using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
+        {
+          res = reader.ReadToEnd();
+        }
+        BackgroundPredicates.Add(filename, res);
+      }
+      return (!)res;
+    }
+
+    static void InitializeGlobalInformation(string! proverExe)
+      ensures _proverPath != null;
+      //throws ProverException, System.IO.FileNotFoundException;
+    {
+      if (_proverPath == null) {
+        // Initialize '_proverPath'
+        _proverPath = Path.Combine(CodebaseString(), proverExe);
+        if (!File.Exists(_proverPath))
+        {
+          _proverPath = Path.Combine(@"c:\Program Files\Microsoft Research\Z3-2.0\bin", proverExe);
+        }
+        if (!File.Exists(_proverPath))
+        {
+          throw new ProverException("Cannot find executable: " + _proverPath);
+        }
+      }
+    }
+
+    [Rep] protected internal ProverProcess thmProver;
+    bool currentProverHasBeenABadBoy = false;
+    // invariant currentProverHasBeenABadBoy ==> thmProver != null;
+    protected int restarts = 0;
+    protected DeclFreeProverContext! ctx;
+    protected string! BackgroundPredFilename;
+    protected ConsoleCancelEventHandler? cancelEvent;
+    
+    [NotDelayed]
+    public ProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx,
+                                string! proverExe, string! backgroundPred)
+      throws UnexpectedProverOutputException;
+    {
+      BackgroundPredFilename = backgroundPred;
+      InitializeGlobalInformation(proverExe);
+      this.ctx = ctx;
+      base(options, "; ", "", "", "", gen);
+      
+      // ensure that a VCExprTranslator is available
+      // if none exists so far, we have to create a new one
+      // from scratch and feed the axioms to it
+      if (ctx.exprTranslator == null) {
+        AxiomVCExprTranslator tl = SpawnVCExprTranslator();
+        ctx.exprTranslator = tl;
+        tl.AddAxiom(tl.translate(ctx.Axioms, -1));
+        // we clear the lists with new axioms and declarations;
+        // they are not needed at this point
+        List<string!> x = tl.NewAxioms;
+        x = x;  // make the compiler happy: somebody uses the value of x
+        x = tl.NewTypeDecls;
+      }
+    }
+
+    /// <summary>
+    /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
+    /// </summary>
+    public override void PushVCExpression(VCExpr! vc) 
+    {
+      vcExprTranslator.AddAxiom( vcExprTranslator.translate(vc,1) ); 
+    }
+
+    [NoDefaultContract]  // important, since we have no idea what state the object might be in when this handler is invoked
+    void ControlCHandler(object o, ConsoleCancelEventArgs a)
+    {
+      if (thmProver != null) {
+        thmProver.Kill();
+      }
+    }
+
+    public override void Close() {
+      if (cancelEvent != null) {
+        Console.CancelKeyPress -= cancelEvent;
+        cancelEvent = null;
+      }
+      if (thmProver != null) {
+        expose (this) {
+          thmProver.Close();
+          thmProver = null;
+          currentProverHasBeenABadBoy = false;
+        }
+      }
+      base.Close();
+    }
+
+    private UnexpectedProverOutputException proverException;
+
+    public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler)
+    {
+      this.NewProblem(descriptiveName);
+      this.proverException = null;
+
+      try {
+        this.ResurrectProver();
+        
+        string vcString = vcExprTranslator.translate(vc, 1);
+
+        Helpers.ExtraTraceInformation("Sending data to theorem prover");
+
+        FeedNewAxiomsDecls2Prover();
+        string! prelude = ctx.GetProverCommands(false);
+        vcString = prelude + vcString;
+        LogActivity(vcString);
+
+        assert thmProver != null;
+        thmProver.BeginCheck(descriptiveName, vcString);
+
+        if (CommandLineOptions.Clo.RestartProverPerVC) {
+          LogComment("Will restart the prover due to /restartProver option");
+          currentProverHasBeenABadBoy = true;
+        }
+      } catch (UnexpectedProverOutputException e) {
+        proverException = e;
+      }
+    }
+
+    public override Outcome CheckOutcome(ErrorHandler! handler)
+      throws UnexpectedProverOutputException;
+    {
+      if (this.thmProver == null) {
+        return Outcome.Undetermined;
+      }
+
+      if (proverException == null) {
+        try {
+          ProverProcess.ProverOutcome result = thmProver.CheckOutcome(handler);
+
+          if (options.ForceLogStatus) {
+            switch (result) {
+            case ProverProcess.ProverOutcome.Valid:
+              LogActivity("DBG_WAS_VALID");
+              break;
+            case ProverProcess.ProverOutcome.NotValid:
+              LogActivity("DBG_WAS_INVALID");
+              break;
+            }
+          }
+
+          switch (result) {
+          case ProverProcess.ProverOutcome.Valid:
+            return Outcome.Valid;
+          case ProverProcess.ProverOutcome.TimeOut:
+            return Outcome.TimeOut;
+          case ProverProcess.ProverOutcome.OutOfMemory:
+            return Outcome.OutOfMemory;
+          case ProverProcess.ProverOutcome.Inconclusive:
+            return Outcome.Undetermined;
+          case ProverProcess.ProverOutcome.NotValid:
+            return Outcome.Invalid;
+          }
+        } catch (UnexpectedProverOutputException e) {
+          proverException = e;
+        }
+      }
+
+      assume proverException != null;
+      LogComment("***** Unexpected prover output");
+      expose (this) {
+        currentProverHasBeenABadBoy = true;  // this will cause the next resurrect to restart the prover
+      }
+      throw proverException;
+    }
+
+    protected virtual void ResurrectProver()
+      throws UnexpectedProverOutputException;
+    {
+      expose (this) {
+        if (thmProver != null) {
+          if (thmProver.HasExited) {
+            DateTime now = DateTime.Now;
+            LogComment("***** Prover Crashed at or before " + now.ToString("G"));
+            
+          } else if (CommandLineOptions.Clo.MaxProverMemory > 0 &&
+              thmProver.NumFormulasChecked > CommandLineOptions.Clo.MinNumOfProverCalls &&
+              thmProver.PeakVirtualMemorySize > CommandLineOptions.Clo.MaxProverMemory)
+          {
+            LogComment("***** Exceeded memory limit.  Peak memory usage so far: " +
+                thmProver.PeakVirtualMemorySize / CommandLineOptions.Megabyte + "MB");
+                
+          } else if (!currentProverHasBeenABadBoy) {
+            // prover is ready to go
+            return;
+          }
+          
+          thmProver.Close();
+          thmProver = null;
+          currentProverHasBeenABadBoy = false;
+          restarts++;
+        }
+        FireUpNewProver();
+      }
+    }
+    
+    protected abstract ProverProcess! CreateProverProcess(string! proverPath);
+    
+    public void LogBgPush(string! s) {
+      LogCommon("(BG_PUSH ");
+      LogCommon(s);
+      LogCommon(")");
+    }
+
+    [NoDefaultContract]
+    private void FireUpNewProver()
+      requires IsExposed;
+      requires thmProver == null;
+      throws UnexpectedProverOutputException;
+    {
+      if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
+        cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
+        Console.CancelKeyPress += cancelEvent;
+      }
+      thmProver = CreateProverProcess(_proverPath);
+      if (restarts == 0) {
+        foreach (string! s in thmProver.OptionComments().Split('\n')) {
+          LogCommonComment(s);
+        }
+        foreach (string! parmsetting in thmProver.ParameterSettings) {
+          LogCommon(parmsetting);
+        }
+      }
+      foreach (string! parmsetting in thmProver.ParameterSettings) {
+        thmProver.Feed(parmsetting, 0);
+      }
+      thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);
+      string! incProverCommands = ctx.GetProverCommands(false);
+      string! proverCommands = ctx.GetProverCommands(true);
+      string! prelude = ctx.GetProverCommands(false);
+
+      if (restarts == 0) {
+        // log the stuff before feeding it into the prover, so when it dies
+        // and takes Boogie with it, we know what happened
+        LogCommon(GetBackgroundPredicate(BackgroundPredFilename));
+        LogCommon(prelude);
+        LogCommon(proverCommands);
+
+        foreach (string! s in vcExprTranslator.AllTypeDecls)
+          LogCommon(s);
+        foreach (string! s in vcExprTranslator.AllAxioms)
+          LogBgPush(s);
+
+        LogCommonComment("Initialized all axioms.");
+      } else {
+        LogCommon(incProverCommands);
+      }
+
+      thmProver.Feed(prelude, 0);
+      thmProver.Feed(proverCommands, 0);
+
+      foreach (string! s in vcExprTranslator.AllTypeDecls)
+        thmProver.Feed(s, 0);
+      foreach (string! s in vcExprTranslator.AllAxioms)
+        thmProver.AddAxioms(s);
+
+      // we have sent everything to the prover and can clear the lists with
+      // new axioms and declarations
+      List<string!> x = vcExprTranslator.NewAxioms;
+      x = x;  // make the compiler happy: somebody uses the value of x
+      x = vcExprTranslator.NewTypeDecls;
+    }
+
+    public override ProverContext! Context
+    {
+      get { return this.ctx; }
+    }
+  }
+  
+  public class SimplifyTheoremProver : ProcessTheoremProver
+  {
+    [NotDelayed]
+    public SimplifyTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx)
+      throws UnexpectedProverOutputException;
+    {
+      base(options, gen, ctx, "simplify.exe", "UnivBackPred2.sx");
+    }
+    
+    protected override ProverProcess! CreateProverProcess(string! proverPath) {
+      return new SimplifyProverProcess(proverPath);
+    }
+
+    protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {
+      return new SimplifyVCExprTranslator(gen);
+    }
+  }
+
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+
+  public abstract class AxiomVCExprTranslator : VCExprTranslator {
+    protected AxiomVCExprTranslator() {
+      AllAxioms = new List<string!> ();
+      NewAxiomsAttr = new List<string!> ();
+      AllTypeDecls = new List<string!> ();
+      NewTypeDeclsAttr = new List<string!> ();
+    }
+
+    protected AxiomVCExprTranslator(AxiomVCExprTranslator! tl) {
+      AllAxioms = new List<string!> (tl.AllAxioms);
+      NewAxiomsAttr = new List<string!> (tl.NewAxiomsAttr);
+      AllTypeDecls = new List<string!> (tl.AllTypeDecls);
+      NewTypeDeclsAttr = new List<string!> (tl.NewTypeDeclsAttr);
+    }
+
+    // we store all typing-related axioms that have been sent to the prover
+    // so that the prover can be re-initialised in case it dies
+    public readonly List<string!>! AllAxioms;
+    private List<string!>! NewAxiomsAttr;
+
+    public List<string!>! NewAxioms { get {
+      List<string!>! res = NewAxiomsAttr;
+      NewAxiomsAttr = new List<string!> ();
+      return res;
+    } }
+
+    // similarly, a list of declarations that have been sent to the prover
+    public readonly List<string!>! AllTypeDecls;
+    private List<string!>! NewTypeDeclsAttr;
+
+    public List<string!>! NewTypeDecls { get {
+      List<string!>! res = NewTypeDeclsAttr;
+      NewTypeDeclsAttr = new List<string!> ();
+      return res;
+    } }
+
+    public void AddAxiom(string! axiom) {
+      AllAxioms.Add(axiom);
+      NewAxiomsAttr.Add(axiom);
+    }
+
+    public void AddTypeDecl(string! typeDecl) {
+      AllTypeDecls.Add(typeDecl);
+      NewTypeDeclsAttr.Add(typeDecl);
+    }
+  }
+
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+
+  public class SimplifyVCExprTranslator : AxiomVCExprTranslator {
+    public SimplifyVCExprTranslator(VCExpressionGenerator! gen) {
+      Gen = gen;
+      TypeAxiomBuilder! axBuilder;
+      switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+        case CommandLineOptions.TypeEncoding.Arguments:
+          axBuilder = new TypeAxiomBuilderArguments (gen);
+          break;
+        default:
+          axBuilder = new TypeAxiomBuilderPremisses (gen);
+          break;
+      }
+      axBuilder.Setup();
+      AxBuilder = axBuilder;
+      Namer = new UniqueNamer ();
+      LitAbstracter = new BigLiteralAbstracter (gen);
+    }
+
+    private SimplifyVCExprTranslator(SimplifyVCExprTranslator! tl) {
+      base(tl);
+      Gen = tl.Gen;
+      AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
+      Namer = (UniqueNamer)tl.Namer.Clone();
+      LitAbstracter = (BigLiteralAbstracter)tl.LitAbstracter.Clone();
+    }
+
+    public override Object! Clone() {
+      return new SimplifyVCExprTranslator(this);
+    }
+
+    private readonly VCExpressionGenerator! Gen;
+    private readonly TypeAxiomBuilder! AxBuilder;
+    private readonly UniqueNamer! Namer;
+    private readonly BigLiteralAbstracter! LitAbstracter;
+
+    public override string! translate(VCExpr! expr, int polarity) {
+      Let2ImpliesMutator! letImplier = new Let2ImpliesMutator (Gen);
+
+      // handle the types in the VCExpr
+      TypeEraser! eraser;
+      switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+        case CommandLineOptions.TypeEncoding.Arguments:
+          eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
+          break;
+        default:
+          eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
+          break;
+      }
+      VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);
+
+      TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
+      VCExpr! exprWithLet = flattener.Flatten(exprWithoutTypes);
+      VCExpr! exprWithoutLet = letImplier.Mutate(exprWithLet);
+
+      // big integer literals
+      VCExpr! exprWithoutBigLits = LitAbstracter.Abstract(exprWithoutLet);
+      AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(LitAbstracter.GetNewAxioms(),
+                                                           Namer));
+
+      // type axioms
+      VCExpr! axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
+      VCExpr! axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
+
+      AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(axiomsWithoutLet, Namer));
+      return SimplifyLikeExprLineariser.ToSimplifyString(exprWithoutBigLits, Namer);
+    }
+  }
+
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+
+  public class Factory : ProverFactory
+  {
+    public override object! SpawnProver(ProverOptions! options, object! ctxt)
+    {
+      return new SimplifyTheoremProver(options,
+                                       ((DeclFreeProverContext!)ctxt).ExprGen,
+                                       (DeclFreeProverContext!)ctxt);
+    }
+
+    public override object! NewProverContext(ProverOptions! options) {
+      if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+        CommandLineOptions.Clo.BracketIdsInVC = 1;
+      }
+      VCExpressionGenerator! gen = new VCExpressionGenerator();
+      List<string!>! proverCommands = new List<string!> ();
+      proverCommands.Add("all");
+      proverCommands.Add("simplify");
+      proverCommands.Add("simplifyLike");
+      return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));
+    }
+
+    public override CommandLineOptions.VCVariety DefaultVCVariety
+    {
+      get { return CommandLineOptions.VCVariety.BlockNested; }
+    }
+
+    // needed to make test7 pass
+    public override bool SupportsDags
+    {
+      get { return true; }
+    }
+  }
+}
diff --git a/Source/Provers/Simplify/Simplify.sscproj b/Source/Provers/Simplify/Simplify.sscproj
new file mode 100644
index 00000000..675a766b
--- /dev/null
+++ b/Source/Provers/Simplify/Simplify.sscproj
@@ -0,0 +1,135 @@
+<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+  <XEN ProjectType="Local"
+     SchemaVersion="1.0"
+     Name="Simplify"
+     ProjectGuid="f75666de-fb56-457c-8782-09be243450fc"
+    >
+    <Build>
+      <Settings ApplicationIcon=""
+         AssemblyName="Provers.Simplify"
+         OutputType="Library"
+         RootNamespace="Microsoft.Boogie.Simplify"
+         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"
+           ReferenceTypesAreNonNullByDefault="False"
+           RunProgramVerifier="False"
+           RunProgramVerifierWhileEditing="False"
+           ProgramVerifierCommandLineOptions=""
+           AllowPointersToManagedStructures="False"
+           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"
+           />
+      </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="Core"
+             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+             Private="true"
+             />
+        <Reference Name="AIFramework"
+             Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
+             Private="true"
+             />
+        <Reference Name="Graph"
+             Project="{4C28FB90-630E-4B55-A937-11A011B79765}"
+             Private="true"
+             />
+        <Reference Name="Mscorlib.Contracts"
+             AssemblyName="Mscorlib.Contracts"
+             Private="false"
+             HintPath="../../../Binaries/Mscorlib.Contracts.dll"
+             />
+        <Reference Name="System.Contracts"
+             AssemblyName="System.Contracts"
+             Private="false"
+             HintPath="../../../Binaries/System.Contracts.dll"
+             />
+        <Reference Name="VCGeneration"
+             Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
+             Private="true"
+             />
+        <Reference Name="Basetypes"
+             Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+             Private="true"
+             />
+        <Reference Name="VCExpr"
+             Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
+             Private="true"
+             />
+      </References>
+    </Build>
+    <Files>
+      <Include>
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="Prover.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="ProverInterface.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="..\..\version.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="Let2ImpliesVisitor.ssc"
+                 />
+      </Include>
+    </Files>
+    <Target Name="AfterBuild"
+                >
+    </Target>
+  </XEN>
+</VisualStudioProject>
+\ No newline at end of file
diff --git a/Source/Provers/Z3/Inspector.ssc b/Source/Provers/Z3/Inspector.ssc
new file mode 100644
index 00000000..ca7fc084
--- /dev/null
+++ b/Source/Provers/Z3/Inspector.ssc
@@ -0,0 +1,130 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+  internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
+    public Dictionary<string!,bool>! Labels = new Dictionary<string!,bool>();
+
+    public static Dictionary<string!,bool>! FindLabels(VCExpr! expr) {
+      FindLabelsVisitor! visitor = new FindLabelsVisitor();
+      visitor.Traverse(expr, true);
+      return visitor.Labels;
+    }
+    
+    protected override bool StandardResult(VCExpr! node, bool arg) {
+      VCExprNAry nary = node as VCExprNAry;
+      if (nary != null) {
+        VCExprLabelOp lab = nary.Op as VCExprLabelOp;
+        if (lab != null) {
+          Labels[lab.label] = lab.pos;
+        }
+      }
+      return true;      
+    }
+  }
+
+  internal class Inspector {
+    [Rep] protected readonly Process! inspector;
+    [Rep] readonly TextReader! fromInspector;
+    [Rep] readonly TextWriter! toInspector;
+
+    public Inspector(Z3InstanceOptions! opts)
+    {
+      ProcessStartInfo! psi = new ProcessStartInfo(opts.Inspector);
+      psi.CreateNoWindow = true;
+      psi.UseShellExecute = false;
+      psi.RedirectStandardInput = true;
+      psi.RedirectStandardOutput = true;
+      psi.RedirectStandardError = false;
+
+      try 
+      {
+        Process inspector = Process.Start(psi);
+        this.inspector = inspector;
+        fromInspector = inspector.StandardOutput;
+        toInspector = inspector.StandardInput;
+      } 
+      catch (System.ComponentModel.Win32Exception e)
+      {
+        throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));
+      }
+    }
+
+    public void NewProver()
+    {
+    }
+
+    public void NewProblem(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
+    {
+      Dictionary<string!,bool>! labels = FindLabelsVisitor.FindLabels(vc);
+      toInspector.WriteLine("PROBLEM " + descriptiveName);
+      toInspector.WriteLine("TOKEN BEGIN");
+      foreach (string! lab in labels.Keys) {
+        string! no = lab.Substring(1);
+        Absy! absy = handler.Label2Absy(no);
+        IToken tok = absy.tok;
+        AssertCmd assrt = absy as AssertCmd;
+        Block blk = absy as Block;
+        string val = tok.val; // might require computation, so cache it
+        if (val == "foo" || tok.filename == null) continue; // no token
+        if (!val.Contains(" ")) val = null;
+
+        toInspector.Write("TOKEN ");
+        toInspector.Write(lab);
+        toInspector.Write(" ");
+
+        if (assrt != null) {
+          toInspector.Write("ASSERT");
+          string errData = assrt.ErrorData as string;
+          if (errData != null) {
+            val = errData;
+          } else if (assrt.ErrorMessage != null) {
+            val = assrt.ErrorMessage;
+          }
+        } else if (blk != null) {
+          toInspector.Write("BLOCK ");
+          toInspector.Write(blk.Label);
+        } else {
+          assume false;
+        }
+        if (val == null) { val = ""; }
+
+        if (absy is LoopInitAssertCmd) {
+          val += " (loop entry)";
+        } else if (absy is LoopInvMaintainedAssertCmd) {
+          val += " (loop body)";
+        } else if (absy is AssertRequiresCmd && val == "") {
+          AssertRequiresCmd req = (AssertRequiresCmd)absy;
+          IToken t2 = req.Requires.tok;
+          val = string.Format("precondition {0}({1},{2})", t2.filename, t2.line, t2.col);
+        }
+
+        val = val.Replace("\r", "").Replace("\n", " ");
+
+        toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));
+      }
+      toInspector.WriteLine("TOKEN END");
+    }
+
+    public void StatsLine(string! line)
+    {
+      toInspector.WriteLine(line);
+      toInspector.Flush();
+    }
+  }
+}
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
new file mode 100644
index 00000000..d3212a9c
--- /dev/null
+++ b/Source/Provers/Z3/Prover.ssc
@@ -0,0 +1,870 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using System.Text;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Basetypes;
+
+// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
+namespace Microsoft.Boogie.Z3
+{
+  internal class Z3ProverProcess : ProverProcess {
+    [Peer] private Z3InstanceOptions! opts;
+    [Peer] private readonly Inspector? inspector;
+    private readonly bool expectingModel = false;
+
+    private string! cmdLineArgs = "";
+    class OptionValue {
+      public readonly string! Option;
+      public readonly string! Value;
+      public OptionValue(string! option, string! value) { Option = option; Value = value; }
+    }
+    static void AddOption(List<OptionValue!>! parms, string! option, string! value)
+      modifies parms.*;
+    {
+      OptionValue ov = new OptionValue(option, value);
+      Owner.AssignSame(ov, Owner.ElementProxy(parms));
+      parms.Add(ov);
+    }
+    private List<OptionValue!>! parameterSettings;
+
+    // [NotDelayed]
+    [Captured]
+    public Z3ProverProcess(Z3InstanceOptions! opts, Inspector? inspector)
+      requires inspector != null ==> Owner.Same(opts, inspector);
+    { // throws ProverException
+      string! z3args = OptionChar() + "si";
+      List<OptionValue!> parms = new List<OptionValue!>();
+
+      if (opts.V2) {
+        AddOption(parms, "MODEL_PARTIAL", "true");
+        AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
+        AddOption(parms, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
+        AddOption(parms, "MODEL_V1", "true");
+        AddOption(parms, "ASYNC_COMMANDS", "false");
+      } else {
+        AddOption(parms, "PARTIAL_MODELS", "true");
+        AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
+        AddOption(parms, "HIDE_UNUSED_PARTITIONS", "false");
+      }
+
+      if (opts.V2) {
+        // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
+        // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
+        AddOption(parms, "PHASE_SELECTION", "0");
+        AddOption(parms, "RESTART_STRATEGY", "0");
+        AddOption(parms, "RESTART_FACTOR", "|1.5|");
+
+        // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
+        // the foo(x0) will be activated for e-matching when x is skolemized to x0.
+        AddOption(parms, "NNF_SK_HACK", "true");
+
+        // More or less like MAM=0.
+        AddOption(parms, "QI_EAGER_THRESHOLD", "100");
+
+        // Make the integer model more diverse by default, speeds up some benchmarks a lot.
+        AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");
+
+        // The left-to-right structural case-splitting strategy.
+        AddOption(parms, "SORT_AND_OR", "false");
+        AddOption(parms, "CASE_SPLIT", "3");
+
+        // In addition delay adding unit conflicts.
+        AddOption(parms, "DELAY_UNITS", "true");
+        AddOption(parms, "DELAY_UNITS_THRESHOLD", "16");
+
+        if (opts.Inspector != null) {
+          AddOption(parms, "PROGRESS_SAMPLING_FREQ", "100");
+        }
+      } else {
+        z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;
+      }
+
+      if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+        z3args += " " + OptionChar() + "@ " +
+                        OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;
+      }
+      if (0 <= opts.Timeout) {
+        z3args += " " + OptionChar() + "t:" + opts.Timeout;
+      }
+      if (opts.Typed) {
+        AddOption(parms, "TYPE_CHECK", "true");
+        if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native) {
+          if (opts.V2) {
+            AddOption(parms, "BV_REFLECT", "true");
+          } else {
+            AddOption(parms, "REFLECT_BV_OPS", "true");
+          }
+        }
+      }
+      if (CommandLineOptions.Clo.PrintErrorModel >= 1 || CommandLineOptions.Clo.EnhancedErrorMessages == 1 || CommandLineOptions.Clo.ContractInfer) {
+        z3args += " " + OptionChar() + "m";
+        expectingModel = true;
+      }
+      // Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args
+      if (opts.V1) {
+        foreach (OptionValue opt in parms) {
+          z3args += string.Format(" \"{0}={1}\"", opt.Option, opt.Value);
+        }
+      }
+      
+      foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
+        int eq = opt.IndexOf("=");
+        // we add them both to command line and the input file:
+        //    - allow for overriding default options
+        //    - some options (like TRACE) work only from command line
+        // Also options with spaces do not work with (SETPARAMETER ...)
+        if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {
+          AddOption(parms, opt.Substring(0, eq), opt.Substring(eq + 1));
+        }
+        z3args += " \"" + opt + "\"";
+      }
+
+      
+      cmdLineArgs = z3args;
+      parameterSettings = parms;
+      
+      string exePath = opts.ExeName;
+      if (!File.Exists(exePath)){
+        exePath = @"c:\Program Files\Microsoft Research\Z3-2.0\bin";
+      }
+      
+      ProcessStartInfo! psi = new ProcessStartInfo(exePath, z3args);
+      psi.CreateNoWindow = true;
+      psi.UseShellExecute = false;
+      psi.RedirectStandardInput = true;
+      psi.RedirectStandardOutput = true;
+      psi.RedirectStandardError = true;
+      
+      base(psi, opts.ExeName);
+
+      Owner.AssignSame(this, opts);
+      this.opts = opts;
+      this.inspector = inspector;
+    }
+    
+    public override string! OptionComments()
+    {
+      StringBuilder sb = new StringBuilder();
+      sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",
+                      opts.ExeName, cmdLineArgs);
+      assume CommandLineOptions.Clo.IsPeerConsistent;
+      foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
+        sb.Append(" ").Append(opt);
+      }
+      sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
+      return sb.ToString();
+    }
+
+    [Pure(false)]
+    public override IEnumerable<string!>! ParameterSettings {
+      get {
+        if (opts.V2) {
+          foreach (OptionValue opt in parameterSettings) {
+            yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
+          }
+        }
+      }
+    }
+
+    // z3 uses different magic characters for options on linux/unix and on windows
+    private static string! OptionChar() {
+      assume Environment.OSVersion != null;
+      switch (Environment.OSVersion.Platform) {
+        case PlatformID.Unix:
+          return "-";
+        default:
+          return "/";
+      }
+    }
+
+    protected override void DoBeginCheck(string! descriptiveName, string! formula)
+    {
+      ToWriteLine(formula);
+      ToWriteLine(String.Format(";   END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
+      ToFlush();
+    }
+
+    protected int TimedFromReadChar()
+    {
+      if (opts.Timeout > 0)
+        return FromReadChar((opts.Timeout + 1) * 1000);
+      else
+        return FromReadChar();
+    }
+
+    private void Trace(string! msg)
+    { 
+      Console.WriteLine("Z3: " + msg);
+    }
+
+    public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler) 
+      throws UnexpectedProverOutputException;
+    {
+      ProverOutcome outcome;
+      bool isInvalid = false;
+
+      if (this.simplify == null) {
+        return ProverOutcome.Inconclusive;
+      }
+
+
+      while (true) {
+        int ch = TimedFromReadChar();
+        if (ch == -1 && this.readTimedOut) {
+          handler.OnResourceExceeded("timeout (forced)");
+          return ProverOutcome.TimeOut;
+        }
+
+        string line = new string((char)ch, 1) + FromReadLine();
+
+        if (line.StartsWith("STATS ")) {
+          if (inspector != null) {
+            inspector.StatsLine(line);
+          }
+          continue;
+        }
+
+        if (opts.Verbosity > 2) {
+          Trace("INPUT: " + line);
+        }
+
+		if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
+		  handler.OnResourceExceeded("memory");
+		  return ProverOutcome.OutOfMemory;
+		}
+
+
+        if (line.StartsWith("WARNING: ")) {
+          string w = line.Substring(9);
+          ReportWarning(w);
+          continue;
+        }
+
+        if (line.ToUpper().StartsWith("ERROR")) {
+          Console.WriteLine("Z3 returns the following error:");
+          Console.WriteLine("    " + line);
+          return ProverOutcome.Inconclusive;
+        }
+
+        int beg = 0;
+        while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9')
+          invariant beg <= line.Length;
+        {
+          beg++;
+        }
+
+        if (beg > 0 && line.Substring(beg).StartsWith(": ")) {
+          string status = line.Substring(beg + 2);
+
+          if (status.StartsWith("Valid")) {
+            return ProverOutcome.Valid;
+          }
+
+          if (status.StartsWith("Timeout")) {
+            handler.OnResourceExceeded("timeout");
+            return ProverOutcome.TimeOut;
+          }
+
+          if (status.StartsWith("Inconclusive")) {
+            return ProverOutcome.Inconclusive;
+          }
+
+          if (status.StartsWith("Invalid")) {
+            isInvalid = true;
+            continue;
+          }
+        }
+
+        if (isInvalid && line == ".") {
+          return ProverOutcome.NotValid;
+        }
+
+        if (isInvalid && line.StartsWith("labels: (")) {
+          List<string!>! l = ParseLabels(line);
+          Z3ErrorModel errModel = null;
+          if (expectingModel) {
+            if (opts.Verbosity > 2) {
+              Trace("waiting for model");
+            }
+            line = FromReadLine();
+            if (line.StartsWith("partitions:")) {
+              line = ParseModel(out errModel);
+              if (opts.Verbosity > 2) {
+                Trace("model parsed, final line " + line);
+              }
+              // Z3 always ends the model with END_OF_MODEL, not with labels: or .
+              assume line == "END_OF_MODEL";
+            } else {
+              throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
+            }
+          }
+          handler.OnModel(l, errModel);
+          continue;
+        }
+
+        throw new UnexpectedProverOutputException(string.Format("evil input from z3: '{0}'", line));
+      }
+    }
+  
+    /* ----------------------------------------------------------------------------
+    BNF Grammar to parse Z3 output, including the model generated when using the /m /si switch:
+
+    Output  ::= VC*
+    VC      ::= number ": " "Valid." | number ": " "Inconclusive" | VCI
+    VCI     ::= number ": " "Invalid"
+                ("labels: " "(" ID* ")"
+                [MODEL] "END_OF_MODEL")+
+                "."
+    MODEL   ::= MBOOL MFUNC
+    MBOOL   ::= "boolean assignment:"
+                "partitions:"
+                MAPPING*
+    MAPPING ::= ZID ["{" ID+"}"] ["->" "(" (number | false | true | BITVECTOR) ")"]
+    BITVECTOR ::= ulong ":bv" int
+    MFUNC   ::= "function interpretations:"
+                F*
+    F       ::= Id "->" "{"
+                MAPLET*
+                "else" "->" ZID
+                "}"
+    MAPLET  ::= ZID* "->" ZID
+
+    -----------------------------------------------------------------------------*/
+    private string! ParseModel(out Z3ErrorModel errModel) 
+      modifies this.*;
+      ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
+      throws UnexpectedProverOutputException;
+    {
+      //Format in the grammar:
+      // ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
+      // storing the model:
+      // map each ID (a string) to the corresping ZID (an integer) in a dictionary:
+      Dictionary<string!, int> identifierToPartition = new Dictionary<string!, int>();
+      // map each ZID to the set (in list form) of IDs belonging to it (possibly empty):
+      List<List<string!>> partitionToIdentifiers = new List<List<string!>>();
+      // map each ZID to the number or boolean given, if any:
+      List<Object> partitionToValue = new List<Object>();
+      // map each value (number or boolean) to the ZID, reverse map of partitionToValue
+      Dictionary<Object, int> valueToPartition = new Dictionary<Object, int>();
+      Owner.AssignSame(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+
+      int ch;
+
+      // read the MAPPING
+      for (int zID = 0; true; zID++)
+      {
+        ch = FromReadChar();
+        if (ch == 'f') {
+          break;
+        }
+        ParseModelMapping(zID, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
+      }// end MAPPING
+
+      // add the fake partition for the 'else -> #undefined' clause
+      List<string!> emptyList = new List<string!>();
+      Owner.AssignSame(emptyList, Owner.ElementProxy(partitionToIdentifiers));
+      partitionToIdentifiers.Add(emptyList);
+      partitionToValue.Add(null);
+
+      // continue in ParseModelFunctions, which breaks up this long method and enables its verification
+      return ParseModelFunctions(ch, out errModel, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
+    }
+
+    private void ParseModelMapping(int zID,
+        Dictionary<string!, int>! identifierToPartition,
+        List<List<string!>>! partitionToIdentifiers,
+        List<Object>! partitionToValue,
+        Dictionary<Object, int>! valueToPartition)
+      requires Owner.Same(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+      modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
+    {
+      string s = FromReadLine();
+      {
+        // sanity check
+        int pos = s.IndexOf(' ');
+        string n = s;
+        int k;
+        if (pos >= 0) {
+          n = s.Substring(0,pos);
+        }
+        if (! (int.TryParse(n, out k) && zID == k)) {
+          System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
+          assume false;
+        }
+      }
+      
+      int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
+      
+      j = s.IndexOf(" -> ", j);
+      if (0 <= j) {
+        j += 4;
+      }
+      assume j == -1 || j < s.Length;  // if ' -> ' is present, then more should remain of the line
+      if (j == -1) {
+        // no "-> " found, end of this line, store that there is no value:
+        partitionToValue.Add(null);
+        int idForNull;
+        if (identifierToPartition.TryGetValue("nullObject", out idForNull) && idForNull == zID) {
+          assume !valueToPartition.ContainsKey("nullObject");  // a RHS value should occur only once in the Z3 output
+          valueToPartition.Add("nullObject", zID);
+          // In this case partitionToValue (as the reverse of valueToPartition) should include
+          // a map from zID -> "nullObject", but doing that breaks printing out the model as 
+          // it is printed out by Z3. Also, that information is not required, valueToPartition
+          // works well enough by itself.
+        }
+        
+      } else if (s[j] == 't'/*rue*/) {
+        partitionToValue.Add(true);
+        object boxedTrue = true;
+        assume !valueToPartition.ContainsKey(boxedTrue);  // a RHS value should occur only once in the Z3 output
+        valueToPartition.Add(boxedTrue, zID);
+      } else if (s[j] == 'f'/*alse*/) {
+        object boxedFalse = false;
+        Owner.AssignSame(boxedFalse, Owner.ElementProxy(partitionToValue));
+        partitionToValue.Add(boxedFalse);
+        assume !valueToPartition.ContainsKey(boxedFalse);  // a RHS value should occur only once in the Z3 output
+        valueToPartition.Add(boxedFalse, zID);
+      } else if (s[j] == 'v') {
+        // -> val!..., i.e. no value
+        partitionToValue.Add(null);
+      } else {
+        string numberOrBv = s.Substring(j);
+        // make number an int, then store it:
+        BigNum bvVal;
+        int bvSize;
+        string number, type;
+
+        int l = numberOrBv.IndexOf(':', 0);
+        if (0 <= l) {
+          number = numberOrBv.Substring(0, l);
+          type = numberOrBv.Substring(l + 1);
+        } else {
+          l = numberOrBv.IndexOf('[', 0);
+          if (0 <= l) {
+            number = numberOrBv.Substring(2, l-2);
+            int closingBracePosition = numberOrBv.IndexOf(']', l);
+            if (l < closingBracePosition)
+              type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
+            else type = "int";
+          } else {
+            number = numberOrBv;
+            type = "int";
+          }
+        }
+
+        if (type == "int") {
+          object boxedN = BigNum.FromString(number);
+          assume Owner.None(boxedN);
+          Owner.AssignSame(boxedN, Owner.ElementProxy(partitionToValue));
+          partitionToValue.Add(boxedN);
+          assume !valueToPartition.ContainsKey(boxedN);  // a RHS value should occur only once in the Z3 output
+          valueToPartition.Add(boxedN, zID); 
+        } else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {
+          BvConst bitV = new BvConst(bvVal, bvSize);
+          Owner.AssignSame(bitV, Owner.ElementProxy(partitionToValue));
+          partitionToValue.Add(bitV);
+          assume !valueToPartition.ContainsKey(bitV);  // a RHS value should occur only once in the Z3 output
+          valueToPartition.Add(bitV, zID);
+        } else {
+          System.Console.WriteLine("cannot parse type: '{0}':'{1}'", number, type);
+          assume false;
+        }
+
+      }
+    }
+
+    private static int ParseModelZidAndIdentifiers(int zID, string! s,
+        Dictionary<string!, int>! identifierToPartition,
+        List<List<string!>>! partitionToIdentifiers)
+      modifies identifierToPartition.*, partitionToIdentifiers.*;
+      ensures 0 <= result && result <= s.Length;
+    {
+      List<string!> identifiers = new List<string!>();
+      int j = s.IndexOf('{', 0) + 1;  // skip the '{', if present, and set j to 0 otherwise
+      if (1 <= j) {
+        // There is a list of ID's.
+        assume j < s.Length;  // there should be more characters; the ending '}', for one
+        //ID*
+        while (true) 
+          invariant identifiers.IsPeerConsistent && identifierToPartition.IsPeerConsistent && partitionToIdentifiers.IsPeerConsistent;
+          invariant 0 <= j && j < s.Length;
+        {
+          int k = s.IndexOfAny(new char[]{' ', '}'}, j);
+          assume j <= k;
+          string id = s.Substring(j, k-j);
+          j = k+1;
+          assume !identifierToPartition.ContainsKey(id);  // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
+          identifierToPartition.Add(id, zID);
+          identifiers.Add(id);
+          if (s[k] == '}') {
+            // end of reading ID*
+            break;
+          }
+          assume j < s.Length;  // there should be more characters; the ending '}', for one
+        }//end ID*
+      }
+      Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));
+      partitionToIdentifiers.Add(identifiers);
+      return j;
+    }
+                  
+    private string! ParseModelFunctions(int ch, out Z3ErrorModel errModel,
+      Dictionary<string!, int>! identifierToPartition,
+      List<List<string!>>! partitionToIdentifiers,
+      List<Object>! partitionToValue,
+      Dictionary<Object, int>! valueToPartition
+    ) 
+      modifies this.*;
+      ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
+      throws UnexpectedProverOutputException;
+    {
+      // read the function F
+      Expect(ch, "function interpretations:");
+      FromReadLine();
+      
+      // mapping of function names to function definitions
+      Dictionary<string!, List<List<int>>!> definedFunctions = new Dictionary<string!, List<List<int>>!>();
+      // function definition given as list of 'pointwise definitions' in the form of the arguments and result
+      // the last element here will always be a list with just one entry which corresponds to the else case
+      List<List<int>> functionDefinition = new List<List<int>>();
+      // list of arguments, followed by the result, the last element of this list is always the result
+      List<int> argumentsAndResult = new List<int>();
+      
+      // read F
+      while (true) 
+      {
+        functionDefinition = new List<List<int>>();
+        string s = FromReadLine();
+        // end of F, "END_OF_MODEL" ends model, '.' ends whole VC, 'l' starts a new set of labels and model
+        //           whenever there is a model this will end with "END_OF_MODEL", the other cases can only
+        //           happen when there is no model printed!
+        if (s == "." || s.StartsWith("labels: (") || s == "END_OF_MODEL") {
+          errModel = new Z3ErrorModel(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions);
+          return s;
+        }
+        int j = s.IndexOf(' ', 0);
+        assume 0 <= j;
+        string id = s.Substring(0, j);
+        // id is stored into definedFunctions once the function definition for it has 
+        // been completely parsed, 
+        
+        // just ignore the "-> {" by dropping string s
+        string zIDstring;
+        
+        // MAPLET
+        while (true) 
+        {
+          argumentsAndResult = new List<int>();
+          // remove the 2 spaces that are here
+          FromReadChar();
+          FromReadChar();
+          s = FromReadLine();
+          if (s.StartsWith("else ->")) break;
+          j = 0;
+          
+          //ZID*
+          while(true) 
+            invariant 0 <= j && j <= s.Length;
+          {
+            j = s.IndexOfAny(new Char[]{'*', '-'}, j);
+            // true because this always ends with a "->":
+            assume 0 <= j;
+            
+            // reading -> means end of ZID*
+            if (s[j] == '-'/*>*/) break;
+            
+            // start reading the ZID* with the number, not the *
+            j = j + 1;
+            // by input string format:
+            assume j < s.Length;
+            int k = s.IndexOf(' ', j);
+            // by input string format:
+            assume j <= k;
+            zIDstring = s.Substring(j, k-j);
+            // add the arguments
+            argumentsAndResult.Add(int.Parse(zIDstring));
+            j = k;
+          }// end ZID*
+          
+          // j is the beginning of "-> *", we want the first character after this
+          j = j + 4;
+          // by input string format:
+          assume j <= s.Length;
+          zIDstring = s.Substring(j);
+          // add the result
+          argumentsAndResult.Add(int.Parse(zIDstring));
+          // add the input line as another 'pointwise defined' element to the functions definition
+          functionDefinition.Add(argumentsAndResult);
+        }// end MAPLET
+
+        // this is the 'else -> #unspecified' case
+        // by input string format:
+        assume s.IndexOf("#unspec") >= 0;
+        // this stores the else line as another argumentsAndResult list
+        argumentsAndResult = new List<int>();
+        argumentsAndResult.Add(partitionToIdentifiers.Count - 1); // use the fake partition we have created before
+        // which is then added to the function definition, which is now complete
+        Owner.AssignSame(argumentsAndResult, Owner.ElementProxy(functionDefinition));
+        functionDefinition.Add(argumentsAndResult);
+
+    /*
+        // this is the 'else -> *' case, that string is already in s
+        j = s.IndexOf('*', 0) + 1;
+        // by input string format:
+        assume 0 < j && j < s.Length;
+        zIDstring = s.Substring(j);
+        // this stores the else line as another argumentsAndResult list
+        argumentsAndResult = new List<int>();
+        argumentsAndResult.Add(int.Parse(zIDstring));
+        // which is then added to the function definition, which is now complete
+        functionDefinition.Add(argumentsAndResult); */
+
+        // and therefore added to the map of defined functions, together with the name 'id'
+        // which had been extracted before
+        assume !definedFunctions.ContainsKey(id);  // each function name in the model is listed only once
+        definedFunctions.Add(id, functionDefinition);
+        
+        // read the line with "}"
+        ch = FromReadChar();
+        Expect(ch, "}");
+        FromReadLine();
+      }// end F
+    }
+
+  }
+
+
+  public class Z3ErrorModel : ErrorModel 
+  {
+    public Z3ErrorModel(Dictionary<string!, int>! identifierToPartition, List<List<string!>>! partitionToIdentifiers, List<Object>! partitionToValue, Dictionary<object, int>! valueToPartition, Dictionary<string!, List<List<int>>!>! definedFunctions)
+      : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions)
+    {
+      this.partitionNames = new string?[partitionToIdentifiers.Count];
+      this.prevPartitionNames = new string?[partitionToIdentifiers.Count];
+    }
+
+    private string?[]! partitionNames;
+    private string?[]! prevPartitionNames;
+
+    private void SetNames()
+    {
+      int len = partitionToIdentifiers.Count;
+      for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
+        prevPartitionNames = partitionNames;
+        partitionNames = new string?[len];
+        for (int pos = 0; pos < len; ++pos)
+          GetPartitionName(pos);
+      }
+    }
+
+    private int NameBadness(string! name)
+    {
+      int badness = name.Length;
+      if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
+        badness += 1000;
+      if (name.IndexOf ("(") > 0)
+        badness += 500;
+      return badness;
+    }
+
+    private string! GetPartitionName(int pos)
+    {
+      string name = partitionNames[pos];
+      if (name != null) {
+        return name;
+      }
+
+      object tmp = partitionToValue[pos];
+      if (tmp != null) {
+        partitionNames[pos] = tmp is BvConst ?  ((BvConst)tmp).ToReadableString() : tmp.ToString();
+      } else {
+        List<string!>! possible_names = new List<string!>();
+        List<string!> pti = partitionToIdentifiers[pos];
+
+        // make sure we're not called recursively
+        string prevName = prevPartitionNames[pos];
+        if (prevName == null) prevName = "*" + pos;
+        partitionNames[pos] = prevName;
+
+        if (pti != null && pti.Count > 0) {
+          // add identifiers
+          foreach (string! name in pti)
+            possible_names.Add(name);
+        }
+
+        // Then also look for functions,
+        // and then collect possible functional definitions
+        foreach (KeyValuePair<string!, List<List<int>>!> kv in definedFunctions) {
+          foreach (List<int>! parms in kv.Value) {
+            if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
+              string! s = kv.Key + "(";
+              for (int i = 0; i < parms.Count - 1; ++i) {
+                if (i != 0) s += ", ";
+                s += GetPartitionName(parms[i]);
+              }
+              s += ")";
+              possible_names.Add(s);
+            }
+          }
+        }
+
+        // choose the shortest possible name
+        if (possible_names.Count > 0) {
+          string! best = possible_names[0];
+          foreach (string! s in possible_names)
+            if (NameBadness(s) < NameBadness(best)) best = s;
+          if (best.Length < 120)
+            partitionNames[pos] = best;
+        }
+      }
+
+      return (!)partitionNames[pos];
+    }
+    
+    private void PrintReadableModel (TextWriter! writer) {
+      writer.WriteLine("Z3 error model: ");
+      SetNames();
+      writer.WriteLine("partitions:");
+      assert partitionToIdentifiers.Count == partitionToValue.Count;
+      for (int i = 0; i < partitionToIdentifiers.Count; i++){
+        writer.Write("{0,5}: {1}  ", "*"+i, GetPartitionName(i));
+        List<string!> pti = partitionToIdentifiers[i];
+        if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
+          writer.Write("{");
+          for (int k = 0; k < pti.Count - 1; k ++) {
+            writer.Write(pti[k] + " ");
+          }
+          //extra work to make sure no " " is at the end of the list of identifiers
+          if (pti.Count != 0) {
+            writer.Write(pti[pti.Count - 1]);
+          }
+          writer.Write("}");
+        }
+        writer.WriteLine();
+      }
+
+      writer.WriteLine();
+      writer.WriteLine("function interpretations:");
+      List<string!> funNames = new List<string!>(definedFunctions.Keys);
+      funNames.Sort();
+      foreach (string! name in funNames) {
+        if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
+        foreach (List<int>! parms in definedFunctions[name]) {
+          string! s = name + "(";
+          if (parms.Count == 1) {
+            continue;
+            // s += "*";
+          } else {
+            for (int i = 0; i < parms.Count - 1; ++i) {
+              if (i != 0) s += ", ";
+              s += GetPartitionName(parms[i]);
+            }
+          }
+          s += ")";
+          string! res = GetPartitionName(parms[parms.Count - 1]);
+          if (res == s)
+            res = "*" + parms[parms.Count - 1] + " (SELF)";
+          writer.WriteLine("{0} = {1}", s, res);
+        }
+        writer.WriteLine();
+      }
+      writer.WriteLine("The end.");
+      writer.WriteLine();
+    }
+
+    public override void Print (TextWriter! writer) {
+      if (CommandLineOptions.Clo.PrintErrorModel == 4) {
+        PrintReadableModel(writer);
+        return;
+      }
+
+      writer.WriteLine("Z3 error model: ");
+
+      writer.WriteLine("partitions:");
+      assert partitionToIdentifiers.Count == partitionToValue.Count;
+      for (int i = 0; i < partitionToIdentifiers.Count; i++){
+        writer.Write("*"+i);
+        List<string!> pti = partitionToIdentifiers[i];
+        if (pti != null && pti.Count != 0) {
+          writer.Write(" {");
+          for (int k = 0; k < pti.Count - 1; k ++) {
+            writer.Write(pti[k] + " ");
+          }
+          //extra work to make sure no " " is at the end of the list of identifiers
+          if (pti.Count != 0) {
+            writer.Write(pti[pti.Count - 1]);
+          }
+          writer.Write("}");
+        }
+        // temp object needed for non-null checking
+        object tempPTVI = partitionToValue[i];
+        if (tempPTVI != null) {
+          if (tempPTVI.ToString() == "True") {
+            writer.Write(" -> " + "true" + "");
+          } else if (tempPTVI.ToString() == "False") {
+            writer.Write(" -> " + "false" + "");
+          } else if (tempPTVI is BigNum) {
+            writer.Write(" -> " + tempPTVI + ":int");
+          } else {
+            writer.Write(" -> " + tempPTVI + "");
+          }
+        } else {
+          writer.Write(" ");
+        }
+        writer.WriteLine();
+      }
+
+      writer.WriteLine("function interpretations:");
+      foreach (KeyValuePair<string!, List<List<int>>!> kvp in definedFunctions) {
+        writer.WriteLine(kvp.Key + " -> {");
+        List<List<int>> kvpValue = kvp.Value;
+        if (kvpValue != null) {
+          foreach(List<int> l in kvpValue) {
+            writer.Write("  ");
+            if (l != null) {
+              for (int i = 0; i < l.Count - 1; i++) {
+                writer.Write("*"+l[i] + " ");
+              }
+              if (l.Count == 1) {
+                writer.WriteLine("else -> #unspecified");
+              } else {
+                writer.WriteLine("-> "+ "*" + l[l.Count - 1]);
+              }
+            }
+          }
+        }
+        writer.WriteLine("}");
+      }
+      writer.WriteLine("END_OF_MODEL");
+      writer.WriteLine(".");
+      
+      if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
+        writer.WriteLine("identifierToPartition:");
+        foreach (KeyValuePair<string!, int> kvp in identifierToPartition) {
+          writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);  
+        }
+        
+        writer.WriteLine("valueToPartition:");
+        foreach (KeyValuePair<object, int> kvp in valueToPartition) {
+          writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
+        }
+        writer.WriteLine("End of model.");
+      }
+    }
+  }
+
+
+}
+
+
diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc
new file mode 100644
index 00000000..02b4f505
--- /dev/null
+++ b/Source/Provers/Z3/ProverInterface.ssc
@@ -0,0 +1,320 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Text;
+using ExternalProver;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Clustering;
+using Microsoft.Boogie.TypeErasure;
+using Microsoft.Boogie.Z3;
+using Microsoft.Boogie.Simplify;
+
+namespace Microsoft.Boogie.Z3
+{
+  public class Z3ProcessTheoremProver : ProcessTheoremProver
+  {
+    private Z3InstanceOptions! opts;
+    private Inspector inspector;
+
+    [NotDelayed]
+    public Z3ProcessTheoremProver(VCExpressionGenerator! gen,
+                                  DeclFreeProverContext! ctx, Z3InstanceOptions! opts)
+      throws UnexpectedProverOutputException;
+    {
+      this.opts = opts;
+      string! backPred = opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx";
+      base(opts, gen, ctx, opts.ExeName, backPred);
+    }
+
+    private void FireUpInspector()
+    {
+      if (inspector == null && opts.Inspector != null) {
+        inspector = new Inspector(opts);
+      }
+    }
+    
+    protected override Microsoft.Boogie.Simplify.ProverProcess! CreateProverProcess(string! proverPath) {
+      opts.ExeName = proverPath;
+      FireUpInspector();
+      if (inspector != null) {
+        inspector.NewProver();
+      }
+      return new Z3ProverProcess(opts, inspector);
+    }
+
+    protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {
+      return new Z3VCExprTranslator(gen, opts);
+    }
+
+    public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler)
+    {
+      FireUpInspector();
+      if (inspector != null) {
+        inspector.NewProblem(descriptiveName, vc, handler);
+      }
+      base.BeginCheck(descriptiveName, vc, handler);
+    }
+  }
+
+  public class Z3InstanceOptions : ProverOptions
+  {
+    public int Timeout { get { return TimeLimit / 1000; } }
+    public bool Typed {
+      get { 
+        return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native; 
+      } 
+    }
+    public bool V1 = false;
+    public bool V2 = false; // default set in PostParse
+    public bool DistZ3 = false;
+    public string! ExeName = "z3.exe";
+    public bool InverseImplies = false;
+    public string? Inspector = null;
+
+    protected override bool Parse(string! opt)
+    {
+      return ParseBool(opt, "V1", ref V1) ||
+             ParseBool(opt, "V2", ref V2) ||
+             ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
+             ParseString(opt, "INSPECTOR", ref Inspector) ||
+             ParseBool(opt, "DIST", ref DistZ3) ||
+             base.Parse(opt);
+    }
+
+    protected override void PostParse()
+    {
+      base.PostParse();
+
+      if (!V1 && !V2) {
+        V2 = true; // default
+      } else if (V1 && V2) {
+        ReportError("V1 and V2 requested at the same time");
+      } else if (V1 && DistZ3) {
+        ReportError("V1 and DistZ3 requested at the same time");
+      }
+      if (V1) {
+        ExeName = "z3-v1.3.exe";
+      }
+      if (DistZ3) {
+		ExeName = "z3-dist.exe";
+		CommandLineOptions.Clo.RestartProverPerVC = true;
+      }
+      
+    }
+  }
+
+  internal class Z3LineariserOptions : LineariserOptions {
+    private readonly Z3InstanceOptions! opts;
+
+    public override CommandLineOptions.BvHandling Bitvectors { get {
+      return opts.BitVectors;
+    } }
+ 
+    internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions !opts, List<VCExprVar!>! letVariables) {
+      base(asTerm);
+      this.opts = opts;
+      this.LetVariablesAttr = letVariables;
+    }
+
+    public override bool UseWeights { get {
+      return opts.V2;
+    } }
+
+    public override bool UseTypes { get {
+      return opts.Typed;
+    } }
+
+    public override bool QuantifierIds { get {
+      return true;
+    } }
+
+    public override bool InverseImplies { get { 
+      return opts.InverseImplies;
+    } }
+
+    public override LineariserOptions! SetAsTerm(bool newVal) {
+      if (newVal == AsTerm)
+        return this;
+      return new Z3LineariserOptions(newVal, opts, LetVariables);
+    }
+
+    // variables representing formulas in let-bindings have to be
+    // printed in a different way than other variables
+    private readonly List<VCExprVar!>! LetVariablesAttr;
+    public override List<VCExprVar!>! LetVariables { get {
+      return LetVariablesAttr;
+    } }
+
+    public override LineariserOptions! AddLetVariable(VCExprVar! furtherVar) {
+      List<VCExprVar!>! allVars = new List<VCExprVar!> ();
+      allVars.AddRange(LetVariables);
+      allVars.Add(furtherVar);
+      return new Z3LineariserOptions(AsTerm, opts, allVars);
+    }
+  }
+
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+
+  public class Z3VCExprTranslator : AxiomVCExprTranslator {
+    public Z3VCExprTranslator(VCExpressionGenerator! gen, Z3InstanceOptions! opts) {
+      Gen = gen;
+      Opts = opts;
+      TypeAxiomBuilder! axBuilder;
+      switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+        case CommandLineOptions.TypeEncoding.Arguments:
+          axBuilder = new TypeAxiomBuilderArguments (gen);
+          break;
+        default:
+          axBuilder = new TypeAxiomBuilderPremisses (gen);
+          break;
+      }
+      axBuilder.Setup();
+      AxBuilder = axBuilder;
+      UniqueNamer namer = new UniqueNamer ();
+      Namer = namer;
+      this.DeclCollector =
+        new TypeDeclCollector (namer, opts.BitVectors == CommandLineOptions.BvHandling.Z3Native);
+    }
+
+    private Z3VCExprTranslator(Z3VCExprTranslator! tl) {
+      base(tl);
+      Gen = tl.Gen;
+      Opts = tl.Opts; // we assume that the options have not changed
+      AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
+      UniqueNamer namer = (UniqueNamer)tl.Namer.Clone();
+      Namer = namer;
+      DeclCollector = new TypeDeclCollector (namer, tl.DeclCollector);
+    }
+
+    public override Object! Clone() {
+      return new Z3VCExprTranslator(this);
+    }
+
+    private readonly Z3InstanceOptions! Opts;
+    private readonly VCExpressionGenerator! Gen;
+    private readonly TypeAxiomBuilder! AxBuilder;
+    private readonly UniqueNamer! Namer;
+    private readonly TypeDeclCollector! DeclCollector;
+
+    public override string! translate(VCExpr! expr, int polarity) {
+      DateTime start = DateTime.Now;
+      if (CommandLineOptions.Clo.Trace)
+        Console.Write("Linearising ... ");
+
+      // handle the types in the VCExpr
+      TypeEraser eraser;
+      switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+        case CommandLineOptions.TypeEncoding.Arguments:
+          eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
+          break;
+        case CommandLineOptions.TypeEncoding.Monomorphic:
+          eraser = null;
+          break;
+        default:
+          eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
+          break;
+      }
+      
+      VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
+      
+      LetBindingSorter! letSorter = new LetBindingSorter(Gen);
+      VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
+      VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+
+      if (Opts.Typed) {
+        DeclCollector.Collect(sortedAxioms);
+        DeclCollector.Collect(sortedExpr);
+        FeedTypeDeclsToProver();
+      } else {
+        TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
+        sortedExpr = flattener.Flatten(sortedExpr);
+        sortedAxioms = flattener.Flatten(sortedAxioms);
+      }
+
+      //////////////////////////////////////////////////////////////////////////
+      //SubtermCollector! coll = new SubtermCollector (gen);
+      //coll.Traverse(sortedExpr, true);
+      //coll.Traverse(sortedAxioms, true);
+      //coll.UnifyClusters();
+      //Console.WriteLine(coll);
+      //////////////////////////////////////////////////////////////////////////
+
+      LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar!>());
+
+      AddAxiom(SimplifyLikeExprLineariser.ToString(sortedAxioms, linOptions, Namer));
+
+      string! res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
+
+      if (CommandLineOptions.Clo.Trace) {
+        TimeSpan elapsed = DateTime.Now - start;
+        Console.WriteLine("finished   [{0} s]  ", elapsed.TotalSeconds);
+      }
+      return res;
+    }
+
+    private void FeedTypeDeclsToProver() {
+      foreach (string! s in DeclCollector.GetNewDeclarations())
+        AddTypeDecl(s);
+    }
+  }
+
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+  // -----------------------------------------------------------------------------------------------
+
+  public class Factory : ProverFactory
+  {
+
+    public override object! SpawnProver(ProverOptions! popts, object! ctxt)
+    {
+      Z3InstanceOptions opts = (Z3InstanceOptions!)popts;
+      return this.SpawnProver(((DeclFreeProverContext!)ctxt).ExprGen,
+                              (DeclFreeProverContext!)ctxt,
+                              opts);
+    }
+
+    public override object! NewProverContext(ProverOptions! options) {
+      if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+        CommandLineOptions.Clo.BracketIdsInVC = 0;
+      }
+
+      Z3InstanceOptions opts = (Z3InstanceOptions!)options;
+      VCExpressionGenerator! gen = new VCExpressionGenerator ();
+      List<string!>! proverCommands = new List<string!> ();
+      proverCommands.Add("all");
+      proverCommands.Add("z3");
+      proverCommands.Add("simplifyLike");
+      if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
+        proverCommands.Add("bvDefSem");
+      if (opts.BitVectors == CommandLineOptions.BvHandling.ToInt)
+        proverCommands.Add("bvInt");
+      VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands);
+
+      return new DeclFreeProverContext(gen, genOptions);
+    }
+
+    public override ProverOptions! BlankProverOptions()
+    {
+      return new Z3InstanceOptions();
+    }
+
+    protected virtual Z3ProcessTheoremProver! SpawnProver(VCExpressionGenerator! gen,
+                                                          DeclFreeProverContext! ctx,
+                                                          Z3InstanceOptions! opts) {
+      return new Z3ProcessTheoremProver(gen, ctx, opts);
+    }
+  }
+}
diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc
new file mode 100644
index 00000000..86307b45
--- /dev/null
+++ b/Source/Provers/Z3/TypeDeclCollector.ssc
@@ -0,0 +1,212 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+  // Visitor for collecting the occurring function symbols in a VCExpr,
+  // and for creating the corresponding declarations that can be fed into
+  // Z3
+
+  // (should this be rather done by Context.DeclareFunction? right now,
+  // the TypeErasure visitor introduces new function symbols that are
+  // not passed to this method)
+
+  public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+
+    private readonly UniqueNamer! Namer;
+
+    private readonly bool NativeBv;
+
+    public TypeDeclCollector(UniqueNamer! namer, bool nativeBv) {
+      this.Namer = namer;
+      this.NativeBv = nativeBv;
+      AllDecls = new List<string!> ();
+      IncDecls = new List<string!> ();
+      KnownFunctions = new Dictionary<Function!, bool> ();
+      KnownVariables = new Dictionary<VCExprVar!, bool> ();
+      KnownTypes = new Dictionary<Type!, bool> ();
+      KnownBvOps = new Dictionary<string!, bool> ();
+    }
+
+    internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) {
+      this.Namer = namer;
+      this.NativeBv = coll.NativeBv;
+      AllDecls = new List<string!> (coll.AllDecls);
+      IncDecls = new List<string!> (coll.IncDecls);
+      KnownFunctions = new Dictionary<Function!, bool> (coll.KnownFunctions);
+      KnownVariables = new Dictionary<VCExprVar!, bool> (coll.KnownVariables);
+      KnownTypes = new Dictionary<Type!, bool> (coll.KnownTypes);
+      KnownBvOps = new Dictionary<string!, bool> (coll.KnownBvOps);
+    }
+
+    // not used
+    protected override bool StandardResult(VCExpr! node, bool arg) {
+      return true;
+    }
+
+    private readonly List<string!>! AllDecls;
+    private readonly List<string!>! IncDecls;
+
+    private readonly IDictionary<Function!, bool>! KnownFunctions;
+    private readonly IDictionary<VCExprVar!, bool>! KnownVariables;
+
+    // bitvector types have to be registered as well
+    private readonly IDictionary<Type!, bool>! KnownTypes;
+
+    // the names of registered BvConcatOps and BvExtractOps
+    private readonly IDictionary<string!, bool>! KnownBvOps;
+
+    public List<string!>! AllDeclarations { get {
+      List<string!>! res = new List<string!> ();
+      res.AddRange(AllDecls);
+      return res;
+    } }
+
+    public List<string!>! GetNewDeclarations() {
+      List<string!>! res = new List<string!> ();
+      res.AddRange(IncDecls);
+      IncDecls.Clear();
+      return res;
+    }
+
+    private void AddDeclaration(string! decl) {
+      AllDecls.Add(decl);
+      IncDecls.Add(decl);
+    }
+
+    public void Collect(VCExpr! expr) {
+      Traverse(expr, true);
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+
+    private static string! TypeToString(Type! t) {
+      return SimplifyLikeExprLineariser.TypeToString(t);
+    }
+
+    private void RegisterType(Type! type)
+    {
+      if (!type.IsBv || !NativeBv) return;
+
+      if (!KnownTypes.ContainsKey(type)) {
+        int bits = type.BvBits;
+        string name = TypeToString(type);
+
+        AddDeclaration("(DEFTYPE " + name + " :BUILTIN BitVec " + bits + ")");
+        // If we add the BUILTIN then the conversion axiom does not work
+        AddDeclaration("(DEFOP " + name + "_to_int " + name + " $int)"); // :BUILTIN bv2int $int)");
+        AddDeclaration("(DEFOP $make_bv" + bits + " $int " + name + " :BUILTIN int2bv " + bits + ")");
+        string! expr = "($make_bv" + bits + " (" + name + "_to_int  x))";
+        AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "
+                       + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");
+
+        KnownTypes.Add(type, true);
+      }
+    }
+
+    public override bool Visit(VCExprNAry! node, bool arg) {
+      // there are a couple of cases where operators have to be
+      // registered by generating appropriate Z3 statements
+
+      if (node.Op.Equals(VCExpressionGenerator.BvConcatOp)) {
+        //
+        if (NativeBv) {
+          RegisterType(node[0].Type);
+          RegisterType(node[1].Type);
+          RegisterType(node.Type);
+
+          string name = SimplifyLikeExprLineariser.BvConcatOpName(node);
+          if (!KnownBvOps.ContainsKey(name)) {
+            AddDeclaration("(DEFOP " + name +
+                           " " + TypeToString(node[0].Type) +
+                           " " + TypeToString(node[1].Type) +
+                           " " + TypeToString(node.Type) +
+                           " :BUILTIN concat)");
+            KnownBvOps.Add(name, true);
+          }
+        }
+        //
+      } else if (node.Op is VCExprBvExtractOp) {
+        //
+        if (NativeBv) {
+          RegisterType(node[0].Type);
+          RegisterType(node.Type);
+
+          VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;
+          string name = SimplifyLikeExprLineariser.BvExtractOpName(node);
+          if (!KnownBvOps.ContainsKey(name)) {
+            AddDeclaration("(DEFOP " + name +
+                           " " + TypeToString(node[0].Type) +
+                           " " + TypeToString(node.Type) + 
+                           " :BUILTIN extract " +
+                           (op.End - 1) + " " + op.Start + ")");
+            KnownBvOps.Add(name, true);
+          }
+        }
+        //
+      } else {
+        //
+        VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
+        if (op != null && !KnownFunctions.ContainsKey(op.Func)) {
+          Function! f = op.Func;
+          string! printedName = Namer.GetName(f, f.Name);
+          string! decl = "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName);
+
+          foreach (Variable! v in f.InParams) {
+            decl += " " + TypeToString(v.TypedIdent.Type);
+            RegisterType(v.TypedIdent.Type);
+          }
+          assert f.OutParams.Length == 1;
+          foreach (Variable! v in f.OutParams) {
+            decl += " " + TypeToString(v.TypedIdent.Type);
+            RegisterType(v.TypedIdent.Type);
+          }
+
+          string? builtin = ExtractBuiltin(f);
+          if (builtin != null)
+            decl += " :BUILTIN " + builtin;
+
+          decl += ")";
+        
+          AddDeclaration(decl);
+          KnownFunctions.Add(f, true);
+        }
+        //
+      }
+
+      return base.Visit(node, arg);
+    }
+
+    private string? ExtractBuiltin(Function! f) {
+      if (NativeBv) {
+        return f.FindStringAttribute("bvbuiltin");
+      } else {
+        return null;
+      }
+    }
+
+    public override bool Visit(VCExprVar! node, bool arg) {
+      if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
+        RegisterType(node.Type);
+        string! printedName = Namer.GetName(node, node.Name);
+        string! decl =
+          "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)
+          + " " + TypeToString(node.Type) + ")";
+        AddDeclaration(decl);
+        KnownVariables.Add(node, true);
+      }
+
+      return base.Visit(node, arg);
+    }
+  }
+
+}
+\ No newline at end of file
diff --git a/Source/Provers/Z3/Z3.sscproj b/Source/Provers/Z3/Z3.sscproj
new file mode 100644
index 00000000..5370a640
--- /dev/null
+++ b/Source/Provers/Z3/Z3.sscproj
@@ -0,0 +1,140 @@
+<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+  <XEN ProjectType="Local"
+     SchemaVersion="1.0"
+     Name="Z3"
+     ProjectGuid="f75666de-cd56-457c-8782-09be243450fc"
+    >
+    <Build>
+      <Settings ApplicationIcon=""
+         AssemblyName="Provers.Z3"
+         OutputType="Library"
+         RootNamespace="Microsoft.Boogie.Z3"
+         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"
+           ReferenceTypesAreNonNullByDefault="False"
+           RunProgramVerifier="False"
+           RunProgramVerifierWhileEditing="False"
+           ProgramVerifierCommandLineOptions=""
+           AllowPointersToManagedStructures="False"
+           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"
+           />
+      </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="Core"
+             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+             Private="true"
+             />
+        <Reference Name="AIFramework"
+             Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
+             Private="true"
+             />
+        <Reference Name="Graph"
+             Project="{4C28FB90-630E-4B55-A937-11A011B79765}"
+             Private="true"
+             />
+        <Reference Name="Mscorlib.Contracts"
+             AssemblyName="Mscorlib.Contracts"
+             Private="false"
+             HintPath="../../../Binaries/Mscorlib.Contracts.dll"
+             />
+        <Reference Name="System.Contracts"
+             AssemblyName="System.Contracts"
+             Private="false"
+             HintPath="../../../Binaries/System.Contracts.dll"
+             />
+        <Reference Name="VCGeneration"
+             Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
+             Private="true"
+             />
+        <Reference Name="Simplify"
+             Project="{F75666DE-FB56-457C-8782-09BE243450FC}"
+             Private="true"
+             />
+        <Reference Name="Basetypes"
+             Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+             Private="true"
+             />
+        <Reference Name="VCExpr"
+             Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
+             Private="true"
+             />
+      </References>
+    </Build>
+    <Files>
+      <Include>
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="Prover.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="ProverInterface.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="..\..\version.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="TypeDeclCollector.ssc"
+                 />
+        <File BuildAction="Compile"
+                 SubType="Code"
+                 RelPath="Inspector.ssc"
+                 />
+      </Include>
+    </Files>
+  </XEN>
+</VisualStudioProject>
+\ No newline at end of file
author	mikebarnett <unknown>	2009-07-15 21:03:41 +0000
committer	mikebarnett <unknown>	2009-07-15 21:03:41 +0000
commit	ce1c2de044c91624370411e23acab13b0381949b (patch)
tree	592539996fe08050ead5ee210c973801611dde40 /Source/Provers