8 files changed, 2394 insertions, 2394 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index ad0c2239..87fd8c17 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -1,728 +1,728 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Threading;

-using System.IO;

-using System.Diagnostics;

-using Microsoft.Boogie.AbstractInterpretation;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Z3;

-using Microsoft.Z3;

-using Microsoft.Boogie.VCExprAST;

-using Microsoft.Basetypes;

-

-using Z3Model = Microsoft.Z3.Model;

-using BoogieModel = Microsoft.Boogie.Model;

-

-namespace Microsoft.Boogie.Z3 {

-  public class Z3apiProverContext : DeclFreeProverContext {

-    private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();

-    internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();

-    internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();

-    internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();

-    internal BacktrackDictionary<Term, VCExpr> constants_inv = null;

-    internal BacktrackDictionary<FuncDecl, Function> functions_inv = null;

-

-    public Config config;

-    public Context z3;

-

-    private Z3TypeCachedBuilder tm;

-    private UniqueNamer namer;

-    private StreamWriter z3log;

-

-    private int counterexamples;

-    private string logFilename;

-    private List<string> debugTraces;

-

-    public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)

-      : base(gen, new VCGenerationOptions(new List<string>())) {

-      int timeout = opts.Timeout * 1000;

-      config = new Config();

-      config.SetParamValue("MODEL", "true");

-      config.SetParamValue("MODEL_V2", "true");

-      config.SetParamValue("MODEL_COMPLETION", "true");

-      config.SetParamValue("MBQI", "false");

-      config.SetParamValue("TYPE_CHECK", "true");

-      if (0 <= timeout) {

-        config.SetParamValue("SOFT_TIMEOUT", timeout.ToString());

-      }

-

-      if (0 <= CommandLineOptions.Clo.ProverCCLimit) {

-        this.counterexamples = CommandLineOptions.Clo.ProverCCLimit;

-      }

-      if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {

-        logFilename = CommandLineOptions.Clo.SimplifyLogFilePath;

-      }

-      this.debugTraces = new List<string>();

-

-      z3 = new Context(config);

-      z3.SetPrintMode(PrintMode.Smtlib2Compliant);

-      if (logFilename != null)

-      {

-#if true

-          Z3Log.Open(logFilename);

-#else

-          z3.OpenLog(logFilename);

-#endif

-      }

-      foreach (string tag in debugTraces)

-        z3.EnableDebugTrace(tag);

-

-      this.z3log = null;

-      this.tm = new Z3TypeCachedBuilder(this);

-      this.namer = new UniqueNamer();

-    }

-

-    public Z3apiProverContext(Context ctx, VCExpressionGenerator gen)

-        : base(gen, new VCGenerationOptions(new List<string>()))

-    {

-        z3 = ctx;

-

-        this.z3log = null;

-        this.tm = new Z3TypeCachedBuilder(this);

-        this.namer = new UniqueNamer();

-

-        // For external 

-

-        constants_inv = new BacktrackDictionary<Term, VCExpr>();

-        functions_inv = new BacktrackDictionary<FuncDecl, Function>();

-    }

-

-    public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) {

-        Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

-        return (Term)expr.Accept(visitor, linOptions);

-    }

-

-

-    private class fromZ3

-    {

-        private VCExpressionGenerator gen;

-        private Dictionary<Term, VCExpr> memo;

-        private BacktrackDictionary<Term, VCExpr> constants_inv;

-        private BacktrackDictionary<FuncDecl, Function> functions_inv;

-        private List<VCExprLetBinding> lets;

-        private int let_ctr = 0;

-

-        private VCExpr create_let(Term t, VCExpr u)

-        {

-            var name = "$x" + let_ctr.ToString();

-            let_ctr++;

-            var sym = gen.Variable(name, u.Type);

-            memo.Remove(t);

-            memo.Add(t, sym);

-            lets.Add(gen.LetBinding(sym, u));

-            return sym;

-        }

-

-        public fromZ3(VCExpressionGenerator _gen,

-                      BacktrackDictionary<Term, VCExpr> _constants_inv,

-                      BacktrackDictionary<FuncDecl, Function> _functions_inv)

-        {

-            gen = _gen;

-            constants_inv = _constants_inv;

-            functions_inv = _functions_inv;

-            memo = new Dictionary<Term, VCExpr>();

-            lets = new List<VCExprLetBinding>();

-        }

-

-        public void clear()

-        {

-            memo.Clear();

-            lets.Clear();

-        }

-        public VCExpr get(Term arg)

-        {

-            if (memo.ContainsKey(arg))

-                return memo[arg];

-            VCExpr res = null;

-            switch (arg.GetKind())

-            {

-                case TermKind.Numeral:

-                    var numstr = arg.GetNumeralString();

-                    if (arg.GetSort().GetSortKind() == SortKind.Int) {

-                      res = gen.Integer(Basetypes.BigNum.FromString(numstr));

-                    }

-                    else {

-                      res = gen.Real(Basetypes.BigDec.FromString(numstr));

-                    }

-                    break;

-                case TermKind.App:

-                    var args = arg.GetAppArgs();

-                    var vcargs = new VCExpr[args.Length];

-                    for (int i = 0; i < args.Length; i++)

-                        vcargs[i] = get(args[i]);

-

-                    switch (arg.GetAppDecl().GetKind())

-                    {

-                        case DeclKind.Add:

-                            if (vcargs.Length == 0) {

-                              if (arg.GetSort().GetSortKind() == SortKind.Int) {

-                                res = gen.Integer(Basetypes.BigNum.ZERO);

-                              }

-                              else {

-                                res = gen.Real(Basetypes.BigDec.ZERO);

-                              }

-                            }

-                            else

-                            {

-                                res = vcargs[0];

-                                for (int k = 1; k < vcargs.Length; k++)

-                                    res = gen.Add(res, vcargs[k]);

-                            }

-                            break;

-                        case DeclKind.And:

-                            res = VCExpressionGenerator.True;

-                            for (int i = 0; i < vcargs.Length; i++)

-                                res = gen.AndSimp(res, vcargs[i]);

-                            break;

-                        case DeclKind.Div:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Eq:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Eq(vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.False:

-                            res = VCExpressionGenerator.False;

-                            break;

-                        case DeclKind.Ge:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Gt:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Gt(vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.IDiv:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Iff:

-                            Debug.Assert(vcargs.Length == 2);

-                            var l = create_let(args[0], vcargs[0]);

-                            var r = create_let(args[1], vcargs[1]);

-                            return gen.And(gen.Implies(l, r), gen.Implies(r, l));

-                        case DeclKind.Implies:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Implies(vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Ite:

-                            Debug.Assert(vcargs.Length == 3);

-                            res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]);

-                            break;

-                        case DeclKind.Le:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Lt:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Mod:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Mul:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Not:

-                            Debug.Assert(vcargs.Length == 1);

-                            res = gen.Not(vcargs[0]);

-                            break;

-                        case DeclKind.Or:

-                            res = VCExpressionGenerator.False;

-                            for (int i = 0; i < vcargs.Length; i++)

-                                res = gen.OrSimp(res, vcargs[i]);

-                            break;

-                        case DeclKind.Select:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Select(vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.Store:

-                            Debug.Assert(vcargs.Length == 3);

-                            res = gen.Store(vcargs[0], vcargs[1], vcargs[2]);

-                            break;

-                        case DeclKind.Sub:

-                            Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]);

-                            break;

-                        case DeclKind.True:

-                            res = VCExpressionGenerator.True;

-                            break;

-                        case DeclKind.Uminus:

-                            Debug.Assert(vcargs.Length == 1);

-                            var argzero = null;

-                            if (vcargs[0].Type.IsInt) {

-                              argzero = gen.Integer(Basetypes.BigNum.ZERO);

-                            }

-                            else {

-                              argzero = gen.Real(Basetypes.BigDec.ZERO);

-                            }

-                            res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]);

-                            break;

-                        case DeclKind.ToInt:

-                            Debug.Assert(vcargs.Length == 1);

-                            res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]);

-                            break;

-                        case DeclKind.ToReal:

-                            Debug.Assert(vcargs.Length == 1);

-                            res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]);

-                            break;

-                        case DeclKind.Uninterpreted:

-                            var name = arg.GetAppDecl().GetDeclName();

-                            if (args.Length == 0)

-                            { // a 0-ary constant is a VCExprVar

-                                if (!constants_inv.TryGetValue(arg, out res))

-                                    throw new Exception("Z3 returned unknown constant: " + name);

-                            }

-                            else

-                            {

-                                Function f;

-                                if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f))

-                                    throw new Exception("Z3 returned unknown function: " + name);

-                                List<VCExpr> vcargsList = new List<VCExpr>(vcargs);

-                                res = gen.Function(f, vcargsList);

-                            }   

-                            break;

-                        default:

-                            throw new Exception("Unknown Z3 operator");

-                    }

-                    break;

-                default:

-                    Debug.Assert(false);

-                    throw new Exception("Unknown Z3 AST kind");

-            }

-

-            memo.Add(arg, res);

-            return res;

-        }

-        public VCExpr add_lets(VCExpr e)

-        {

-            foreach (var let in lets)

-            {

-                e = gen.Let(e, let);

-            }

-            return e;

-        }

-    }

-

-    public VCExpr TermToVCExpr(Term t)

-    {

-      var fZ = new fromZ3(gen, constants_inv, functions_inv);

-      return fZ.add_lets(fZ.get(t));

-    }

-

-

-    

-

-

-    public override void DeclareType(TypeCtorDecl t, string attributes) {

-      base.DeclareType(t, attributes);

-      log("(declare-sort {0})", t.Name);

-    }

-

-    public override void DeclareConstant(Constant c, bool uniq, string attributes) {

-      base.DeclareConstant(c, uniq, attributes);

-      DeclareConstant(c.Name, c.TypedIdent.Type);

-    }

-

-    public override void DeclareFunction(Function f, string attributes) {

-      base.DeclareFunction(f, attributes);

-      List<Type> domain = new List<Type>();

-      foreach (Variable v in f.InParams) {

-        domain.Add(v.TypedIdent.Type);

-      }

-      if (f.OutParams.Length != 1)

-        throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters.");

-      Type range = f.OutParams[0].TypedIdent.Type;

-

-      string functionName = f.Name;

-      Symbol symbolAst = GetSymbol(functionName);

-      var domainStr = "";

-      List<Sort> domainAst = new List<Sort>();

-      foreach (Type domainType in domain) {

-        Sort type = tm.GetType(domainType);

-        domainAst.Add(type);

-        domainStr += type.ToString() + " ";

-      }

-      Sort rangeAst = tm.GetType(range);

-      FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);

-      functions.Add(functionName, constDeclAst);

-      if(functions_inv != null)functions_inv.Add(constDeclAst, f);

-      log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);

-    }

-

-    public override void DeclareGlobalVariable(GlobalVariable v, string attributes) {

-      base.DeclareGlobalVariable(v, attributes);

-      DeclareConstant(v.Name, v.TypedIdent.Type);

-    }

-

-    public override string Lookup(VCExprVar var) {

-      return namer.Lookup(var);

-    }

-

-    public void log(string format, params object[] args) {

-      // Currently, this is a no-op because z3log is always null

-      // We use the default (automatic) tracing facility of z3

-      if (z3log != null) {

-        var str = string.Format(format, args);

-        // Do standard string replacement

-        str = str.Replace("array", "Array");

-        z3log.WriteLine(str);

-        z3log.Flush();

-      }

-    }

-

-    public void CloseLog() {

-#if true

-        Z3Log.Close();

-#else

-        z3.CloseLog();

-#endif

-      if (z3log != null) {

-        z3log.Close();

-      }

-      z3log = null;

-    }

-

-    public void CreateBacktrackPoint() {

-      symbols.CreateBacktrackPoint();

-      constants.CreateBacktrackPoint();

-      functions.CreateBacktrackPoint();

-      labels.CreateBacktrackPoint();

-      if(constants_inv != null)constants_inv.CreateBacktrackPoint();

-      if(functions_inv != null)functions_inv.CreateBacktrackPoint();

-      z3.Push();

-      log("(push)");

-    }

-

-    public void Backtrack() {

-      z3.Pop();

-      labels.Backtrack();

-      functions.Backtrack();

-      constants.Backtrack();

-      symbols.Backtrack();

-      if (constants_inv != null) constants_inv.Backtrack();

-      if (functions_inv != null) functions_inv.Backtrack();

-      log("(pop)");

-    }

-

-    public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) {

-      Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

-      Term term = (Term)axiom.Accept(visitor, linOptions);

-      log("(assert {0})", term);

-      z3.AssertCnstr(term);

-    }

-

-    public void AddConjecture(VCExpr vc, LineariserOptions linOptions) {

-      VCExpr not_vc = (VCExpr)this.gen.Not(vc);

-      Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

-      Term term = (Term)not_vc.Accept(visitor, linOptions);

-      log("(assert {0})", term);

-      z3.AssertCnstr(term);

-    }

-

-    public void AddSmtlibString(string smtlibString) {

-      FuncDecl[] decls;

-      Term[] assumptions;

-      Term[] terms;

-      Sort[] sorts;

-      string tmp;

-

-      z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },

-                           out assumptions, out terms, out decls, out sorts, out tmp);

-      // TBD: check with Nikolaj about the correct position of assumptions

-      foreach (FuncDecl decl in decls) {

-        Symbol symbol = z3.GetDeclName(decl);

-        string functionName = z3.GetSymbolString(symbol);

-        functions.Add(functionName, decl);

-      }

-      foreach (Term assumption in assumptions) {

-        log("(assert {0})", assumption);

-        z3.AssertCnstr(assumption);

-      }

-    }

-

-    private List<Sort> GetTypes(List<Type> boogieTypes) {

-      List<Sort> z3Types = new List<Sort>();

-      foreach (Type boogieType in boogieTypes) {

-        Sort type = tm.GetType(boogieType);

-        z3Types.Add(type);

-      }

-      return z3Types;

-    }

-

-    private static bool Equals(List<string> l, List<string> r) {

-      Debug.Assert(l != null);

-      if (r == null)

-        return false;

-

-      if (l.Count != r.Count)

-        return false;

-

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

-        if (!l[i].Equals(r[i]))

-          return false;

-      return true;

-    }

-

-    private void DisplayRelevantLabels(List<string> relevantLabels) {

-      foreach (string labelName in relevantLabels) {

-        System.Console.Write(labelName + ",");

-      }

-      System.Console.WriteLine("---");

-    }

-

-    private void DeclareConstant(string constantName, Type boogieType) {

-      Symbol symbolAst = GetSymbol(constantName);

-      Sort typeAst = tm.GetType(boogieType);

-

-      Term constAst = z3.MkConst(symbolAst, typeAst);

-      constants.Add(constantName, constAst);

-      log("(declare-funs (({0} {1})))", constAst, typeAst);

-    }

-

-    public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {

-      Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");

-      boogieErrors = new List<Z3ErrorModelAndLabels>();

-      LBool outcome = LBool.Undef;

-      Debug.Assert(0 < this.counterexamples);

-      while (true) {

-        Z3Model z3Model;

-        outcome = z3.CheckAndGetModel(out z3Model);

-

-        log("(check-sat)");

-        if (outcome == LBool.False)

-          break;

-

-        if (outcome == LBool.Undef && z3Model == null) {

-          // Blame this on timeout

-          return ProverInterface.Outcome.TimeOut;

-        }

-

-        Debug.Assert(z3Model != null);

-        LabeledLiterals labels = z3.GetRelevantLabels();

-        Debug.Assert(labels != null);

-

-        List<string> labelStrings = new List<string>();

-        uint numLabels = labels.GetNumLabels();

-        for (uint i = 0; i < numLabels; ++i) {

-          Symbol sym = labels.GetLabel(i);

-          string labelName = z3.GetSymbolString(sym);

-          if (!labelName.StartsWith("@")) {

-            labels.Disable(i);

-          }

-          labelStrings.Add(labelName);

-        }

-

-        var sw = new StringWriter();

-        sw.WriteLine("*** MODEL");

-        z3Model.Display(sw);

-        sw.WriteLine("*** END_MODEL");

-        var sr = new StringReader(sw.ToString());

-        var models = Microsoft.Boogie.Model.ParseModels(sr);

-        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));

-        boogieErrors.Add(e);

-

-        if (boogieErrors.Count < this.counterexamples) {

-          z3.BlockLiterals(labels);

-          log("block-literals {0}", labels);

-        }

-

-        labels.Dispose();

-        z3Model.Dispose();

-        if (boogieErrors.Count == this.counterexamples)

-          break;

-      }

-

-      if (boogieErrors.Count > 0) {

-        return ProverInterface.Outcome.Invalid;

-      }

-      else if (outcome == LBool.False) {

-        return ProverInterface.Outcome.Valid;

-      }

-      else {

-        Debug.Assert(outcome == LBool.Undef);

-        return ProverInterface.Outcome.Undetermined;

-      }

-    }

-

-    public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,

-        out List<Z3ErrorModelAndLabels> boogieErrors,

-        out List<int> unsatCore) {

-      Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");

-      boogieErrors = new List<Z3ErrorModelAndLabels>();

-      unsatCore = new List<int>();

-      LBool outcome = LBool.Undef;

-

-      Z3Model z3Model;

-      Term proof;

-      Term[] core;

-      Term[] assumption_terms = new Term[assumptions.Count];

-      var logstring = "";

-      for (int i = 0; i < assumptions.Count; i++) {

-        Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

-        Term z3ast = (Term)assumptions[i].Accept(visitor, linOptions);

-        assumption_terms[i] = z3ast;

-        logstring += string.Format("({0}) ", assumption_terms[i]);

-      }

-

-      log("(get-core {0})", logstring);

-      outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);

-

-      if (outcome != LBool.False) {

-        Debug.Assert(z3Model != null);

-        LabeledLiterals labels = z3.GetRelevantLabels();

-        Debug.Assert(labels != null);

-

-        List<string> labelStrings = new List<string>();

-        uint numLabels = labels.GetNumLabels();

-        for (uint i = 0; i < numLabels; ++i) {

-          Symbol sym = labels.GetLabel(i);

-          string labelName = z3.GetSymbolString(sym);

-          if (!labelName.StartsWith("@")) {

-            labels.Disable(i);

-          }

-          labelStrings.Add(labelName);

-        }

-

-        var sw = new StringWriter();

-        sw.WriteLine("*** MODEL");

-        z3Model.Display(sw);

-        sw.WriteLine("*** END_MODEL");

-        var sr = new StringReader(sw.ToString());

-        var models = Microsoft.Boogie.Model.ParseModels(sr);

-        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));

-        boogieErrors.Add(e);

-

-        labels.Dispose();

-        z3Model.Dispose();

-      }

-

-      if (boogieErrors.Count > 0) {

-        return ProverInterface.Outcome.Invalid;

-      }

-      else if (outcome == LBool.False) {

-        foreach (Term t in core) {

-          for (int i = 0; i < assumption_terms.Length; i++) {

-            if (t.Equals(assumption_terms[i]))

-              unsatCore.Add(i);

-          }

-        }

-        return ProverInterface.Outcome.Valid;

-      }

-      else {

-        Debug.Assert(outcome == LBool.Undef);

-        return ProverInterface.Outcome.Undetermined;

-      }

-    }

-

-    private Symbol GetSymbol(string symbolName) {

-      if (!symbols.ContainsKey(symbolName)) {

-        Symbol symbolAst = z3.MkSymbol(symbolName);

-        symbols.Add(symbolName, symbolAst);

-      }

-      Symbol result;

-      if (!symbols.TryGetValue(symbolName, out result))

-        throw new Exception("symbol " + symbolName + " is undefined");

-      return result;

-    }

-

-    public Term GetConstant(string constantName, Type constantType, VCExpr node)

-    {

-      Term typeSafeTerm;

-      if (!constants.ContainsKey(constantName))

-        this.DeclareConstant(constantName, constantType);

-

-      if (!constants.TryGetValue(constantName, out typeSafeTerm))

-        throw new Exception("constant " + constantName + " is not defined");

-

-      if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm))

-          constants_inv.Add(typeSafeTerm, node);

-

-      return typeSafeTerm;

-    }

-

-    public FuncDecl GetFunction(string functionName) {

-      FuncDecl f;

-      if (!functions.TryGetValue(functionName, out f))

-        throw new Exception("function " + functionName + " is undefined");

-      return f;

-    }

-

-    public Term MakeLabel(string labelName, bool pos, Term child) {

-      Symbol labelSymbol = this.GetSymbol(labelName);

-      Term labeledExpr = z3.MkLabel(labelSymbol, pos, child);

-      labels.Add(labelName, labeledExpr);

-      return labeledExpr;

-    }

-

-    public LabeledLiterals GetRelevantLabels() {

-      LabeledLiterals safeLiterals = z3.GetRelevantLabels();

-      log("get-relevant-labels");

-      return safeLiterals;

-    }

-  }

-

-  internal class BacktrackDictionary<K, V> {

-    private Dictionary<K, V> dictionary = new Dictionary<K, V>();

-    private Stack<List<K>> keyStack = new Stack<List<K>>();

-

-    public BacktrackDictionary() {

-      CreateBacktrackPoint();

-    }

-

-    public bool TryGetValue(K key, out V val) {

-      return dictionary.TryGetValue(key, out val);

-    }

-

-    public void Add(K key, V v) {

-      if (dictionary.ContainsKey(key)) {

-        dictionary.Remove(key);

-      }

-      dictionary.Add(key, v);

-      keyStack.Peek().Add(key);

-    }

-

-    public bool ContainsKey(K k) {

-      return dictionary.ContainsKey(k);

-    }

-

-    public void CreateBacktrackPoint() {

-      keyStack.Push(new List<K>());

-    }

-

-    public void Backtrack() {

-      List<K> keysToErase = keyStack.Pop();

-      foreach (K key in keysToErase) {

-        dictionary.Remove(key);

-      }

-      if (keyStack.Count == 0)

-        this.CreateBacktrackPoint();

-    }

-

-    public IEnumerator GetEnumerator() {

-      return dictionary.Keys.GetEnumerator();

-    }

-  }

-

-  public class Z3ErrorModelAndLabels {

-    private Model _model;

-    private List<string> _relevantLabels;

-    public Model Model {

-      get { return this._model; }

-    }

-    public List<string> RelevantLabels {

-      get { return this._relevantLabels; }

-    }

-    public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) {

-      this._model = model;

-      this._relevantLabels = relevantLabels;

-    }

-  }

-

-

-

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Basetypes;
+
+using Z3Model = Microsoft.Z3.Model;
+using BoogieModel = Microsoft.Boogie.Model;
+
+namespace Microsoft.Boogie.Z3 {
+  public class Z3apiProverContext : DeclFreeProverContext {
+    private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();
+    internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();
+    internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();
+    internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();
+    internal BacktrackDictionary<Term, VCExpr> constants_inv = null;
+    internal BacktrackDictionary<FuncDecl, Function> functions_inv = null;
+
+    public Config config;
+    public Context z3;
+
+    private Z3TypeCachedBuilder tm;
+    private UniqueNamer namer;
+    private StreamWriter z3log;
+
+    private int counterexamples;
+    private string logFilename;
+    private List<string> debugTraces;
+
+    public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)
+      : base(gen, new VCGenerationOptions(new List<string>())) {
+      int timeout = opts.Timeout * 1000;
+      config = new Config();
+      config.SetParamValue("MODEL", "true");
+      config.SetParamValue("MODEL_V2", "true");
+      config.SetParamValue("MODEL_COMPLETION", "true");
+      config.SetParamValue("MBQI", "false");
+      config.SetParamValue("TYPE_CHECK", "true");
+      if (0 <= timeout) {
+        config.SetParamValue("SOFT_TIMEOUT", timeout.ToString());
+      }
+
+      if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+        this.counterexamples = CommandLineOptions.Clo.ProverCCLimit;
+      }
+      if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+        logFilename = CommandLineOptions.Clo.SimplifyLogFilePath;
+      }
+      this.debugTraces = new List<string>();
+
+      z3 = new Context(config);
+      z3.SetPrintMode(PrintMode.Smtlib2Compliant);
+      if (logFilename != null)
+      {
+#if true
+          Z3Log.Open(logFilename);
+#else
+          z3.OpenLog(logFilename);
+#endif
+      }
+      foreach (string tag in debugTraces)
+        z3.EnableDebugTrace(tag);
+
+      this.z3log = null;
+      this.tm = new Z3TypeCachedBuilder(this);
+      this.namer = new UniqueNamer();
+    }
+
+    public Z3apiProverContext(Context ctx, VCExpressionGenerator gen)
+        : base(gen, new VCGenerationOptions(new List<string>()))
+    {
+        z3 = ctx;
+
+        this.z3log = null;
+        this.tm = new Z3TypeCachedBuilder(this);
+        this.namer = new UniqueNamer();
+
+        // For external 
+
+        constants_inv = new BacktrackDictionary<Term, VCExpr>();
+        functions_inv = new BacktrackDictionary<FuncDecl, Function>();
+    }
+
+    public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) {
+        Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+        return (Term)expr.Accept(visitor, linOptions);
+    }
+
+
+    private class fromZ3
+    {
+        private VCExpressionGenerator gen;
+        private Dictionary<Term, VCExpr> memo;
+        private BacktrackDictionary<Term, VCExpr> constants_inv;
+        private BacktrackDictionary<FuncDecl, Function> functions_inv;
+        private List<VCExprLetBinding> lets;
+        private int let_ctr = 0;
+
+        private VCExpr create_let(Term t, VCExpr u)
+        {
+            var name = "$x" + let_ctr.ToString();
+            let_ctr++;
+            var sym = gen.Variable(name, u.Type);
+            memo.Remove(t);
+            memo.Add(t, sym);
+            lets.Add(gen.LetBinding(sym, u));
+            return sym;
+        }
+
+        public fromZ3(VCExpressionGenerator _gen,
+                      BacktrackDictionary<Term, VCExpr> _constants_inv,
+                      BacktrackDictionary<FuncDecl, Function> _functions_inv)
+        {
+            gen = _gen;
+            constants_inv = _constants_inv;
+            functions_inv = _functions_inv;
+            memo = new Dictionary<Term, VCExpr>();
+            lets = new List<VCExprLetBinding>();
+        }
+
+        public void clear()
+        {
+            memo.Clear();
+            lets.Clear();
+        }
+        public VCExpr get(Term arg)
+        {
+            if (memo.ContainsKey(arg))
+                return memo[arg];
+            VCExpr res = null;
+            switch (arg.GetKind())
+            {
+                case TermKind.Numeral:
+                    var numstr = arg.GetNumeralString();
+                    if (arg.GetSort().GetSortKind() == SortKind.Int) {
+                      res = gen.Integer(Basetypes.BigNum.FromString(numstr));
+                    }
+                    else {
+                      res = gen.Real(Basetypes.BigDec.FromString(numstr));
+                    }
+                    break;
+                case TermKind.App:
+                    var args = arg.GetAppArgs();
+                    var vcargs = new VCExpr[args.Length];
+                    for (int i = 0; i < args.Length; i++)
+                        vcargs[i] = get(args[i]);
+
+                    switch (arg.GetAppDecl().GetKind())
+                    {
+                        case DeclKind.Add:
+                            if (vcargs.Length == 0) {
+                              if (arg.GetSort().GetSortKind() == SortKind.Int) {
+                                res = gen.Integer(Basetypes.BigNum.ZERO);
+                              }
+                              else {
+                                res = gen.Real(Basetypes.BigDec.ZERO);
+                              }
+                            }
+                            else
+                            {
+                                res = vcargs[0];
+                                for (int k = 1; k < vcargs.Length; k++)
+                                    res = gen.Add(res, vcargs[k]);
+                            }
+                            break;
+                        case DeclKind.And:
+                            res = VCExpressionGenerator.True;
+                            for (int i = 0; i < vcargs.Length; i++)
+                                res = gen.AndSimp(res, vcargs[i]);
+                            break;
+                        case DeclKind.Div:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Eq:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Eq(vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.False:
+                            res = VCExpressionGenerator.False;
+                            break;
+                        case DeclKind.Ge:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Gt:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Gt(vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.IDiv:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Iff:
+                            Debug.Assert(vcargs.Length == 2);
+                            var l = create_let(args[0], vcargs[0]);
+                            var r = create_let(args[1], vcargs[1]);
+                            return gen.And(gen.Implies(l, r), gen.Implies(r, l));
+                        case DeclKind.Implies:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Implies(vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Ite:
+                            Debug.Assert(vcargs.Length == 3);
+                            res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]);
+                            break;
+                        case DeclKind.Le:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Lt:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Mod:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Mul:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Not:
+                            Debug.Assert(vcargs.Length == 1);
+                            res = gen.Not(vcargs[0]);
+                            break;
+                        case DeclKind.Or:
+                            res = VCExpressionGenerator.False;
+                            for (int i = 0; i < vcargs.Length; i++)
+                                res = gen.OrSimp(res, vcargs[i]);
+                            break;
+                        case DeclKind.Select:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Select(vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.Store:
+                            Debug.Assert(vcargs.Length == 3);
+                            res = gen.Store(vcargs[0], vcargs[1], vcargs[2]);
+                            break;
+                        case DeclKind.Sub:
+                            Debug.Assert(vcargs.Length == 2);
+                            res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]);
+                            break;
+                        case DeclKind.True:
+                            res = VCExpressionGenerator.True;
+                            break;
+                        case DeclKind.Uminus:
+                            Debug.Assert(vcargs.Length == 1);
+                            var argzero = null;
+                            if (vcargs[0].Type.IsInt) {
+                              argzero = gen.Integer(Basetypes.BigNum.ZERO);
+                            }
+                            else {
+                              argzero = gen.Real(Basetypes.BigDec.ZERO);
+                            }
+                            res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]);
+                            break;
+                        case DeclKind.ToInt:
+                            Debug.Assert(vcargs.Length == 1);
+                            res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]);
+                            break;
+                        case DeclKind.ToReal:
+                            Debug.Assert(vcargs.Length == 1);
+                            res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]);
+                            break;
+                        case DeclKind.Uninterpreted:
+                            var name = arg.GetAppDecl().GetDeclName();
+                            if (args.Length == 0)
+                            { // a 0-ary constant is a VCExprVar
+                                if (!constants_inv.TryGetValue(arg, out res))
+                                    throw new Exception("Z3 returned unknown constant: " + name);
+                            }
+                            else
+                            {
+                                Function f;
+                                if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f))
+                                    throw new Exception("Z3 returned unknown function: " + name);
+                                List<VCExpr> vcargsList = new List<VCExpr>(vcargs);
+                                res = gen.Function(f, vcargsList);
+                            }   
+                            break;
+                        default:
+                            throw new Exception("Unknown Z3 operator");
+                    }
+                    break;
+                default:
+                    Debug.Assert(false);
+                    throw new Exception("Unknown Z3 AST kind");
+            }
+
+            memo.Add(arg, res);
+            return res;
+        }
+        public VCExpr add_lets(VCExpr e)
+        {
+            foreach (var let in lets)
+            {
+                e = gen.Let(e, let);
+            }
+            return e;
+        }
+    }
+
+    public VCExpr TermToVCExpr(Term t)
+    {
+      var fZ = new fromZ3(gen, constants_inv, functions_inv);
+      return fZ.add_lets(fZ.get(t));
+    }
+
+
+    
+
+
+    public override void DeclareType(TypeCtorDecl t, string attributes) {
+      base.DeclareType(t, attributes);
+      log("(declare-sort {0})", t.Name);
+    }
+
+    public override void DeclareConstant(Constant c, bool uniq, string attributes) {
+      base.DeclareConstant(c, uniq, attributes);
+      DeclareConstant(c.Name, c.TypedIdent.Type);
+    }
+
+    public override void DeclareFunction(Function f, string attributes) {
+      base.DeclareFunction(f, attributes);
+      List<Type> domain = new List<Type>();
+      foreach (Variable v in f.InParams) {
+        domain.Add(v.TypedIdent.Type);
+      }
+      if (f.OutParams.Length != 1)
+        throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters.");
+      Type range = f.OutParams[0].TypedIdent.Type;
+
+      string functionName = f.Name;
+      Symbol symbolAst = GetSymbol(functionName);
+      var domainStr = "";
+      List<Sort> domainAst = new List<Sort>();
+      foreach (Type domainType in domain) {
+        Sort type = tm.GetType(domainType);
+        domainAst.Add(type);
+        domainStr += type.ToString() + " ";
+      }
+      Sort rangeAst = tm.GetType(range);
+      FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);
+      functions.Add(functionName, constDeclAst);
+      if(functions_inv != null)functions_inv.Add(constDeclAst, f);
+      log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);
+    }
+
+    public override void DeclareGlobalVariable(GlobalVariable v, string attributes) {
+      base.DeclareGlobalVariable(v, attributes);
+      DeclareConstant(v.Name, v.TypedIdent.Type);
+    }
+
+    public override string Lookup(VCExprVar var) {
+      return namer.Lookup(var);
+    }
+
+    public void log(string format, params object[] args) {
+      // Currently, this is a no-op because z3log is always null
+      // We use the default (automatic) tracing facility of z3
+      if (z3log != null) {
+        var str = string.Format(format, args);
+        // Do standard string replacement
+        str = str.Replace("array", "Array");
+        z3log.WriteLine(str);
+        z3log.Flush();
+      }
+    }
+
+    public void CloseLog() {
+#if true
+        Z3Log.Close();
+#else
+        z3.CloseLog();
+#endif
+      if (z3log != null) {
+        z3log.Close();
+      }
+      z3log = null;
+    }
+
+    public void CreateBacktrackPoint() {
+      symbols.CreateBacktrackPoint();
+      constants.CreateBacktrackPoint();
+      functions.CreateBacktrackPoint();
+      labels.CreateBacktrackPoint();
+      if(constants_inv != null)constants_inv.CreateBacktrackPoint();
+      if(functions_inv != null)functions_inv.CreateBacktrackPoint();
+      z3.Push();
+      log("(push)");
+    }
+
+    public void Backtrack() {
+      z3.Pop();
+      labels.Backtrack();
+      functions.Backtrack();
+      constants.Backtrack();
+      symbols.Backtrack();
+      if (constants_inv != null) constants_inv.Backtrack();
+      if (functions_inv != null) functions_inv.Backtrack();
+      log("(pop)");
+    }
+
+    public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) {
+      Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+      Term term = (Term)axiom.Accept(visitor, linOptions);
+      log("(assert {0})", term);
+      z3.AssertCnstr(term);
+    }
+
+    public void AddConjecture(VCExpr vc, LineariserOptions linOptions) {
+      VCExpr not_vc = (VCExpr)this.gen.Not(vc);
+      Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+      Term term = (Term)not_vc.Accept(visitor, linOptions);
+      log("(assert {0})", term);
+      z3.AssertCnstr(term);
+    }
+
+    public void AddSmtlibString(string smtlibString) {
+      FuncDecl[] decls;
+      Term[] assumptions;
+      Term[] terms;
+      Sort[] sorts;
+      string tmp;
+
+      z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },
+                           out assumptions, out terms, out decls, out sorts, out tmp);
+      // TBD: check with Nikolaj about the correct position of assumptions
+      foreach (FuncDecl decl in decls) {
+        Symbol symbol = z3.GetDeclName(decl);
+        string functionName = z3.GetSymbolString(symbol);
+        functions.Add(functionName, decl);
+      }
+      foreach (Term assumption in assumptions) {
+        log("(assert {0})", assumption);
+        z3.AssertCnstr(assumption);
+      }
+    }
+
+    private List<Sort> GetTypes(List<Type> boogieTypes) {
+      List<Sort> z3Types = new List<Sort>();
+      foreach (Type boogieType in boogieTypes) {
+        Sort type = tm.GetType(boogieType);
+        z3Types.Add(type);
+      }
+      return z3Types;
+    }
+
+    private static bool Equals(List<string> l, List<string> r) {
+      Debug.Assert(l != null);
+      if (r == null)
+        return false;
+
+      if (l.Count != r.Count)
+        return false;
+
+      for (int i = 0; i < l.Count; i++)
+        if (!l[i].Equals(r[i]))
+          return false;
+      return true;
+    }
+
+    private void DisplayRelevantLabels(List<string> relevantLabels) {
+      foreach (string labelName in relevantLabels) {
+        System.Console.Write(labelName + ",");
+      }
+      System.Console.WriteLine("---");
+    }
+
+    private void DeclareConstant(string constantName, Type boogieType) {
+      Symbol symbolAst = GetSymbol(constantName);
+      Sort typeAst = tm.GetType(boogieType);
+
+      Term constAst = z3.MkConst(symbolAst, typeAst);
+      constants.Add(constantName, constAst);
+      log("(declare-funs (({0} {1})))", constAst, typeAst);
+    }
+
+    public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {
+      Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
+      boogieErrors = new List<Z3ErrorModelAndLabels>();
+      LBool outcome = LBool.Undef;
+      Debug.Assert(0 < this.counterexamples);
+      while (true) {
+        Z3Model z3Model;
+        outcome = z3.CheckAndGetModel(out z3Model);
+
+        log("(check-sat)");
+        if (outcome == LBool.False)
+          break;
+
+        if (outcome == LBool.Undef && z3Model == null) {
+          // Blame this on timeout
+          return ProverInterface.Outcome.TimeOut;
+        }
+
+        Debug.Assert(z3Model != null);
+        LabeledLiterals labels = z3.GetRelevantLabels();
+        Debug.Assert(labels != null);
+
+        List<string> labelStrings = new List<string>();
+        uint numLabels = labels.GetNumLabels();
+        for (uint i = 0; i < numLabels; ++i) {
+          Symbol sym = labels.GetLabel(i);
+          string labelName = z3.GetSymbolString(sym);
+          if (!labelName.StartsWith("@")) {
+            labels.Disable(i);
+          }
+          labelStrings.Add(labelName);
+        }
+
+        var sw = new StringWriter();
+        sw.WriteLine("*** MODEL");
+        z3Model.Display(sw);
+        sw.WriteLine("*** END_MODEL");
+        var sr = new StringReader(sw.ToString());
+        var models = Microsoft.Boogie.Model.ParseModels(sr);
+        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
+        boogieErrors.Add(e);
+
+        if (boogieErrors.Count < this.counterexamples) {
+          z3.BlockLiterals(labels);
+          log("block-literals {0}", labels);
+        }
+
+        labels.Dispose();
+        z3Model.Dispose();
+        if (boogieErrors.Count == this.counterexamples)
+          break;
+      }
+
+      if (boogieErrors.Count > 0) {
+        return ProverInterface.Outcome.Invalid;
+      }
+      else if (outcome == LBool.False) {
+        return ProverInterface.Outcome.Valid;
+      }
+      else {
+        Debug.Assert(outcome == LBool.Undef);
+        return ProverInterface.Outcome.Undetermined;
+      }
+    }
+
+    public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,
+        out List<Z3ErrorModelAndLabels> boogieErrors,
+        out List<int> unsatCore) {
+      Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
+      boogieErrors = new List<Z3ErrorModelAndLabels>();
+      unsatCore = new List<int>();
+      LBool outcome = LBool.Undef;
+
+      Z3Model z3Model;
+      Term proof;
+      Term[] core;
+      Term[] assumption_terms = new Term[assumptions.Count];
+      var logstring = "";
+      for (int i = 0; i < assumptions.Count; i++) {
+        Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+        Term z3ast = (Term)assumptions[i].Accept(visitor, linOptions);
+        assumption_terms[i] = z3ast;
+        logstring += string.Format("({0}) ", assumption_terms[i]);
+      }
+
+      log("(get-core {0})", logstring);
+      outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);
+
+      if (outcome != LBool.False) {
+        Debug.Assert(z3Model != null);
+        LabeledLiterals labels = z3.GetRelevantLabels();
+        Debug.Assert(labels != null);
+
+        List<string> labelStrings = new List<string>();
+        uint numLabels = labels.GetNumLabels();
+        for (uint i = 0; i < numLabels; ++i) {
+          Symbol sym = labels.GetLabel(i);
+          string labelName = z3.GetSymbolString(sym);
+          if (!labelName.StartsWith("@")) {
+            labels.Disable(i);
+          }
+          labelStrings.Add(labelName);
+        }
+
+        var sw = new StringWriter();
+        sw.WriteLine("*** MODEL");
+        z3Model.Display(sw);
+        sw.WriteLine("*** END_MODEL");
+        var sr = new StringReader(sw.ToString());
+        var models = Microsoft.Boogie.Model.ParseModels(sr);
+        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
+        boogieErrors.Add(e);
+
+        labels.Dispose();
+        z3Model.Dispose();
+      }
+
+      if (boogieErrors.Count > 0) {
+        return ProverInterface.Outcome.Invalid;
+      }
+      else if (outcome == LBool.False) {
+        foreach (Term t in core) {
+          for (int i = 0; i < assumption_terms.Length; i++) {
+            if (t.Equals(assumption_terms[i]))
+              unsatCore.Add(i);
+          }
+        }
+        return ProverInterface.Outcome.Valid;
+      }
+      else {
+        Debug.Assert(outcome == LBool.Undef);
+        return ProverInterface.Outcome.Undetermined;
+      }
+    }
+
+    private Symbol GetSymbol(string symbolName) {
+      if (!symbols.ContainsKey(symbolName)) {
+        Symbol symbolAst = z3.MkSymbol(symbolName);
+        symbols.Add(symbolName, symbolAst);
+      }
+      Symbol result;
+      if (!symbols.TryGetValue(symbolName, out result))
+        throw new Exception("symbol " + symbolName + " is undefined");
+      return result;
+    }
+
+    public Term GetConstant(string constantName, Type constantType, VCExpr node)
+    {
+      Term typeSafeTerm;
+      if (!constants.ContainsKey(constantName))
+        this.DeclareConstant(constantName, constantType);
+
+      if (!constants.TryGetValue(constantName, out typeSafeTerm))
+        throw new Exception("constant " + constantName + " is not defined");
+
+      if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm))
+          constants_inv.Add(typeSafeTerm, node);
+
+      return typeSafeTerm;
+    }
+
+    public FuncDecl GetFunction(string functionName) {
+      FuncDecl f;
+      if (!functions.TryGetValue(functionName, out f))
+        throw new Exception("function " + functionName + " is undefined");
+      return f;
+    }
+
+    public Term MakeLabel(string labelName, bool pos, Term child) {
+      Symbol labelSymbol = this.GetSymbol(labelName);
+      Term labeledExpr = z3.MkLabel(labelSymbol, pos, child);
+      labels.Add(labelName, labeledExpr);
+      return labeledExpr;
+    }
+
+    public LabeledLiterals GetRelevantLabels() {
+      LabeledLiterals safeLiterals = z3.GetRelevantLabels();
+      log("get-relevant-labels");
+      return safeLiterals;
+    }
+  }
+
+  internal class BacktrackDictionary<K, V> {
+    private Dictionary<K, V> dictionary = new Dictionary<K, V>();
+    private Stack<List<K>> keyStack = new Stack<List<K>>();
+
+    public BacktrackDictionary() {
+      CreateBacktrackPoint();
+    }
+
+    public bool TryGetValue(K key, out V val) {
+      return dictionary.TryGetValue(key, out val);
+    }
+
+    public void Add(K key, V v) {
+      if (dictionary.ContainsKey(key)) {
+        dictionary.Remove(key);
+      }
+      dictionary.Add(key, v);
+      keyStack.Peek().Add(key);
+    }
+
+    public bool ContainsKey(K k) {
+      return dictionary.ContainsKey(k);
+    }
+
+    public void CreateBacktrackPoint() {
+      keyStack.Push(new List<K>());
+    }
+
+    public void Backtrack() {
+      List<K> keysToErase = keyStack.Pop();
+      foreach (K key in keysToErase) {
+        dictionary.Remove(key);
+      }
+      if (keyStack.Count == 0)
+        this.CreateBacktrackPoint();
+    }
+
+    public IEnumerator GetEnumerator() {
+      return dictionary.Keys.GetEnumerator();
+    }
+  }
+
+  public class Z3ErrorModelAndLabels {
+    private Model _model;
+    private List<string> _relevantLabels;
+    public Model Model {
+      get { return this._model; }
+    }
+    public List<string> RelevantLabels {
+      get { return this._relevantLabels; }
+    }
+    public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) {
+      this._model = model;
+      this._relevantLabels = relevantLabels;
+    }
+  }
+
+
+
 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index d72705f3..cb7df8d7 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -1,354 +1,354 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Threading;

-using System.IO;

-using System.Diagnostics;

-using Microsoft.Boogie.AbstractInterpretation;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Z3;

-using Microsoft.Boogie.VCExprAST;

-using System.Diagnostics.Contracts;

-

-using TypeAst = System.IntPtr;

-using TermAst = System.IntPtr;

-using ConstDeclAst = System.IntPtr;

-using ConstAst = System.IntPtr;

-using Value = System.IntPtr;

-using PatternAst = System.IntPtr;

-

-namespace Microsoft.Boogie.Z3

-{

-  public class Z3InstanceOptions : ProverOptions {

-    public int Timeout { get { return TimeLimit / 1000; } }

-    public int Lets {

-      get {

-        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);

-        return CommandLineOptions.Clo.Z3lets;

-      }

-    }

-    public bool DistZ3 = false;

-    public string ExeName = "z3.exe";

-    public bool InverseImplies = false;

-    public string Inspector = null;

-    public bool OptimizeForBv = false;

-

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(ExeName != null);

-    }

-

-    protected override bool Parse(string opt) {

-      //Contract.Requires(opt!=null);

-      return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||

-             ParseString(opt, "INSPECTOR", ref Inspector) ||

-             ParseBool(opt, "DIST", ref DistZ3) ||

-             ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||

-             base.Parse(opt);

-    }

-

-    public override void PostParse() {

-      base.PostParse();

-

-      if (DistZ3) {

-        ExeName = "z3-dist.exe";

-        CommandLineOptions.Clo.RestartProverPerVC = true;

-      }

-    }

-

-    public override string Help {

-      get {

-        return

-@"

-Z3-specific options:

-~~~~~~~~~~~~~~~~~~~~

-INSPECTOR=<string>        Use the specified Z3Inspector binary.

-OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.

-

-Obscure options:

-~~~~~~~~~~~~~~~~

-DIST=<bool>               Use z3-dist.exe binary.

-REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.

-

-" + base.Help;

-        // DIST requires non-public binaries

-      }

-    }

-  }

-

-  public class Z3LineariserOptions : LineariserOptions {

-    private readonly Z3InstanceOptions opts;

-

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(opts != null);

-    }

-

-

-    public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables)

-      : base(asTerm) {

-      Contract.Requires(opts != null);

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

-

-      this.opts = opts;

-      this.LetVariablesAttr = letVariables;

-    }

-

-    public override bool UseWeights {

-      get {

-        return true;

-      }

-    }

-

-    public override bool UseTypes {

-      get {

-        return true;

-      }

-    }

-

-    public override bool QuantifierIds {

-      get {

-        return true;

-      }

-    }

-

-    public override bool InverseImplies {

-      get {

-        return opts.InverseImplies;

-      }

-    }

-

-    public override LineariserOptions SetAsTerm(bool newVal) {

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

-

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

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

-

-        return LetVariablesAttr;

-      }

-    }

-

-    public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {

-      //Contract.Requires(furtherVar != null);

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

-

-      List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();

-      allVars.AddRange(LetVariables);

-      allVars.Add(furtherVar);

-      return new Z3LineariserOptions(AsTerm, opts, allVars);

-    }

-

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

-      //Contract.Requires(furtherVars != null);

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

-

-      List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();

-      allVars.AddRange(LetVariables);

-      allVars.AddRange(furtherVars);

-      return new Z3LineariserOptions(AsTerm, opts, allVars);

-    }

-  }

-

-    public class Z3apiProcessTheoremProver : ProverInterface

-    {

-        public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)

-        {

-            this.options = opts;

-            this.context = (Z3apiProverContext) ctxt;

-            this.numAxiomsPushed = 0;

-        }

-

-        private Z3InstanceOptions options;

-

-        private Z3apiProverContext context;

-        public override ProverContext Context

-        {

-            get { return context; }

-        }

-

-        public override VCExpressionGenerator VCExprGen

-        {

-            get { return context.ExprGen; }

-        }

-

-        private int numAxiomsPushed;

-

-        public override void Close()

-        {

-            base.Close();

-            context.CloseLog();

-            context.z3.Dispose();

-            context.config.Dispose();

-        }

-

-        public void PushAxiom(VCExpr axiom)

-        {

-            context.CreateBacktrackPoint();

-            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            context.AddAxiom(axiom, linOptions);

-        }

-

-        private void PushConjecture(VCExpr conjecture)

-        {

-            context.CreateBacktrackPoint();

-            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            context.AddConjecture(conjecture, linOptions);

-        }

-

-        public override void PushVCExpression(VCExpr vc)

-        {

-            PushAxiom(vc);

-            numAxiomsPushed++;

-        }

-

-        public void CreateBacktrackPoint()

-        {

-            context.CreateBacktrackPoint();

-        }

-

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

-        {

-            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            Push();

-            context.AddAxiom(context.Axioms, linOptions);

-            context.AddConjecture(vc, linOptions);

-            outcome = context.Check(out z3LabelModels);

-            Pop();

-        }

-  

-        public override void Check()

-        {

-            outcome = context.Check(out z3LabelModels);

-        }

-

-        public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)

-        {

-            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);

-        }

-

-        public override void Push()

-        {

-            context.CreateBacktrackPoint();

-        }

-

-        public override void Pop()

-        {

-            context.Backtrack();

-        }

-

-        public override void Assert(VCExpr vc, bool polarity)

-        {

-            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            if (polarity)

-                context.AddAxiom(vc, linOptions);

-            else

-                context.AddConjecture(vc, linOptions);

-        }

-

-        public override void AssertAxioms()

-        {

-            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            context.AddAxiom(context.Axioms, linOptions);

-        }

-

-        // Number of axioms pushed since the last call to FlushAxioms

-        public override int NumAxiomsPushed()

-        {

-            return numAxiomsPushed;

-        }

-

-        public override int FlushAxiomsToTheoremProver()

-        {

-            var ret = numAxiomsPushed;

-            numAxiomsPushed = 0;

-            return ret;

-        }

-

-        private Outcome outcome;

-        private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();

-

-        [NoDefaultContract]

-        public override Outcome CheckOutcome(ErrorHandler handler)

-        {

-            if (outcome == Outcome.Invalid)

-            {

-                foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)

-                {

-                    List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);

-                    handler.OnModel(unprefixedLabels, z3LabelModel.Model);

-                }

-            }

-            return outcome;

-        }

-

-        public override Outcome CheckOutcomeCore(ErrorHandler handler) {

-          if (outcome == Outcome.Invalid) {

-            foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {

-              List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);

-              handler.OnModel(unprefixedLabels, z3LabelModel.Model);

-            }

-          }

-          return outcome;

-        }

-

-        private List<string> RemovePrefixes(List<string> labels)

-        {

-            List<string> result = new List<string>();

-            foreach (string label in labels)

-            {

-                if (label.StartsWith("+"))

-                {

-                    result.Add(label.Substring(1));

-                }

-                else if (label.StartsWith("|"))

-                {

-                    result.Add(label.Substring(1));

-                }

-                else if (label.StartsWith("@"))

-                {

-                    result.Add(label.Substring(1));

-                }

-                else

-                    throw new Exception("Unknown prefix in label " + label);

-            }

-            return result;

-        }

-    }

-}

-

-namespace Microsoft.Boogie.Z3api

-{

-    public class Factory : ProverFactory

-    {

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

-        {

-            return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt);

-        }

-

-        public override object NewProverContext(ProverOptions opts)

-        {

-            if (CommandLineOptions.Clo.BracketIdsInVC < 0)

-            {

-                CommandLineOptions.Clo.BracketIdsInVC = 0;

-            }

-

-            VCExpressionGenerator gen = new VCExpressionGenerator();

-            return new Z3apiProverContext((Z3InstanceOptions)opts, gen);

-        }

-

-        public override ProverOptions BlankProverOptions()

-        {

-            return new Z3InstanceOptions();

-        }

-    }

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Boogie.VCExprAST;
+using System.Diagnostics.Contracts;
+
+using TypeAst = System.IntPtr;
+using TermAst = System.IntPtr;
+using ConstDeclAst = System.IntPtr;
+using ConstAst = System.IntPtr;
+using Value = System.IntPtr;
+using PatternAst = System.IntPtr;
+
+namespace Microsoft.Boogie.Z3
+{
+  public class Z3InstanceOptions : ProverOptions {
+    public int Timeout { get { return TimeLimit / 1000; } }
+    public int Lets {
+      get {
+        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
+        return CommandLineOptions.Clo.Z3lets;
+      }
+    }
+    public bool DistZ3 = false;
+    public string ExeName = "z3.exe";
+    public bool InverseImplies = false;
+    public string Inspector = null;
+    public bool OptimizeForBv = false;
+
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(ExeName != null);
+    }
+
+    protected override bool Parse(string opt) {
+      //Contract.Requires(opt!=null);
+      return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
+             ParseString(opt, "INSPECTOR", ref Inspector) ||
+             ParseBool(opt, "DIST", ref DistZ3) ||
+             ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
+             base.Parse(opt);
+    }
+
+    public override void PostParse() {
+      base.PostParse();
+
+      if (DistZ3) {
+        ExeName = "z3-dist.exe";
+        CommandLineOptions.Clo.RestartProverPerVC = true;
+      }
+    }
+
+    public override string Help {
+      get {
+        return
+@"
+Z3-specific options:
+~~~~~~~~~~~~~~~~~~~~
+INSPECTOR=<string>        Use the specified Z3Inspector binary.
+OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
+
+Obscure options:
+~~~~~~~~~~~~~~~~
+DIST=<bool>               Use z3-dist.exe binary.
+REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
+
+" + base.Help;
+        // DIST requires non-public binaries
+      }
+    }
+  }
+
+  public class Z3LineariserOptions : LineariserOptions {
+    private readonly Z3InstanceOptions opts;
+
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(opts != null);
+    }
+
+
+    public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables)
+      : base(asTerm) {
+      Contract.Requires(opts != null);
+      Contract.Requires(cce.NonNullElements(letVariables));
+
+      this.opts = opts;
+      this.LetVariablesAttr = letVariables;
+    }
+
+    public override bool UseWeights {
+      get {
+        return true;
+      }
+    }
+
+    public override bool UseTypes {
+      get {
+        return true;
+      }
+    }
+
+    public override bool QuantifierIds {
+      get {
+        return true;
+      }
+    }
+
+    public override bool InverseImplies {
+      get {
+        return opts.InverseImplies;
+      }
+    }
+
+    public override LineariserOptions SetAsTerm(bool newVal) {
+      Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+      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 {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
+
+        return LetVariablesAttr;
+      }
+    }
+
+    public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {
+      //Contract.Requires(furtherVar != null);
+      Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+      List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
+      allVars.AddRange(LetVariables);
+      allVars.Add(furtherVar);
+      return new Z3LineariserOptions(AsTerm, opts, allVars);
+    }
+
+    public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {
+      //Contract.Requires(furtherVars != null);
+      Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+      List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
+      allVars.AddRange(LetVariables);
+      allVars.AddRange(furtherVars);
+      return new Z3LineariserOptions(AsTerm, opts, allVars);
+    }
+  }
+
+    public class Z3apiProcessTheoremProver : ProverInterface
+    {
+        public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)
+        {
+            this.options = opts;
+            this.context = (Z3apiProverContext) ctxt;
+            this.numAxiomsPushed = 0;
+        }
+
+        private Z3InstanceOptions options;
+
+        private Z3apiProverContext context;
+        public override ProverContext Context
+        {
+            get { return context; }
+        }
+
+        public override VCExpressionGenerator VCExprGen
+        {
+            get { return context.ExprGen; }
+        }
+
+        private int numAxiomsPushed;
+
+        public override void Close()
+        {
+            base.Close();
+            context.CloseLog();
+            context.z3.Dispose();
+            context.config.Dispose();
+        }
+
+        public void PushAxiom(VCExpr axiom)
+        {
+            context.CreateBacktrackPoint();
+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+            context.AddAxiom(axiom, linOptions);
+        }
+
+        private void PushConjecture(VCExpr conjecture)
+        {
+            context.CreateBacktrackPoint();
+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+            context.AddConjecture(conjecture, linOptions);
+        }
+
+        public override void PushVCExpression(VCExpr vc)
+        {
+            PushAxiom(vc);
+            numAxiomsPushed++;
+        }
+
+        public void CreateBacktrackPoint()
+        {
+            context.CreateBacktrackPoint();
+        }
+
+        public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
+        {
+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+            Push();
+            context.AddAxiom(context.Axioms, linOptions);
+            context.AddConjecture(vc, linOptions);
+            outcome = context.Check(out z3LabelModels);
+            Pop();
+        }
+  
+        public override void Check()
+        {
+            outcome = context.Check(out z3LabelModels);
+        }
+
+        public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
+        {
+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+            return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
+        }
+
+        public override void Push()
+        {
+            context.CreateBacktrackPoint();
+        }
+
+        public override void Pop()
+        {
+            context.Backtrack();
+        }
+
+        public override void Assert(VCExpr vc, bool polarity)
+        {
+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+            if (polarity)
+                context.AddAxiom(vc, linOptions);
+            else
+                context.AddConjecture(vc, linOptions);
+        }
+
+        public override void AssertAxioms()
+        {
+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+            context.AddAxiom(context.Axioms, linOptions);
+        }
+
+        // Number of axioms pushed since the last call to FlushAxioms
+        public override int NumAxiomsPushed()
+        {
+            return numAxiomsPushed;
+        }
+
+        public override int FlushAxiomsToTheoremProver()
+        {
+            var ret = numAxiomsPushed;
+            numAxiomsPushed = 0;
+            return ret;
+        }
+
+        private Outcome outcome;
+        private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();
+
+        [NoDefaultContract]
+        public override Outcome CheckOutcome(ErrorHandler handler)
+        {
+            if (outcome == Outcome.Invalid)
+            {
+                foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
+                {
+                    List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
+                    handler.OnModel(unprefixedLabels, z3LabelModel.Model);
+                }
+            }
+            return outcome;
+        }
+
+        public override Outcome CheckOutcomeCore(ErrorHandler handler) {
+          if (outcome == Outcome.Invalid) {
+            foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {
+              List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
+              handler.OnModel(unprefixedLabels, z3LabelModel.Model);
+            }
+          }
+          return outcome;
+        }
+
+        private List<string> RemovePrefixes(List<string> labels)
+        {
+            List<string> result = new List<string>();
+            foreach (string label in labels)
+            {
+                if (label.StartsWith("+"))
+                {
+                    result.Add(label.Substring(1));
+                }
+                else if (label.StartsWith("|"))
+                {
+                    result.Add(label.Substring(1));
+                }
+                else if (label.StartsWith("@"))
+                {
+                    result.Add(label.Substring(1));
+                }
+                else
+                    throw new Exception("Unknown prefix in label " + label);
+            }
+            return result;
+        }
+    }
+}
+
+namespace Microsoft.Boogie.Z3api
+{
+    public class Factory : ProverFactory
+    {
+        public override object SpawnProver(ProverOptions options, object ctxt)
+        {
+            return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt);
+        }
+
+        public override object NewProverContext(ProverOptions opts)
+        {
+            if (CommandLineOptions.Clo.BracketIdsInVC < 0)
+            {
+                CommandLineOptions.Clo.BracketIdsInVC = 0;
+            }
+
+            VCExpressionGenerator gen = new VCExpressionGenerator();
+            return new Z3apiProverContext((Z3InstanceOptions)opts, gen);
+        }
+
+        public override ProverOptions BlankProverOptions()
+        {
+            return new Z3InstanceOptions();
+        }
+    }
 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 72192804..b83d6dff 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -1,16 +1,16 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Threading;

-using System.IO;

-using System.Diagnostics;

-using Microsoft.Boogie.AbstractInterpretation;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Z3;

-using Microsoft.Z3;

-using Microsoft.Boogie.VCExprAST;

-

-namespace Microsoft.Boogie.Z3

-{

-   

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+   
 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index b129b378..79f140aa 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -1,75 +1,75 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Threading;

-using System.IO;

-using System.Diagnostics;

-using Microsoft.Boogie.AbstractInterpretation;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Z3;

-using Microsoft.Z3;

-using Microsoft.Boogie.VCExprAST;

-

-namespace Microsoft.Boogie.Z3 {

-  public class Z3StubContext : Z3Context {

-    class Z3StubPatternAst: Z3PatternAst {}

-    class Z3StubTermAst: Z3TermAst {}

-    class Z3StubLabeledLiterals: Z3LabeledLiterals {}

-  

-    public void CreateBacktrackPoint(){}

-    public void Backtrack(){}

-    public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) { }

-    public void AddConjecture(VCExpr vc, LineariserOptions linOptions){}

-    public void AddSmtlibString(string smtlibString) {}

-    public string GetDeclName(Z3ConstDeclAst constDeclAst) {

-      return "";

-    }

-    public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {

-      return new Z3StubPatternAst();

-    }

-    public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

-        return new Z3StubTermAst();

-    }

-    public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {

-      boogieErrors = new List<Z3ErrorModelAndLabels>();

-      return ProverInterface.Outcome.Undetermined;

-    }

-    public void TypeCheckBool(Z3TermAst t){}

-    public void TypeCheckInt(Z3TermAst t){}

-    public void DeclareType(string typeName) {}

-    public void DeclareConstant(string constantName, Type boogieType) {}

-    public void DeclareFunction(string functionName, List<Type> domain, Type range) {}

-    public Z3TermAst GetConstant(string constantName, Type constantType) {

-      return new Z3StubTermAst();

-    }    

-    public Z3TermAst MakeIntLiteral(string numeral) {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeBvLiteral(int i, uint bvSize) {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeTrue() {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeFalse() {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) {

-      return new Z3StubTermAst();

-    }

-    public Z3LabeledLiterals GetRelevantLabels() {

-      return new Z3StubLabeledLiterals();

-    }

-    public Z3TermAst Make(string op, List<Z3TermAst> children) {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeArraySelect(List<Z3TermAst> args)

-    {

-        return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeArrayStore(List<Z3TermAst> args)

-    {

-        return new Z3StubTermAst();

-    }

-  }

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3 {
+  public class Z3StubContext : Z3Context {
+    class Z3StubPatternAst: Z3PatternAst {}
+    class Z3StubTermAst: Z3TermAst {}
+    class Z3StubLabeledLiterals: Z3LabeledLiterals {}
+  
+    public void CreateBacktrackPoint(){}
+    public void Backtrack(){}
+    public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) { }
+    public void AddConjecture(VCExpr vc, LineariserOptions linOptions){}
+    public void AddSmtlibString(string smtlibString) {}
+    public string GetDeclName(Z3ConstDeclAst constDeclAst) {
+      return "";
+    }
+    public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {
+      return new Z3StubPatternAst();
+    }
+    public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {
+        return new Z3StubTermAst();
+    }
+    public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {
+      boogieErrors = new List<Z3ErrorModelAndLabels>();
+      return ProverInterface.Outcome.Undetermined;
+    }
+    public void TypeCheckBool(Z3TermAst t){}
+    public void TypeCheckInt(Z3TermAst t){}
+    public void DeclareType(string typeName) {}
+    public void DeclareConstant(string constantName, Type boogieType) {}
+    public void DeclareFunction(string functionName, List<Type> domain, Type range) {}
+    public Z3TermAst GetConstant(string constantName, Type constantType) {
+      return new Z3StubTermAst();
+    }    
+    public Z3TermAst MakeIntLiteral(string numeral) {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeBvLiteral(int i, uint bvSize) {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeTrue() {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeFalse() {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) {
+      return new Z3StubTermAst();
+    }
+    public Z3LabeledLiterals GetRelevantLabels() {
+      return new Z3StubLabeledLiterals();
+    }
+    public Z3TermAst Make(string op, List<Z3TermAst> children) {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeArraySelect(List<Z3TermAst> args)
+    {
+        return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeArrayStore(List<Z3TermAst> args)
+    {
+        return new Z3StubTermAst();
+    }
+  }
 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index 879211f7..f2a9a8fd 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -1,197 +1,197 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Threading;

-using System.IO;

-using System.Diagnostics;

-using Microsoft.Boogie.AbstractInterpretation;

-using Microsoft.Boogie;

-using Microsoft.Boogie.Z3;

-using Microsoft.Z3;

-using Microsoft.Boogie.VCExprAST;

-

-namespace Microsoft.Boogie.Z3

-{

-    internal class Z3TypeCachedBuilder

-    {

-        private class MapTypeComparator : IEqualityComparer<MapType>

-        {

-            public bool Equals(MapType x, MapType y)

-            {

-                if (x.MapArity != y.MapArity)

-                    return false;

-                for (int i = 0; i < x.MapArity; i++)

-                {

-                    if (!Equals(x.Arguments[i], y.Arguments[i]))

-                        return false;

-                }

-                return Equals(x.Result, y.Result);

-

-            }

-            public int GetHashCode(MapType mapType)

-            {

-                return mapType.GetHashCode();

-            }

-        }

-

-        private class BvTypeComparator : IEqualityComparer<BvType>

-        {

-            public bool Equals(BvType x, BvType y)

-            {

-                return x.Bits == y.Bits;

-            }

-            public int GetHashCode(BvType bvType)

-            {

-                return bvType.Bits;

-            }

-        }

-

-        private class BasicTypeComparator : IEqualityComparer<BasicType>

-        {

-            public bool Equals(BasicType x, BasicType y)

-            {

-                return (x.IsBool == y.IsBool) &&

-                       (x.IsInt == y.IsInt) &&

-                       (x.IsReal == y.IsReal);

-            }

-

-            public int GetHashCode(BasicType basicType)

-            {

-                if (basicType.IsBool)

-                    return 1;

-                else if (basicType.IsInt)

-                    return 2;

-                else if (basicType.IsReal)

-                  return 3;

-                else

-                    throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");

-            }

-        }

-

-        private class CtorTypeComparator : IEqualityComparer<CtorType> {

-          public bool Equals(CtorType x, CtorType y) {

-            return (x.Decl.Name == y.Decl.Name);

-          }

-

-          public int GetHashCode(CtorType ctorType) {

-            return ctorType.Decl.Name.GetHashCode();

-          }

-        }

-

-        private Dictionary<MapType, Sort> mapTypes = new Dictionary<MapType, Sort>(new MapTypeComparator());

-        private Dictionary<BvType, Sort> bvTypes = new Dictionary<BvType, Sort>(new BvTypeComparator());

-        private Dictionary<BasicType, Sort> basicTypes = new Dictionary<BasicType, Sort>(new BasicTypeComparator());

-        private Dictionary<CtorType, Sort> ctorTypes = new Dictionary<CtorType, Sort>(new CtorTypeComparator());

-

-        private Z3apiProverContext container;

-

-        public Z3TypeCachedBuilder(Z3apiProverContext context)

-        {

-            this.container = context;

-        }

-

-        private Sort GetMapType(MapType mapType) {

-          Context z3 = ((Z3apiProverContext)container).z3;

-          if (!mapTypes.ContainsKey(mapType)) {

-            Type result = mapType.Result;

-            for (int i = mapType.Arguments.Length-1; i > 0; i--) {

-              GetType(result);

-              result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result);

-            }

-            mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result)));

-          }

-          return mapTypes[mapType];

-        }

-

-        private Sort GetBvType(BvType bvType)

-        {

-            if (!bvTypes.ContainsKey(bvType))

-            {

-                Sort typeAst = BuildBvType(bvType);

-                bvTypes.Add(bvType, typeAst);

-            }

-            Sort result;

-            bool containsKey = bvTypes.TryGetValue(bvType, out result);

-            Debug.Assert(containsKey);

-            return result;

-        }

-

-        private Sort GetBasicType(BasicType basicType)

-        {

-            if (!basicTypes.ContainsKey(basicType))

-            {

-                Sort typeAst = BuildBasicType(basicType);

-                basicTypes.Add(basicType, typeAst);

-            }

-            Sort result;

-            bool containsKey = basicTypes.TryGetValue(basicType, out result);

-            Debug.Assert(containsKey);

-            return result;

-        }

-

-        private Sort GetCtorType(CtorType ctorType) {

-          if (!ctorTypes.ContainsKey(ctorType)) {

-            Sort typeAst = BuildCtorType(ctorType);

-            ctorTypes.Add(ctorType, typeAst);

-          }

-          Sort result;

-          bool containsKey = ctorTypes.TryGetValue(ctorType, out result);

-          Debug.Assert(containsKey);

-          return result;

-        }

-

-        public virtual Sort GetType(Type boogieType) {

-          System.Type type = boogieType.GetType();

-          if (type.Equals(typeof(BvType)))

-            return GetBvType((BvType)boogieType);

-          else if (type.Equals(typeof(BasicType)))

-            return GetBasicType((BasicType)boogieType);

-          else if (type.Equals(typeof(MapType)))

-            return GetMapType((MapType)boogieType);

-          else if (type.Equals(typeof(CtorType)))

-            return GetCtorType((CtorType)boogieType);

-          else

-            throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");

-        }

-

-        public Sort BuildMapType(Sort domain, Sort range)

-        {

-            Context z3 = ((Z3apiProverContext)container).z3;

-            return z3.MkArraySort(domain, range);

-        }

-

-        public Sort BuildBvType(BvType bvType)

-        {

-            Context z3 = ((Z3apiProverContext)container).z3;

-            return z3.MkBvSort((uint)bvType.Bits);

-        }

-

-        public Sort BuildBasicType(BasicType basicType)

-        {

-            Context z3 = ((Z3apiProverContext)container).z3;

-            Sort typeAst;

-            if (basicType.IsBool)

-            {

-                typeAst = z3.MkBoolSort();

-            }

-            else if (basicType.IsInt)

-            {

-                typeAst = z3.MkIntSort();

-            }

-            else if (basicType.IsReal)

-            {

-                typeAst = z3.MkRealSort();

-            }

-            else

-                throw new Exception("Unknown Basic Type " + basicType.ToString());

-            return typeAst;

-        }

-

-        public Sort BuildCtorType(CtorType ctorType) {

-          Context z3 = ((Z3apiProverContext)container).z3;

-          if (ctorType.Arguments.Length > 0)

-            throw new Exception("Type constructor of non-zero arity are not handled");

-          return z3.MkSort(ctorType.Decl.Name);

-        }

-    }

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+    internal class Z3TypeCachedBuilder
+    {
+        private class MapTypeComparator : IEqualityComparer<MapType>
+        {
+            public bool Equals(MapType x, MapType y)
+            {
+                if (x.MapArity != y.MapArity)
+                    return false;
+                for (int i = 0; i < x.MapArity; i++)
+                {
+                    if (!Equals(x.Arguments[i], y.Arguments[i]))
+                        return false;
+                }
+                return Equals(x.Result, y.Result);
+
+            }
+            public int GetHashCode(MapType mapType)
+            {
+                return mapType.GetHashCode();
+            }
+        }
+
+        private class BvTypeComparator : IEqualityComparer<BvType>
+        {
+            public bool Equals(BvType x, BvType y)
+            {
+                return x.Bits == y.Bits;
+            }
+            public int GetHashCode(BvType bvType)
+            {
+                return bvType.Bits;
+            }
+        }
+
+        private class BasicTypeComparator : IEqualityComparer<BasicType>
+        {
+            public bool Equals(BasicType x, BasicType y)
+            {
+                return (x.IsBool == y.IsBool) &&
+                       (x.IsInt == y.IsInt) &&
+                       (x.IsReal == y.IsReal);
+            }
+
+            public int GetHashCode(BasicType basicType)
+            {
+                if (basicType.IsBool)
+                    return 1;
+                else if (basicType.IsInt)
+                    return 2;
+                else if (basicType.IsReal)
+                  return 3;
+                else
+                    throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");
+            }
+        }
+
+        private class CtorTypeComparator : IEqualityComparer<CtorType> {
+          public bool Equals(CtorType x, CtorType y) {
+            return (x.Decl.Name == y.Decl.Name);
+          }
+
+          public int GetHashCode(CtorType ctorType) {
+            return ctorType.Decl.Name.GetHashCode();
+          }
+        }
+
+        private Dictionary<MapType, Sort> mapTypes = new Dictionary<MapType, Sort>(new MapTypeComparator());
+        private Dictionary<BvType, Sort> bvTypes = new Dictionary<BvType, Sort>(new BvTypeComparator());
+        private Dictionary<BasicType, Sort> basicTypes = new Dictionary<BasicType, Sort>(new BasicTypeComparator());
+        private Dictionary<CtorType, Sort> ctorTypes = new Dictionary<CtorType, Sort>(new CtorTypeComparator());
+
+        private Z3apiProverContext container;
+
+        public Z3TypeCachedBuilder(Z3apiProverContext context)
+        {
+            this.container = context;
+        }
+
+        private Sort GetMapType(MapType mapType) {
+          Context z3 = ((Z3apiProverContext)container).z3;
+          if (!mapTypes.ContainsKey(mapType)) {
+            Type result = mapType.Result;
+            for (int i = mapType.Arguments.Length-1; i > 0; i--) {
+              GetType(result);
+              result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result);
+            }
+            mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result)));
+          }
+          return mapTypes[mapType];
+        }
+
+        private Sort GetBvType(BvType bvType)
+        {
+            if (!bvTypes.ContainsKey(bvType))
+            {
+                Sort typeAst = BuildBvType(bvType);
+                bvTypes.Add(bvType, typeAst);
+            }
+            Sort result;
+            bool containsKey = bvTypes.TryGetValue(bvType, out result);
+            Debug.Assert(containsKey);
+            return result;
+        }
+
+        private Sort GetBasicType(BasicType basicType)
+        {
+            if (!basicTypes.ContainsKey(basicType))
+            {
+                Sort typeAst = BuildBasicType(basicType);
+                basicTypes.Add(basicType, typeAst);
+            }
+            Sort result;
+            bool containsKey = basicTypes.TryGetValue(basicType, out result);
+            Debug.Assert(containsKey);
+            return result;
+        }
+
+        private Sort GetCtorType(CtorType ctorType) {
+          if (!ctorTypes.ContainsKey(ctorType)) {
+            Sort typeAst = BuildCtorType(ctorType);
+            ctorTypes.Add(ctorType, typeAst);
+          }
+          Sort result;
+          bool containsKey = ctorTypes.TryGetValue(ctorType, out result);
+          Debug.Assert(containsKey);
+          return result;
+        }
+
+        public virtual Sort GetType(Type boogieType) {
+          System.Type type = boogieType.GetType();
+          if (type.Equals(typeof(BvType)))
+            return GetBvType((BvType)boogieType);
+          else if (type.Equals(typeof(BasicType)))
+            return GetBasicType((BasicType)boogieType);
+          else if (type.Equals(typeof(MapType)))
+            return GetMapType((MapType)boogieType);
+          else if (type.Equals(typeof(CtorType)))
+            return GetCtorType((CtorType)boogieType);
+          else
+            throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
+        }
+
+        public Sort BuildMapType(Sort domain, Sort range)
+        {
+            Context z3 = ((Z3apiProverContext)container).z3;
+            return z3.MkArraySort(domain, range);
+        }
+
+        public Sort BuildBvType(BvType bvType)
+        {
+            Context z3 = ((Z3apiProverContext)container).z3;
+            return z3.MkBvSort((uint)bvType.Bits);
+        }
+
+        public Sort BuildBasicType(BasicType basicType)
+        {
+            Context z3 = ((Z3apiProverContext)container).z3;
+            Sort typeAst;
+            if (basicType.IsBool)
+            {
+                typeAst = z3.MkBoolSort();
+            }
+            else if (basicType.IsInt)
+            {
+                typeAst = z3.MkIntSort();
+            }
+            else if (basicType.IsReal)
+            {
+                typeAst = z3.MkRealSort();
+            }
+            else
+                throw new Exception("Unknown Basic Type " + basicType.ToString());
+            return typeAst;
+        }
+
+        public Sort BuildCtorType(CtorType ctorType) {
+          Context z3 = ((Z3apiProverContext)container).z3;
+          if (ctorType.Arguments.Length > 0)
+            throw new Exception("Type constructor of non-zero arity are not handled");
+          return z3.MkSort(ctorType.Decl.Name);
+        }
+    }
 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index e56a7950..52c7d8fd 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -1,649 +1,649 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Text;

-using System.IO;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-using Microsoft.Z3;

-

-namespace Microsoft.Boogie.Z3

-{

-    using System.Numerics.BigInteger;

-

-    public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>

-    {

-        private Z3apiOpLineariser opLineariser = null;

-        private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser

-        {

-            get

-            {

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

-                if (opLineariser == null)

-                    opLineariser = new Z3apiOpLineariser(this);

-                return opLineariser;

-            }

-        }

-

-        internal readonly UniqueNamer namer;

-        internal readonly Dictionary<VCExprVar, Term> letBindings;

-        protected Z3apiProverContext cm;

-

-        public Z3apiExprLineariser(Z3apiProverContext cm, UniqueNamer namer)

-        {

-            this.cm = cm;

-            this.namer = namer;

-            this.letBindings = new Dictionary<VCExprVar, Term>();

-        }

-

-        public Term Linearise(VCExpr expr, LineariserOptions options)

-        {

-            Contract.Requires(options != null);

-            Contract.Requires(expr != null);

-            return expr.Accept<Term, LineariserOptions>(this, options);

-        }

-

-        /////////////////////////////////////////////////////////////////////////////////////

-

-        public Term Make(VCExprOp op, List<Term> children) {

-          Context z3 = cm.z3;

-          Term[] unwrapChildren = children.ToArray();

-          VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;

-          if (boogieFunctionOp != null) {

-            FuncDecl f = cm.GetFunction(boogieFunctionOp.Func.Name);

-            return z3.MkApp(f, unwrapChildren);

-          }

-          VCExprDistinctOp distinctOp = op as VCExprDistinctOp;

-          if (distinctOp != null) {

-            return z3.MkDistinct(unwrapChildren);

-          }

-

-          if (op == VCExpressionGenerator.AndOp) {

-            return z3.MkAnd(unwrapChildren);

-          }

-

-          if (op == VCExpressionGenerator.OrOp) {

-            return z3.MkOr(unwrapChildren);

-          }

-

-          if (op == VCExpressionGenerator.ImpliesOp) {

-            return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.NotOp) {

-            return z3.MkNot(unwrapChildren[0]);

-          }

-

-          if (op == VCExpressionGenerator.EqOp) {

-            return z3.MkEq(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.NeqOp) {

-            return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1]));

-          }

-

-          if (op == VCExpressionGenerator.LtOp) {

-            return z3.MkLt(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.LeOp) {

-            return z3.MkLe(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.GtOp) {

-            return z3.MkGt(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.GeOp) {

-            return z3.MkGe(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.AddOp) {

-            return z3.MkAdd(unwrapChildren);

-          }

-

-          if (op == VCExpressionGenerator.SubOp) {

-            return z3.MkSub(unwrapChildren);

-          }

-

-          if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) {

-            return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.MulOp) {

-            return z3.MkMul(unwrapChildren);

-          }

-

-          if (op == VCExpressionGenerator.ModOp) {

-            return z3.MkMod(unwrapChildren[0], unwrapChildren[1]);

-          }

-

-          if (op == VCExpressionGenerator.IfThenElseOp) {

-            return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);

-          }

-

-          if (op == VCExpressionGenerator.ToIntOp) {

-            return z3.MkToInt(unwrapChildren[0]);

-          }

-

-          if (op == VCExpressionGenerator.ToRealOp) {

-            return z3.MkToReal(unwrapChildren[0]);

-          }

-

-          throw new Exception("unhandled boogie operator");

-        }

-

-        public Term Visit(VCExprLiteral node, LineariserOptions options)

-        {

-            Contract.Requires(options != null);

-            Contract.Requires(node != null);

-

-            if (node == VCExpressionGenerator.True)

-                return cm.z3.MkTrue();

-            else if (node == VCExpressionGenerator.False)

-                return cm.z3.MkFalse();

-            else if (node is VCExprIntLit)

-                return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());

-            else if (node is VCExprRealLit) {

-                string m = ((VCExprRealLit)node).Val.Mantissa.ToString();

-                BigInteger e = ((VCExprRealLit)node).Val.Exponent;

-                string f = BigInteger.Pow(10, e.Abs);

-

-                if (e == 0) {

-                    return cm.z3.MkNumeral(m, cm.z3.MkRealSort());

-                }

-                else if (((VCExprRealLit)node).Val.Exponent > 0) {

-                    return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));

-                }

-                else {

-                    return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));

-                }

-            }

-            else {

-              Contract.Assert(false);

-              throw new cce.UnreachableException();

-            }

-        }

-

-        public Term Visit(VCExprNAry node, LineariserOptions options)

-        {

-            Contract.Requires(options != null);

-            Contract.Requires(node != null);

-            VCExprOp op = node.Op;

-            Contract.Assert(op != null);

-

-            if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))

-            {

-                // handle these operators without recursion

-                List<Term> asts = new List<Term>();

-                string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";

-

-                IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

-                Contract.Assert(enumerator != null);

-                while (enumerator.MoveNext())

-                {

-                    VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

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

-                    {

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

-                    }

-                }

-

-                return Make(op, asts);

-            }

-

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

-        }

-

-        public Term Visit(VCExprVar node, LineariserOptions options)

-        {

-            Contract.Requires(options != null);

-            Contract.Requires(node != null);

-            if (letBindings.ContainsKey(node))

-            {

-                return letBindings[node];

-            }

-            else

-            {

-                string varName = namer.GetName(node, node.Name);

-                return cm.GetConstant(varName, node.Type,node);

-            }

-        }

-

-        public Term Visit(VCExprQuantifier node, LineariserOptions options)

-        {

-            Contract.Requires(options != null);

-            Contract.Requires(node != null);

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

-

-            namer.PushScope();

-            try

-            {

-                List<string> varNames;

-                List<Type> varTypes;

-                VisitBounds(node.BoundVars, out varNames, out varTypes);

-                List<Pattern> patterns;

-                List<Term> no_patterns;

-                VisitTriggers(node.Triggers, options, out patterns, out no_patterns);

-                Term body = Linearise(node.Body, options);

-                Term result;

-                uint weight = 1;

-                string qid = "";

-                int skolemid = 0;

-

-                if (options.QuantifierIds)

-                {

-                    VCQuantifierInfos infos = node.Infos;

-                    Contract.Assert(infos != null);

-                    if (infos.qid != null)

-                    {

-                        qid = infos.qid;

-                    }

-                    if (0 <= infos.uniqueId)

-                    {

-                        skolemid = infos.uniqueId;

-                    }

-                }

-

-                if (options.UseWeights)

-                {

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

-                }

-

-                switch (node.Quan)

-                {

-                    case Microsoft.Boogie.VCExprAST.Quantifier.ALL:

-                        result = MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;

-                    case Microsoft.Boogie.VCExprAST.Quantifier.EX:

-                        result = MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;

-                    default:

-                        throw new Exception("unknown quantifier kind " + node.Quan);

-                }

-                return result;

-            }

-            finally

-            {

-                namer.PopScope();

-            }

-        }

-

-        private Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {

-          List<Term> bound = new List<Term>();

-          for (int i = 0; i < varNames.Count; i++) {

-            Term t = cm.GetConstant(varNames[i], boogieTypes[i], null);

-            bound.Add(t);

-          }

-

-          Term termAst = cm.z3.MkQuantifier(isForall, weight, cm.z3.MkSymbol(qid), cm.z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body);

-          return termAst;

-        }

-

-        private void VisitBounds(List<VCExprVar> boundVars, out List<string> varNames, out List<Type> varTypes)

-        {

-            varNames = new List<string>();

-            varTypes = new List<Type>();

-            foreach (VCExprVar var in boundVars)

-            {

-                string varName = namer.GetLocalName(var, var.Name);

-                varNames.Add(varName);

-                varTypes.Add(var.Type);

-            }

-        }

-

-        private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns)

-        {

-            patterns = new List<Pattern>();

-            no_patterns = new List<Term>();

-            foreach (VCTrigger trigger in triggers)

-            {

-                List<Term> exprs = new List<Term>();

-                foreach (VCExpr expr in trigger.Exprs)

-                {

-                    System.Diagnostics.Debug.Assert(expr != null);

-                    Term termAst = Linearise(expr, options);

-                    exprs.Add(termAst);

-                }

-                if (exprs.Count > 0)

-                {

-                  if (trigger.Pos) {

-                    Pattern pattern = cm.z3.MkPattern(exprs.ToArray());

-                    patterns.Add(pattern);

-                  }

-                  else {

-                    System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");

-                    foreach (Term expr in exprs)

-                      no_patterns.Add(expr);

-                  }

-                }

-            }

-        }

-

-        public Term Visit(VCExprLet node, LineariserOptions options)

-        {

-            foreach (VCExprLetBinding b in node)

-            {

-                Term defAst = Linearise(b.E, options);

-                letBindings.Add(b.V, defAst);

-            }

-            Term letAst = Linearise(node.Body, options);

-            foreach (VCExprLetBinding b in node)

-            {

-                letBindings.Remove(b.V);

-            }

-            return letAst;

-        }  

-

-        /////////////////////////////////////////////////////////////////////////////////////

-

-        internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>

-        {

-            [ContractInvariantMethod]

-            void ObjectInvariant()

-            {

-                Contract.Invariant(ExprLineariser != null);

-            }

-

-            private readonly Z3apiExprLineariser ExprLineariser;

-

-            public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser)

-            {

-                Contract.Requires(ExprLineariser != null);

-                this.ExprLineariser = ExprLineariser;

-            }

-

-            ///////////////////////////////////////////////////////////////////////////////////

-

-            private Term WriteApplication(VCExprOp op, IEnumerable<VCExpr> terms, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(op != null);

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

-

-                List<Term> args = new List<Term>();

-                foreach (VCExpr e in terms)

-                {

-                    Contract.Assert(e != null);

-                    args.Add(ExprLineariser.Linearise(e, options));

-                }

-                return ExprLineariser.Make(op, args);

-            }

-

-            ///////////////////////////////////////////////////////////////////////////////////

-

-            public Term VisitNotOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitEqOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitAndOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);  

-            }

-

-            public Term VisitOrOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options); 

-            }

-

-            public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) 

-            {

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-              return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                VCExprLabelOp op = (VCExprLabelOp)node.Op;

-                Contract.Assert(op != null);

-                return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); 

-            }

-

-            public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                List<Term> args = new List<Term>();

-                foreach (VCExpr e in node)

-                {

-                    Contract.Assert(e != null);

-                    args.Add(ExprLineariser.Linearise(e, options));

-                }

-                System.Diagnostics.Debug.Assert(args.Count >= 2);

-

-                Term selectTerm = args[0];

-                for (int i = 1; i < args.Count; i++) {

-                  selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]);

-                }

-                return selectTerm;

-            }

-

-            private Term ConstructStoreTerm(Term mapTerm, List<Term> args, int index) {

-              System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1);

-              if (index == args.Count - 2) {

-                return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]);

-              }

-              else {

-                Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1);

-                return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t);

-              }

-            }

-

-            public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                List<Term> args = new List<Term>();

-                foreach (VCExpr e in node)

-                {

-                    Contract.Assert(e != null);

-                    args.Add(ExprLineariser.Linearise(e, options));

-                }

-                return ConstructStoreTerm(args[0], args, 1);

-            }

-

-            public Term VisitBvOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                List<int> args = new List<int>();

-                foreach (VCExpr e in node) {

-                  VCExprIntLit literal = e as VCExprIntLit;

-                  System.Diagnostics.Debug.Assert(literal != null);

-                  args.Add(literal.Val.ToInt);

-                }

-                System.Diagnostics.Debug.Assert(args.Count == 1);

-                return ExprLineariser.cm.z3.MkNumeral(args[0], ExprLineariser.cm.z3.MkBvSort((uint)node.Type.BvBits));

-            }

-

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

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-

-              VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;

-              Contract.Assert(op != null);

-              System.Diagnostics.Debug.Assert(0 <= op.Start && op.Start < op.End);

-

-              List<Term> args = new List<Term>();

-              foreach (VCExpr e in node) {

-                Contract.Assert(e != null);

-                args.Add(ExprLineariser.Linearise(e, options));

-              }

-              System.Diagnostics.Debug.Assert(args.Count == 1);

-              return ExprLineariser.cm.z3.MkBvExtract((uint) op.End - 1, (uint) op.Start, args[0]);

-            }

-

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

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-

-              VCExprBvConcatOp op = (VCExprBvConcatOp)node.Op;

-              Contract.Assert(op != null);

-

-              List<Term> args = new List<Term>();

-              foreach (VCExpr e in node) {

-                Contract.Assert(e != null);

-                args.Add(ExprLineariser.Linearise(e, options));

-              }

-              System.Diagnostics.Debug.Assert(args.Count == 2);

-              return ExprLineariser.cm.z3.MkBvConcat(args[0], args[1]);

-            }

-

-            public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(node != null);

-                Contract.Requires(options != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

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

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-              return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitSubOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitMulOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitDivOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitModOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) {

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-              return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitPowOp(VCExprNAry node, LineariserOptions options) {

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-              return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitLtOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitLeOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitGtOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitGeOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) {

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-              return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) {

-              Contract.Requires(options != null);

-              Contract.Requires(node != null);

-              return WriteApplication(node.Op, node, options);

-            }

-

-            public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(node.Op, node, options);

-            }

-        }

-    }

-}

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Z3;
+
+namespace Microsoft.Boogie.Z3
+{
+    using System.Numerics.BigInteger;
+
+    public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>
+    {
+        private Z3apiOpLineariser opLineariser = null;
+        private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
+                if (opLineariser == null)
+                    opLineariser = new Z3apiOpLineariser(this);
+                return opLineariser;
+            }
+        }
+
+        internal readonly UniqueNamer namer;
+        internal readonly Dictionary<VCExprVar, Term> letBindings;
+        protected Z3apiProverContext cm;
+
+        public Z3apiExprLineariser(Z3apiProverContext cm, UniqueNamer namer)
+        {
+            this.cm = cm;
+            this.namer = namer;
+            this.letBindings = new Dictionary<VCExprVar, Term>();
+        }
+
+        public Term Linearise(VCExpr expr, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(expr != null);
+            return expr.Accept<Term, LineariserOptions>(this, options);
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        public Term Make(VCExprOp op, List<Term> children) {
+          Context z3 = cm.z3;
+          Term[] unwrapChildren = children.ToArray();
+          VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;
+          if (boogieFunctionOp != null) {
+            FuncDecl f = cm.GetFunction(boogieFunctionOp.Func.Name);
+            return z3.MkApp(f, unwrapChildren);
+          }
+          VCExprDistinctOp distinctOp = op as VCExprDistinctOp;
+          if (distinctOp != null) {
+            return z3.MkDistinct(unwrapChildren);
+          }
+
+          if (op == VCExpressionGenerator.AndOp) {
+            return z3.MkAnd(unwrapChildren);
+          }
+
+          if (op == VCExpressionGenerator.OrOp) {
+            return z3.MkOr(unwrapChildren);
+          }
+
+          if (op == VCExpressionGenerator.ImpliesOp) {
+            return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.NotOp) {
+            return z3.MkNot(unwrapChildren[0]);
+          }
+
+          if (op == VCExpressionGenerator.EqOp) {
+            return z3.MkEq(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.NeqOp) {
+            return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1]));
+          }
+
+          if (op == VCExpressionGenerator.LtOp) {
+            return z3.MkLt(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.LeOp) {
+            return z3.MkLe(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.GtOp) {
+            return z3.MkGt(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.GeOp) {
+            return z3.MkGe(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.AddOp) {
+            return z3.MkAdd(unwrapChildren);
+          }
+
+          if (op == VCExpressionGenerator.SubOp) {
+            return z3.MkSub(unwrapChildren);
+          }
+
+          if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) {
+            return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.MulOp) {
+            return z3.MkMul(unwrapChildren);
+          }
+
+          if (op == VCExpressionGenerator.ModOp) {
+            return z3.MkMod(unwrapChildren[0], unwrapChildren[1]);
+          }
+
+          if (op == VCExpressionGenerator.IfThenElseOp) {
+            return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
+          }
+
+          if (op == VCExpressionGenerator.ToIntOp) {
+            return z3.MkToInt(unwrapChildren[0]);
+          }
+
+          if (op == VCExpressionGenerator.ToRealOp) {
+            return z3.MkToReal(unwrapChildren[0]);
+          }
+
+          throw new Exception("unhandled boogie operator");
+        }
+
+        public Term Visit(VCExprLiteral node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+
+            if (node == VCExpressionGenerator.True)
+                return cm.z3.MkTrue();
+            else if (node == VCExpressionGenerator.False)
+                return cm.z3.MkFalse();
+            else if (node is VCExprIntLit)
+                return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());
+            else if (node is VCExprRealLit) {
+                string m = ((VCExprRealLit)node).Val.Mantissa.ToString();
+                BigInteger e = ((VCExprRealLit)node).Val.Exponent;
+                string f = BigInteger.Pow(10, e.Abs);
+
+                if (e == 0) {
+                    return cm.z3.MkNumeral(m, cm.z3.MkRealSort());
+                }
+                else if (((VCExprRealLit)node).Val.Exponent > 0) {
+                    return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));
+                }
+                else {
+                    return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));
+                }
+            }
+            else {
+              Contract.Assert(false);
+              throw new cce.UnreachableException();
+            }
+        }
+
+        public Term Visit(VCExprNAry node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+            VCExprOp op = node.Op;
+            Contract.Assert(op != null);
+
+            if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))
+            {
+                // handle these operators without recursion
+                List<Term> asts = new List<Term>();
+                string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";
+
+                IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
+                Contract.Assert(enumerator != null);
+                while (enumerator.MoveNext())
+                {
+                    VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+                    if (naryExpr == null || !naryExpr.Op.Equals(op))
+                    {
+                        asts.Add(Linearise(cce.NonNull((VCExpr)enumerator.Current), options));
+                    }
+                }
+
+                return Make(op, asts);
+            }
+
+            return node.Accept<Term, LineariserOptions>(OpLineariser, options);
+        }
+
+        public Term Visit(VCExprVar node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+            if (letBindings.ContainsKey(node))
+            {
+                return letBindings[node];
+            }
+            else
+            {
+                string varName = namer.GetName(node, node.Name);
+                return cm.GetConstant(varName, node.Type,node);
+            }
+        }
+
+        public Term Visit(VCExprQuantifier node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+            Contract.Assert(node.TypeParameters.Count == 0);
+
+            namer.PushScope();
+            try
+            {
+                List<string> varNames;
+                List<Type> varTypes;
+                VisitBounds(node.BoundVars, out varNames, out varTypes);
+                List<Pattern> patterns;
+                List<Term> no_patterns;
+                VisitTriggers(node.Triggers, options, out patterns, out no_patterns);
+                Term body = Linearise(node.Body, options);
+                Term result;
+                uint weight = 1;
+                string qid = "";
+                int skolemid = 0;
+
+                if (options.QuantifierIds)
+                {
+                    VCQuantifierInfos infos = node.Infos;
+                    Contract.Assert(infos != null);
+                    if (infos.qid != null)
+                    {
+                        qid = infos.qid;
+                    }
+                    if (0 <= infos.uniqueId)
+                    {
+                        skolemid = infos.uniqueId;
+                    }
+                }
+
+                if (options.UseWeights)
+                {
+                    weight = (uint) QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
+                }
+
+                switch (node.Quan)
+                {
+                    case Microsoft.Boogie.VCExprAST.Quantifier.ALL:
+                        result = MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
+                    case Microsoft.Boogie.VCExprAST.Quantifier.EX:
+                        result = MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
+                    default:
+                        throw new Exception("unknown quantifier kind " + node.Quan);
+                }
+                return result;
+            }
+            finally
+            {
+                namer.PopScope();
+            }
+        }
+
+        private Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {
+          List<Term> bound = new List<Term>();
+          for (int i = 0; i < varNames.Count; i++) {
+            Term t = cm.GetConstant(varNames[i], boogieTypes[i], null);
+            bound.Add(t);
+          }
+
+          Term termAst = cm.z3.MkQuantifier(isForall, weight, cm.z3.MkSymbol(qid), cm.z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body);
+          return termAst;
+        }
+
+        private void VisitBounds(List<VCExprVar> boundVars, out List<string> varNames, out List<Type> varTypes)
+        {
+            varNames = new List<string>();
+            varTypes = new List<Type>();
+            foreach (VCExprVar var in boundVars)
+            {
+                string varName = namer.GetLocalName(var, var.Name);
+                varNames.Add(varName);
+                varTypes.Add(var.Type);
+            }
+        }
+
+        private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns)
+        {
+            patterns = new List<Pattern>();
+            no_patterns = new List<Term>();
+            foreach (VCTrigger trigger in triggers)
+            {
+                List<Term> exprs = new List<Term>();
+                foreach (VCExpr expr in trigger.Exprs)
+                {
+                    System.Diagnostics.Debug.Assert(expr != null);
+                    Term termAst = Linearise(expr, options);
+                    exprs.Add(termAst);
+                }
+                if (exprs.Count > 0)
+                {
+                  if (trigger.Pos) {
+                    Pattern pattern = cm.z3.MkPattern(exprs.ToArray());
+                    patterns.Add(pattern);
+                  }
+                  else {
+                    System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");
+                    foreach (Term expr in exprs)
+                      no_patterns.Add(expr);
+                  }
+                }
+            }
+        }
+
+        public Term Visit(VCExprLet node, LineariserOptions options)
+        {
+            foreach (VCExprLetBinding b in node)
+            {
+                Term defAst = Linearise(b.E, options);
+                letBindings.Add(b.V, defAst);
+            }
+            Term letAst = Linearise(node.Body, options);
+            foreach (VCExprLetBinding b in node)
+            {
+                letBindings.Remove(b.V);
+            }
+            return letAst;
+        }  
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>
+        {
+            [ContractInvariantMethod]
+            void ObjectInvariant()
+            {
+                Contract.Invariant(ExprLineariser != null);
+            }
+
+            private readonly Z3apiExprLineariser ExprLineariser;
+
+            public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser)
+            {
+                Contract.Requires(ExprLineariser != null);
+                this.ExprLineariser = ExprLineariser;
+            }
+
+            ///////////////////////////////////////////////////////////////////////////////////
+
+            private Term WriteApplication(VCExprOp op, IEnumerable<VCExpr> terms, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(op != null);
+                Contract.Requires(cce.NonNullElements(terms));
+
+                List<Term> args = new List<Term>();
+                foreach (VCExpr e in terms)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                return ExprLineariser.Make(op, args);
+            }
+
+            ///////////////////////////////////////////////////////////////////////////////////
+
+            public Term VisitNotOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitEqOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitAndOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);  
+            }
+
+            public Term VisitOrOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options); 
+            }
+
+            public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) 
+            {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+              return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                VCExprLabelOp op = (VCExprLabelOp)node.Op;
+                Contract.Assert(op != null);
+                return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); 
+            }
+
+            public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                List<Term> args = new List<Term>();
+                foreach (VCExpr e in node)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                System.Diagnostics.Debug.Assert(args.Count >= 2);
+
+                Term selectTerm = args[0];
+                for (int i = 1; i < args.Count; i++) {
+                  selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]);
+                }
+                return selectTerm;
+            }
+
+            private Term ConstructStoreTerm(Term mapTerm, List<Term> args, int index) {
+              System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1);
+              if (index == args.Count - 2) {
+                return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]);
+              }
+              else {
+                Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1);
+                return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t);
+              }
+            }
+
+            public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                List<Term> args = new List<Term>();
+                foreach (VCExpr e in node)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                return ConstructStoreTerm(args[0], args, 1);
+            }
+
+            public Term VisitBvOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                List<int> args = new List<int>();
+                foreach (VCExpr e in node) {
+                  VCExprIntLit literal = e as VCExprIntLit;
+                  System.Diagnostics.Debug.Assert(literal != null);
+                  args.Add(literal.Val.ToInt);
+                }
+                System.Diagnostics.Debug.Assert(args.Count == 1);
+                return ExprLineariser.cm.z3.MkNumeral(args[0], ExprLineariser.cm.z3.MkBvSort((uint)node.Type.BvBits));
+            }
+
+            public Term VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+
+              VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
+              Contract.Assert(op != null);
+              System.Diagnostics.Debug.Assert(0 <= op.Start && op.Start < op.End);
+
+              List<Term> args = new List<Term>();
+              foreach (VCExpr e in node) {
+                Contract.Assert(e != null);
+                args.Add(ExprLineariser.Linearise(e, options));
+              }
+              System.Diagnostics.Debug.Assert(args.Count == 1);
+              return ExprLineariser.cm.z3.MkBvExtract((uint) op.End - 1, (uint) op.Start, args[0]);
+            }
+
+            public Term VisitBvConcatOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+
+              VCExprBvConcatOp op = (VCExprBvConcatOp)node.Op;
+              Contract.Assert(op != null);
+
+              List<Term> args = new List<Term>();
+              foreach (VCExpr e in node) {
+                Contract.Assert(e != null);
+                args.Add(ExprLineariser.Linearise(e, options));
+              }
+              System.Diagnostics.Debug.Assert(args.Count == 2);
+              return ExprLineariser.cm.z3.MkBvConcat(args[0], args[1]);
+            }
+
+            public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(node != null);
+                Contract.Requires(options != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitAddOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+              return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitSubOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitMulOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitDivOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitModOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+              return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitPowOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+              return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitLtOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitLeOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitGtOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitGeOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+              return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) {
+              Contract.Requires(options != null);
+              Contract.Requires(node != null);
+              return WriteApplication(node.Op, node, options);
+            }
+
+            public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(node.Op, node, options);
+            }
+        }
+    }
+}
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 1627536d..3fb2fe48 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -1,189 +1,189 @@
-<?xml version="1.0" encoding="utf-8"?>

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

-  <PropertyGroup>

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

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

-    <ProductVersion>9.0.21022</ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>

-    <OutputType>Library</OutputType>

-    <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>Microsoft.Boogie.Z3api</RootNamespace>

-    <AssemblyName>Provers.Z3api</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-    <StartupObject>

-    </StartupObject>

-    <FileUpgradeFlags>

-    </FileUpgradeFlags>

-    <OldToolsVersion>3.5</OldToolsVersion>

-    <UpgradeBackupLocation />

-    <PublishUrl>publish\</PublishUrl>

-    <Install>true</Install>

-    <InstallFrom>Disk</InstallFrom>

-    <UpdateEnabled>false</UpdateEnabled>

-    <UpdateMode>Foreground</UpdateMode>

-    <UpdateInterval>7</UpdateInterval>

-    <UpdateIntervalUnits>Days</UpdateIntervalUnits>

-    <UpdatePeriodically>false</UpdatePeriodically>

-    <UpdateRequired>false</UpdateRequired>

-    <MapFileExtensions>true</MapFileExtensions>

-    <ApplicationRevision>0</ApplicationRevision>

-    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>

-    <IsWebBootstrapper>false</IsWebBootstrapper>

-    <UseApplicationTrust>false</UseApplicationTrust>

-    <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>

-    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

-  </PropertyGroup>

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

-    <DebugSymbols>true</DebugSymbols>

-    <DebugType>full</DebugType>

-    <Optimize>false</Optimize>

-    <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

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

-    <DebugType>pdbonly</DebugType>

-    <Optimize>true</Optimize>

-    <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\z3apidebug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisRuleAssemblies>

-    </CodeAnalysisRuleAssemblies>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>Migrated rules for Z3api.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

-  </PropertyGroup>

-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\Checked\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisLogFile>bin\Debug\Provers.Z3api.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-  </PropertyGroup>

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

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

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

-  <Target Name="BeforeBuild">

-  </Target>

-  <Target Name="AfterBuild">

-  </Target>

-  -->

-  <ItemGroup>

-    <Reference Include="ManagedAPI">

-      <HintPath>..\..\..\..\..\iZ3\win\iZ3\Debug\ManagedAPI.dll</HintPath>

-    </Reference>

-    <Reference Include="System" />

-    <Reference Include="System.Core">

-      <RequiredTargetFramework>3.5</RequiredTargetFramework>

-    </Reference>

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

-    <Reference Include="System.XML" />

-  </ItemGroup>

-  <ItemGroup>

-    <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">

-      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

-      <Name>Basetypes</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj">

-      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

-      <Name>CodeContractsExtender</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\Core\Core.csproj">

-      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

-      <Name>Core</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\Model\Model.csproj">

-      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

-      <Name>Model</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">

-      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

-      <Name>ParserHelper</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">

-      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

-      <Name>VCExpr</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">

-      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

-      <Name>VCGeneration</Name>

-    </ProjectReference>

-  </ItemGroup>

-  <ItemGroup>

-    <Compile Include="..\..\version.cs">

-      <Link>version.cs</Link>

-    </Compile>

-    <Compile Include="ContextLayer.cs" />

-    <Compile Include="ProverLayer.cs" />

-    <Compile Include="TypeAdapter.cs">

-      <SubType>Code</SubType>

-    </Compile>

-    <Compile Include="VCExprVisitor.cs" />

-  </ItemGroup>

-  <ItemGroup>

-    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">

-      <Visible>False</Visible>

-      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>

-      <Install>false</Install>

-    </BootstrapperPackage>

-    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">

-      <Visible>False</Visible>

-      <ProductName>.NET Framework 3.5 SP1</ProductName>

-      <Install>true</Install>

-    </BootstrapperPackage>

-    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">

-      <Visible>False</Visible>

-      <ProductName>Windows Installer 3.1</ProductName>

-      <Install>true</Install>

-    </BootstrapperPackage>

-  </ItemGroup>

+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+    <ProductVersion>9.0.21022</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>Microsoft.Boogie.Z3api</RootNamespace>
+    <AssemblyName>Provers.Z3api</AssemblyName>
+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+    <FileAlignment>512</FileAlignment>
+    <StartupObject>
+    </StartupObject>
+    <FileUpgradeFlags>
+    </FileUpgradeFlags>
+    <OldToolsVersion>3.5</OldToolsVersion>
+    <UpgradeBackupLocation />
+    <PublishUrl>publish\</PublishUrl>
+    <Install>true</Install>
+    <InstallFrom>Disk</InstallFrom>
+    <UpdateEnabled>false</UpdateEnabled>
+    <UpdateMode>Foreground</UpdateMode>
+    <UpdateInterval>7</UpdateInterval>
+    <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+    <UpdatePeriodically>false</UpdatePeriodically>
+    <UpdateRequired>false</UpdateRequired>
+    <MapFileExtensions>true</MapFileExtensions>
+    <ApplicationRevision>0</ApplicationRevision>
+    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+    <IsWebBootstrapper>false</IsWebBootstrapper>
+    <UseApplicationTrust>false</UseApplicationTrust>
+    <BootstrapperEnabled>true</BootstrapperEnabled>
+    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <OutputPath>bin\Debug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <OutputPath>bin\Release\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\z3apidebug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CodeAnalysisRuleAssemblies>
+    </CodeAnalysisRuleAssemblies>
+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>Migrated rules for Z3api.ruleset</CodeAnalysisRuleSet>
+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+  </PropertyGroup>
+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\Checked\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CodeAnalysisLogFile>bin\Debug\Provers.Z3api.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly />
+    <CodeContractsCustomRewriterClass />
+    <CodeContractsLibPaths />
+    <CodeContractsExtraRewriteOptions />
+    <CodeContractsExtraAnalysisOptions />
+    <CodeContractsBaseLineFile />
+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+  </PropertyGroup>
+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
+  <ItemGroup>
+    <Reference Include="ManagedAPI">
+      <HintPath>..\..\..\..\..\iZ3\win\iZ3\Debug\ManagedAPI.dll</HintPath>
+    </Reference>
+    <Reference Include="System" />
+    <Reference Include="System.Core">
+      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    </Reference>
+    <Reference Include="System.Data" />
+    <Reference Include="System.XML" />
+  </ItemGroup>
+  <ItemGroup>
+    <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+      <Name>Basetypes</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj">
+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+      <Name>CodeContractsExtender</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\Core\Core.csproj">
+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+      <Name>Core</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\Model\Model.csproj">
+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+      <Name>Model</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">
+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+      <Name>ParserHelper</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
+      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+      <Name>VCExpr</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+      <Name>VCGeneration</Name>
+    </ProjectReference>
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="..\..\version.cs">
+      <Link>version.cs</Link>
+    </Compile>
+    <Compile Include="ContextLayer.cs" />
+    <Compile Include="ProverLayer.cs" />
+    <Compile Include="TypeAdapter.cs">
+      <SubType>Code</SubType>
+    </Compile>
+    <Compile Include="VCExprVisitor.cs" />
+  </ItemGroup>
+  <ItemGroup>
+    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+      <Install>false</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
+      <Visible>False</Visible>
+      <ProductName>Windows Installer 3.1</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+  </ItemGroup>
 </Project>
\ No newline at end of file
diff --git a/Source/Provers/Z3api/cce.cs b/Source/Provers/Z3api/cce.cs
index ef594484..1e0b12a5 100644
--- a/Source/Provers/Z3api/cce.cs
+++ b/Source/Provers/Z3api/cce.cs
@@ -1,193 +1,193 @@
-using System;

-using SA=System.Attribute;

-using System.Collections.Generic;

-using System.Diagnostics.Contracts;

-using System.Text;

-//using Microsoft.Boogie;

-

-/// <summary>

-/// A class containing static methods to extend the functionality of Code Contracts

-/// </summary>

-

-public static class cce {

-  //[Pure]

-  //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

-  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

-  //}

-  [Pure]

-  public static T NonNull<T>(T t) {

-    Contract.Assert(t != null);

-    return t;

-  }

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerable<T> collection) {

-    return collection != null && Contract.ForAll(collection, c => c != null);

-  }

-  [Pure]

-  public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

-    return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));

-  }

-  //[Pure]

-  //public static bool NonNullElements(VariableSeq collection) {

-  //  return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

-  //}

-  /// <summary>

-  /// For possibly-null lists of non-null elements

-  /// </summary>

-  /// <typeparam name="T"></typeparam>

-  /// <param name="collection"></param>

-  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

-  /// <returns></returns>

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

-    return (nullability && collection == null) || cce.NonNullElements(collection);

-    //Should be the same as:

-    /*if(nullability&&collection==null)

-     * return true;

-     * return cce.NonNullElements(collection)

-     */

-

-  }

-  [Pure]

-  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

-    return kvp.Key != null && kvp.Value != null;

-  }

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

-    return iEnumerator != null;

-  }

-  //[Pure]

-  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

-  //  return cce.NonNullElements(graph.TopologicalSort());

-  //}

-  [Pure]

-  public static void BeginExpose(object o) {

-  }

-  [Pure]

-  public static void EndExpose() {

-  }

-  [Pure]

-  public static bool IsPeerConsistent(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsConsistent(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsExposable(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsExposed(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsNew(object o) {

-    return true;

-  }

-  public static class Owner {

-    [Pure]

-    public static bool Same(object o, object p) {

-      return true;

-    }

-    [Pure]

-    public static void AssignSame(object o, object p) {

-    }

-    [Pure]

-    public static object ElementProxy(object o) {

-      return o;

-    }

-    [Pure]

-    public static bool None(object o) {

-      return true;

-    }

-    [Pure]

-    public static bool Different(object o, object p) {

-      return true;

-    }

-    [Pure]

-    public static bool New(object o) {

-      return true;

-    }

-  }

-  [Pure]

-  public static void LoopInvariant(bool p) {

-    Contract.Assert(p);

-  }

-  public class UnreachableException : Exception {

-    public UnreachableException() {

-    }

-  }

-  //[Pure]

-  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

-  //  return true;

-  //}

-  //public static List<T> toList<T>(PureCollections.Sequence s) {

-  //  List<T> toRet = new List<T>();

-  //  foreach (T t in s.elems)

-  //    if(t!=null)

-  //    toRet.Add(t);

-  //  return toRet;

-  //}

-

-  //internal static bool NonNullElements(Set set) {

-  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

-  //}

-}

-

-public class PeerAttribute : SA {

-}

-public class RepAttribute : SA {

-}

-public class CapturedAttribute : SA {

-}

-public class NotDelayedAttribute : SA {

-}

-public class NoDefaultContractAttribute : SA {

-}

-public class VerifyAttribute : SA {

-  public VerifyAttribute(bool b) {

-

-  }

-}

-public class StrictReadonlyAttribute : SA {

-}

-public class AdditiveAttribute : SA {

-}

-public class ReadsAttribute : SA {

-  public enum Reads {

-    Nothing,

-    Everything,

-  };

-  public ReadsAttribute(object o) {

-  }

-}

-public class GlobalAccessAttribute : SA {

-  public GlobalAccessAttribute(bool b) {

-  }

-}

-public class EscapesAttribute : SA {

-  public EscapesAttribute(bool b, bool b_2) {

-  }

-}

-public class NeedsContractsAttribute : SA {

-  public NeedsContractsAttribute() {

-  }

-  public NeedsContractsAttribute(bool ret, bool parameters) {

-  }

-  public NeedsContractsAttribute(bool ret, int[] parameters) {

-  }

-}

-public class ImmutableAttribute : SA {

-}

-public class InsideAttribute : SA {

-}

-public class SpecPublicAttribute : SA {

-}

-public class ElementsPeerAttribute : SA {

-}

-public class ResultNotNewlyAllocatedAttribute : SA {

-}

-public class OnceAttribute : SA {

+using System;
+using SA=System.Attribute;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Text;
+//using Microsoft.Boogie;
+
+/// <summary>
+/// A class containing static methods to extend the functionality of Code Contracts
+/// </summary>
+
+public static class cce {
+  //[Pure]
+  //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
+  //}
+  [Pure]
+  public static T NonNull<T>(T t) {
+    Contract.Assert(t != null);
+    return t;
+  }
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerable<T> collection) {
+    return collection != null && Contract.ForAll(collection, c => c != null);
+  }
+  [Pure]
+  public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
+    return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
+  }
+  //[Pure]
+  //public static bool NonNullElements(VariableSeq collection) {
+  //  return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
+  //}
+  /// <summary>
+  /// For possibly-null lists of non-null elements
+  /// </summary>
+  /// <typeparam name="T"></typeparam>
+  /// <param name="collection"></param>
+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>
+  /// <returns></returns>
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
+    return (nullability && collection == null) || cce.NonNullElements(collection);
+    //Should be the same as:
+    /*if(nullability&&collection==null)
+     * return true;
+     * return cce.NonNullElements(collection)
+     */
+
+  }
+  [Pure]
+  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
+    return kvp.Key != null && kvp.Value != null;
+  }
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
+    return iEnumerator != null;
+  }
+  //[Pure]
+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
+  //  return cce.NonNullElements(graph.TopologicalSort());
+  //}
+  [Pure]
+  public static void BeginExpose(object o) {
+  }
+  [Pure]
+  public static void EndExpose() {
+  }
+  [Pure]
+  public static bool IsPeerConsistent(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsConsistent(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsExposable(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsExposed(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsNew(object o) {
+    return true;
+  }
+  public static class Owner {
+    [Pure]
+    public static bool Same(object o, object p) {
+      return true;
+    }
+    [Pure]
+    public static void AssignSame(object o, object p) {
+    }
+    [Pure]
+    public static object ElementProxy(object o) {
+      return o;
+    }
+    [Pure]
+    public static bool None(object o) {
+      return true;
+    }
+    [Pure]
+    public static bool Different(object o, object p) {
+      return true;
+    }
+    [Pure]
+    public static bool New(object o) {
+      return true;
+    }
+  }
+  [Pure]
+  public static void LoopInvariant(bool p) {
+    Contract.Assert(p);
+  }
+  public class UnreachableException : Exception {
+    public UnreachableException() {
+    }
+  }
+  //[Pure]
+  //public static bool IsValid(Microsoft.Dafny.Expression expression) {
+  //  return true;
+  //}
+  //public static List<T> toList<T>(PureCollections.Sequence s) {
+  //  List<T> toRet = new List<T>();
+  //  foreach (T t in s.elems)
+  //    if(t!=null)
+  //    toRet.Add(t);
+  //  return toRet;
+  //}
+
+  //internal static bool NonNullElements(Set set) {
+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
+  //}
+}
+
+public class PeerAttribute : SA {
+}
+public class RepAttribute : SA {
+}
+public class CapturedAttribute : SA {
+}
+public class NotDelayedAttribute : SA {
+}
+public class NoDefaultContractAttribute : SA {
+}
+public class VerifyAttribute : SA {
+  public VerifyAttribute(bool b) {
+
+  }
+}
+public class StrictReadonlyAttribute : SA {
+}
+public class AdditiveAttribute : SA {
+}
+public class ReadsAttribute : SA {
+  public enum Reads {
+    Nothing,
+    Everything,
+  };
+  public ReadsAttribute(object o) {
+  }
+}
+public class GlobalAccessAttribute : SA {
+  public GlobalAccessAttribute(bool b) {
+  }
+}
+public class EscapesAttribute : SA {
+  public EscapesAttribute(bool b, bool b_2) {
+  }
+}
+public class NeedsContractsAttribute : SA {
+  public NeedsContractsAttribute() {
+  }
+  public NeedsContractsAttribute(bool ret, bool parameters) {
+  }
+  public NeedsContractsAttribute(bool ret, int[] parameters) {
+  }
+}
+public class ImmutableAttribute : SA {
+}
+public class InsideAttribute : SA {
+}
+public class SpecPublicAttribute : SA {
+}
+public class ElementsPeerAttribute : SA {
+}
+public class ResultNotNewlyAllocatedAttribute : SA {
+}
+public class OnceAttribute : SA {
 }
\ No newline at end of file