clean up in z3api

7 files changed, 593 insertions, 837 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index e6ba7b66..ed45c4fc 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -69,38 +69,6 @@ namespace Microsoft.Boogie.Z3
         }

     }

 

-    public abstract class Z3TermAst { }

-    public abstract class Z3PatternAst { }

-    public abstract class Z3ConstDeclAst { }

-    public abstract class Z3LabeledLiterals { }

-

-    public interface Z3Context

-    {

-        void CreateBacktrackPoint();

-        void Backtrack();

-        void AddAxiom(VCExpr axiom, LineariserOptions linOptions);

-        void AddConjecture(VCExpr vc, LineariserOptions linOptions);

-        void AddSmtlibString(string smtlibString);

-        string GetDeclName(Z3ConstDeclAst constDeclAst);

-        Z3PatternAst MakePattern(List<Z3TermAst> exprs);

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

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

-        void TypeCheckBool(Z3TermAst t);

-        void TypeCheckInt(Z3TermAst t);

-        void DeclareType(string typeName);

-        void DeclareConstant(string constantName, Type boogieType);

-        void DeclareFunction(string functionName, List<Type> domain, Type range);

-        Z3TermAst GetConstant(string constantName, Type constantType);

-        Z3TermAst MakeIntLiteral(string numeral);

-        Z3TermAst MakeTrue();

-        Z3TermAst MakeFalse();

-        Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child);

-        Z3LabeledLiterals GetRelevantLabels();

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

-        Z3TermAst MakeArraySelect(List<Z3TermAst> args);

-        Z3TermAst MakeArrayStore(List<Z3TermAst> args);

-    }

-

     internal class PartitionMap

     {

         private Context ctx;

@@ -138,43 +106,51 @@ namespace Microsoft.Boogie.Z3
             Sort boolSort = ctx.MkBoolSort();

             Sort intSort = ctx.MkIntSort();

             ArrayValue av;

-

+            

             if (s.Equals(boolSort))

             {

                 return ctx.GetBoolValue(v);

             }

-            else if (s.Equals(intSort))

-            {

-                int i;

-                if (ctx.TryGetNumeralInt(v, out i))

-                {

-                    return BigNum.FromInt(i);

-                }

-                else

-                {

-                    return BigNum.FromString(ctx.GetNumeralString(v));

-                }

+            else if (s.Equals(intSort)) {

+              int i;

+              long il;

+              uint u;

+              ulong ul;

+              if (ctx.TryGetNumeralInt(v, out i)) {

+                return BigNum.FromInt(i);

+              }

+              else if (ctx.TryGetNumeralInt64(v, out il)) {

+                return BigNum.FromLong(il);

+              }

+              else if (ctx.TryGetNumeralUInt(v, out u)) {

+                return BigNum.FromUInt(u);

+              }

+              else if (ctx.TryGetNumeralUInt64(v, out ul)) {

+                return BigNum.FromULong(ul);

+              }

+              else {

+                string str = v.ToString();

+                return GetPartition(v);

+                //return BigNum.FromString(ctx.GetNumeralString(v));

+              }

             }

-            else if (model.TryGetArrayValue(v, out av))

-            {

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

-                List<int> tuple;

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

-                {

-                    tuple = new List<int>();

-                    tuple.Add(GetPartition(av.Domain[i]));

-                    tuple.Add(GetPartition(av.Range[i]));

-                    arrayValue.Add(tuple);

-                }

+            else if (model.TryGetArrayValue(v, out av)) {

+              List<List<int>> arrayValue = new List<List<int>>();

+              List<int> tuple;

+              for (int i = 0; i < av.Domain.Length; i++) {

                 tuple = new List<int>();

-                tuple.Add(GetPartition(av.ElseCase));

+                tuple.Add(GetPartition(av.Domain[i]));

+                tuple.Add(GetPartition(av.Range[i]));

                 arrayValue.Add(tuple);

-                return arrayValue;

+              }

+              tuple = new List<int>();

+              tuple.Add(GetPartition(av.ElseCase));

+              arrayValue.Add(tuple);

+              return arrayValue;

             }

-            else

-            {

-                // The term is uninterpreted; just return the partition id.

-                return GetPartition(v);

+            else {

+              // The term is uninterpreted; just return the partition id.

+              return GetPartition(v);

             }

         }

 

@@ -249,7 +225,7 @@ namespace Microsoft.Boogie.Z3
         public BoogieErrorModelBuilder(Z3Context container, Model z3Model)

         {

             this.container = container;

-            this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3, z3Model);

+            this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model);

         }

         

         private Dictionary<string, int> CreateConstantToPartition(Model z3Model)

@@ -257,7 +233,7 @@ namespace Microsoft.Boogie.Z3
             Dictionary<string, int> constantToPartition = new Dictionary<string, int>();

             foreach (FuncDecl c in z3Model.GetModelConstants())

             {

-                string name = container.GetDeclName(new Z3TypeSafeConstDecl(c));

+                string name = container.GetDeclName(c);

                 int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0]));

                 constantToPartition.Add(name, pid);

             }

@@ -285,7 +261,7 @@ namespace Microsoft.Boogie.Z3
             foreach (KeyValuePair<FuncDecl, FunctionGraph> kv in z3Model.GetFunctionGraphs())

             {

                 List<List<int>> f_tuples = new List<List<int>>();

-                string f_name = container.GetDeclName(new Z3TypeSafeConstDecl(kv.Key));

+                string f_name = container.GetDeclName(kv.Key);

                 FunctionGraph graph = kv.Value;

                 foreach (FunctionEntry entry in graph.Entries)

                 {

@@ -310,8 +286,8 @@ namespace Microsoft.Boogie.Z3
             Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);

             Dictionary<string, List<List<int>>> functionToPartition = CreateFunctionToPartition(z3Model);

             List<List<string>> partitionToConstant = CreatePartitionToConstant(constantToPartition);

-            List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3SafeContext)container).z3);

-            Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3SafeContext)container).z3);

+            List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3Context)container).z3);

+            Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3Context)container).z3);

             return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition);

         }

     }

@@ -334,4 +310,395 @@ namespace Microsoft.Boogie.Z3
             this._relevantLabels = relevantLabels;

         }

     }

+

+    public class Z3Context {

+      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>();

+

+      public Context z3;

+      public Z3Config config;

+      public Z3apiProverContext ctxt;

+      private VCExpressionGenerator gen;

+      private Z3TypeCachedBuilder tm;

+      private UniqueNamer namer;

+      public UniqueNamer Namer {

+        get { return namer; }

+      }

+      private StreamWriter z3log;

+      public Z3Context(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen) {

+        Context z3 = new Context(config.Config);

+        if (config.LogFilename != null)

+          z3.OpenLog(config.LogFilename);

+        foreach (string tag in config.DebugTraces)

+          z3.EnableDebugTrace(tag);

+        this.ctxt = ctxt;

+        this.z3 = z3;

+        this.config = config;

+        this.tm = new Z3TypeCachedBuilder(this);

+        this.gen = gen;

+        this.namer = new UniqueNamer();

+        this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);

+        this.z3log = null;

+      }

+

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

+        z3.CloseLog();

+        if (z3log != null) {

+          z3log.Close();

+        }

+        z3log = null;

+      }

+

+      public void CreateBacktrackPoint() {

+        symbols.CreateBacktrackPoint();

+        constants.CreateBacktrackPoint();

+        functions.CreateBacktrackPoint();

+        labels.CreateBacktrackPoint();

+        z3.Push();

+        log("(push)");

+      }

+

+      public void Backtrack() {

+        z3.Pop();

+        labels.Backtrack();

+        functions.Backtrack();

+        constants.Backtrack();

+        symbols.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);

+        }

+      }

+

+      public string GetDeclName(FuncDecl constDeclAst) {

+        Symbol symbol = z3.GetDeclName(constDeclAst);

+        return z3.GetSymbolString(symbol);

+      }

+

+      public Pattern MakePattern(List<Term> exprs) {

+        Pattern pattern = z3.MkPattern(exprs.ToArray());

+        return pattern;

+      }

+

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

+      }

+

+      public 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 = GetConstant(varNames[i], boogieTypes[i]);

+          bound.Add(t);

+        }

+

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

+        return termAst;

+      }

+

+      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 Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels) {

+        BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model);

+        Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);

+        return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));

+      }

+

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

+        foreach (string labelName in relevantLabels) {

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

+        }

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

+      }

+

+      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.config.Counterexamples);

+        while (true) {

+          Model 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);

+          }

+          boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

+

+          if (boogieErrors.Count < this.config.Counterexamples) {

+            z3.BlockLiterals(labels);

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

+          }

+

+          labels.Dispose();

+          z3Model.Dispose();

+          if (boogieErrors.Count == this.config.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;

+

+        Model 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);

+          }

+          boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

+

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

+        }

+      }

+

+      public void DeclareType(string typeName) {

+        log("(declare-sort {0})", typeName);

+      }

+

+      public 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 void DeclareFunction(string functionName, List<Type> domain, Type range) {

+        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);

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

+      }

+

+      private List<Symbol> GetSymbols(List<string> symbolNames) {

+        List<Symbol> symbols = new List<Symbol>();

+        foreach (string symbolName in symbolNames)

+          symbols.Add(GetSymbol(symbolName));

+        return symbols;

+      }

+

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

+      }

+

+      private FuncDecl GetFunction(string functionName) {

+        FuncDecl function;

+        if (!functions.TryGetValue(functionName, out function))

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

+        return function;

+      }

+

+      public Term GetConstant(string constantName, Type constantType) {

+        Term typeSafeTerm;

+        if (!constants.ContainsKey(constantName))

+          this.DeclareConstant(constantName, constantType);

+

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

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

+        return typeSafeTerm;

+      }

+

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

+      }

+

+      public Term Make(string op, List<Term> children) {

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

+        Term term;

+        switch (op) {

+          // formulas  

+          case "AND": term = z3.MkAnd(unwrapChildren); break;

+          case "OR": term = z3.MkOr(unwrapChildren); break;

+          case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break;

+          case "NOT": term = z3.MkNot(unwrapChildren[0]); break;

+          case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break;

+          // terms

+          case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break;

+          case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break;

+          case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break;

+          // terms

+          case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break;

+          case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break;

+          case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break;

+          case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break;

+          case "+": term = z3.MkAdd(unwrapChildren); break;

+          case "-": term = z3.MkSub(unwrapChildren); break;

+          case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break;

+          case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break;

+          case "*": term = z3.MkMul(unwrapChildren); break;

+          default: {

+              FuncDecl f = GetFunction(op);

+              term = z3.MkApp(f, unwrapChildren);

+            }

+            break;

+        }

+        return term;

+      }

+    }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 7bdc07a0..f691cffc 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.Z3
         public override void Close()

         {

             base.Close();

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.CloseLog();

             cm.z3.Dispose();

             cm.config.Config.Dispose();

@@ -55,7 +55,7 @@ namespace Microsoft.Boogie.Z3
 

         public void PushAxiom(VCExpr axiom)

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.CreateBacktrackPoint();

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

             cm.AddAxiom(axiom, linOptions);

@@ -64,7 +64,7 @@ namespace Microsoft.Boogie.Z3
 

         private void PushConjecture(VCExpr conjecture)

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.CreateBacktrackPoint();

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

             cm.AddConjecture(conjecture, linOptions);

@@ -78,14 +78,14 @@ namespace Microsoft.Boogie.Z3
 

         public void CreateBacktrackPoint()

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.CreateBacktrackPoint();

         }

 

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

         {

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

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             Push();

             cm.AddAxiom(context.Axioms, linOptions);

             cm.AddConjecture(vc, linOptions);

@@ -95,33 +95,33 @@ namespace Microsoft.Boogie.Z3
   

         public override void Check()

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             outcome = cm.Check(out z3LabelModels);

         }

 

         public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

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

             outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);

         }

 

         public override void Push()

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.CreateBacktrackPoint();

         }

 

         public override void Pop()

         {

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.Backtrack();

         }

 

         public override void Assert(VCExpr vc, bool polarity)

         {

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

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             if (polarity)

                 cm.AddAxiom(vc, linOptions);

             else

@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.Z3
         public override void AssertAxioms()

         {

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

-            Z3SafeContext cm = context.cm;

+            Z3Context cm = context.cm;

             cm.AddAxiom(context.Axioms, linOptions);

         }

 

@@ -191,13 +191,13 @@ namespace Microsoft.Boogie.Z3
 

     public class Z3apiProverContext : DeclFreeProverContext

     {

-        public Z3SafeContext cm;

+        public Z3Context cm;

         

         public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)

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

         {

             Z3Config config = BuildConfig(opts.Timeout * 1000, true);

-            this.cm = new Z3SafeContext(this, config, gen);

+            this.cm = new Z3Context(this, config, gen);

         }

         private static Z3Config BuildConfig(int timeout, bool nativeBv)

         {

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 30207e75..72192804 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -12,641 +12,5 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace Microsoft.Boogie.Z3

 {

-    internal class Z3TypeSafeTerm : Z3TermAst

-    {

-        private Term termAst;

-        public Z3TypeSafeTerm(Term termAst)

-        {

-            this.termAst = termAst;

-        }

-        public Term TermAst

-        {

-            get { return this.termAst; }

-        }

-    }

-

-    internal class Z3TypeSafePattern : Z3PatternAst

-    {

-        private Pattern patternAst;

-        public Z3TypeSafePattern(Pattern patternAst)

-        {

-            this.patternAst = patternAst;

-        }

-        public Pattern PatternAst

-        {

-            get { return this.patternAst; }

-        }

-    }

-

-    internal class Z3TypeSafeConstDecl : Z3ConstDeclAst

-    {

-        private FuncDecl constDeclAst;

-        public Z3TypeSafeConstDecl(FuncDecl constDeclAst)

-        {

-            this.constDeclAst = constDeclAst;

-        }

-        public FuncDecl ConstDeclAst

-        {

-            get { return this.constDeclAst; }

-        }

-    }

-

-    public class Z3SafeType : Z3Type

-    {

-        private Sort typeAst;

-        public Z3SafeType(Sort typeAst)

-        {

-            this.typeAst = typeAst;

-        }

-        public Sort TypeAst

-        {

-            get { return this.typeAst; }

-        }

-    }

-

-    public class Z3SafeLabeledLiterals : Z3LabeledLiterals

-    {

-        private LabeledLiterals labeledLiterals;

-        public Z3SafeLabeledLiterals(LabeledLiterals labeledLiterals)

-        {

-            this.labeledLiterals = labeledLiterals;

-        }

-        public LabeledLiterals LabeledLiterals

-        {

-            get { return this.labeledLiterals; }

-        }

-    }

-

-    public class Z3SafeContext : Z3Context

-    {

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

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

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

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

-

-        public Context z3;

-        public Z3Config config;

-        public Z3apiProverContext ctxt;

-        private VCExpressionGenerator gen;

-        private Z3TypeCachedBuilder tm;

-        private UniqueNamer namer;

-        public UniqueNamer Namer

-        {

-            get { return namer; }

-        }

-        private StreamWriter z3log;

-        public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen)

-        {

-            Context z3 = new Context(config.Config);

-            if (config.LogFilename != null)

-                z3.OpenLog(config.LogFilename);

-            foreach (string tag in config.DebugTraces)

-                z3.EnableDebugTrace(tag);

-            this.ctxt = ctxt;

-            this.z3 = z3;

-            this.config = config;

-            this.tm = new Z3TypeCachedBuilder(this);

-            this.gen = gen;

-            this.namer = new UniqueNamer();

-            this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);

-            this.z3log = null;

-        }

-

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

-        {

-            z3.CloseLog();

-            if (z3log != null)

-            {

-                z3log.Close();

-            }

-            z3log = null;

-        }

-

-        public void CreateBacktrackPoint()

-        {

-            symbols.CreateBacktrackPoint();

-            constants.CreateBacktrackPoint();

-            functions.CreateBacktrackPoint();

-            labels.CreateBacktrackPoint();

-            z3.Push();

-            log("(push)");

-        }

-

-        public void Backtrack()

-        {

-            z3.Pop();

-            labels.Backtrack();

-            functions.Backtrack();

-            constants.Backtrack();

-            symbols.Backtrack();

-            log("(pop)");

-        }

-

-        public void AddAxiom(VCExpr axiom, LineariserOptions linOptions)

-        {

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

-            Z3TermAst z3ast = (Z3TermAst)axiom.Accept(visitor, linOptions);

-            Term term = Unwrap(z3ast);

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

-            Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);

-            Term term = Unwrap(z3ast);

-            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, new Z3TypeSafeConstDecl(decl));

-            }

-            foreach (Term assumption in assumptions)

-            {

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

-                z3.AssertCnstr(assumption);

-            }

-        }

-

-        public string GetDeclName(Z3ConstDeclAst constDeclAst)

-        {

-            Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst;

-            Symbol symbol = z3.GetDeclName(typeSafeConstDecl.ConstDeclAst);

-            return z3.GetSymbolString(symbol);

-        }

-

-        private List<Term> Unwrap(List<Z3TermAst> terms)

-        {

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

-            foreach (Z3TermAst term in terms)

-            {

-                Term unwrapTerm = Unwrap(term);

-                unwrap.Add(unwrapTerm);

-            }

-            return unwrap;

-        }

-

-        private List<Pattern> Unwrap(List<Z3PatternAst> patterns)

-        {

-            List<Pattern> unwrap = new List<Pattern>();

-            foreach (Z3PatternAst pattern in patterns)

-            {

-                Z3TypeSafePattern typeSafePattern = (Z3TypeSafePattern)pattern;

-                unwrap.Add(typeSafePattern.PatternAst);

-            }

-            return unwrap;

-        }

-

-        private Sort Unwrap(Z3Type type)

-        {

-            Z3SafeType typeSafeTerm = (Z3SafeType)type;

-            return typeSafeTerm.TypeAst;

-        }

-

-        private Term Unwrap(Z3TermAst term)

-        {

-            Z3TypeSafeTerm typeSafeTerm = (Z3TypeSafeTerm)term;

-            return typeSafeTerm.TermAst;

-        }

-

-        private FuncDecl Unwrap(Z3ConstDeclAst constDeclAst)

-        {

-            Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst;

-            return typeSafeConstDecl.ConstDeclAst;

-        }

-

-        private Z3TypeSafeTerm Wrap(Term term)

-        {

-            return new Z3TypeSafeTerm(term);

-        }

-

-        private Z3TypeSafeConstDecl Wrap(FuncDecl constDecl)

-        {

-            return new Z3TypeSafeConstDecl(constDecl);

-        }

-

-        private Z3TypeSafePattern Wrap(Pattern pattern)

-        {

-            return new Z3TypeSafePattern(pattern);

-        }

-

-        public Z3PatternAst MakePattern(List<Z3TermAst> exprs)

-        {

-            List<Term> unwrapExprs = Unwrap(exprs);

-            Pattern pattern = z3.MkPattern(unwrapExprs.ToArray());

-            Z3PatternAst wrapPattern = Wrap(pattern);

-            return wrapPattern;

-        }

-

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

-        {

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

-            foreach (Type boogieType in boogieTypes)

-            {

-                Z3Type type = tm.GetType(boogieType);

-                Sort unwrapType = Unwrap(type);

-                z3Types.Add(unwrapType);

-            }

-            return z3Types;

-        }

-

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

-        {

-            List<Pattern> unwrapPatterns = Unwrap(patterns);

-            List<Term> unwrapNoPatterns = Unwrap(no_patterns);

-            Term unwrapBody = Unwrap(body);

-

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

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

-            {

-                Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]);

-                bound.Add(Unwrap(t));

-            }

-

-            Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody);

-            return Wrap(termAst);

-        }

    

-        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 Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels)

-        {

-            BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model);

-            Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);

-            return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));

-        }

-

-        private void DisplayRelevantLabels(List<string> relevantLabels)

-        {

-            foreach (string labelName in relevantLabels)

-            {

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

-            }

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

-        }

-

-        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.config.Counterexamples);

-            while (true)

-            {

-                Model 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);

-                }

-                boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

-

-                if (boogieErrors.Count < this.config.Counterexamples)

-                {

-                    z3.BlockLiterals(labels);

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

-                }

-

-                labels.Dispose();

-                z3Model.Dispose();

-                if (boogieErrors.Count == this.config.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;

-

-            Model 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);

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

-                assumption_terms[i] = Unwrap(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);

-                }

-                boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

-

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

-            }

-        }

-

-        public void TypeCheckBool(Z3TermAst term)

-        {

-            Term unwrapTerm = Unwrap(term);

-            bool boolType = z3.GetSort(unwrapTerm).Equals(z3.MkBoolSort());

-            if (!boolType)

-                throw new Exception("Failed Bool Typecheck");

-        }

-

-        public void TypeCheckInt(Z3TermAst term)

-        {

-            Term unwrapTerm = Unwrap(term);

-            bool intType = z3.GetSort(unwrapTerm).Equals(z3.MkIntSort());

-            if (!intType)

-                throw new Exception("Failed Int Typecheck");

-        }

-

-        public void DeclareType(string typeName)

-        {

-            log("(declare-sort {0})", typeName);

-        }

-

-        public void DeclareConstant(string constantName, Type boogieType)

-        {

-            Symbol symbolAst = GetSymbol(constantName);

-            Z3Type typeAst = tm.GetType(boogieType);

-            Sort unwrapTypeAst = Unwrap(typeAst);

-

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

-            constants.Add(constantName, Wrap(constAst));

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

-        }

-

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

-        {

-            Symbol symbolAst = GetSymbol(functionName);

-

-            var domainStr = "";

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

-            foreach (Type domainType in domain)

-            {

-                Z3Type type = tm.GetType(domainType);

-                Sort unwrapType = Unwrap(type);

-                domainAst.Add(unwrapType);

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

-            }

-            Z3Type rangeAst = tm.GetType(range);

-            Sort unwrapRangeAst = Unwrap(rangeAst);

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

-            Z3TypeSafeConstDecl typeSafeConstDecl = Wrap(constDeclAst);

-            functions.Add(functionName, typeSafeConstDecl);

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

-        }

-

-        private List<Symbol> GetSymbols(List<string> symbolNames)

-        {

-            List<Symbol> symbols = new List<Symbol>();

-            foreach (string symbolName in symbolNames)

-                symbols.Add(GetSymbol(symbolName));

-            return symbols;

-        }

-

-        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 Z3TermAst GetConstant(string constantName, Type constantType)

-        {

-            Z3TypeSafeTerm typeSafeTerm;

-            if (!constants.ContainsKey(constantName))

-                this.DeclareConstant(constantName, constantType);

-

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

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

-            return typeSafeTerm;

-        }

-

-        public Z3TermAst MakeIntLiteral(string numeral)

-        {

-            Term term = z3.MkNumeral(numeral, z3.MkIntSort());

-            Z3TypeSafeTerm typeSafeTerm = Wrap(term);

-            return typeSafeTerm;

-        }

-

-        public Z3TermAst MakeTrue()

-        {

-            Term term = z3.MkTrue();

-            Z3TypeSafeTerm typeSafeTerm = Wrap(term);

-            return typeSafeTerm;

-        }

-

-        public Z3TermAst MakeFalse()

-        {

-            Term term = z3.MkFalse();

-            Z3TypeSafeTerm typeSafeTerm = Wrap(term);

-            return typeSafeTerm;

-        }

-

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

-        {

-            Symbol labelSymbol = this.GetSymbol(labelName);

-            Term unwrapChild = Unwrap(child);

-

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

-

-            Z3TypeSafeTerm wrapLabeledExpr = Wrap(labeledExpr);

-            labels.Add(labelName, wrapLabeledExpr);

-            return wrapLabeledExpr;

-        }

-

-        public Z3LabeledLiterals GetRelevantLabels()

-        {

-            Z3SafeLabeledLiterals safeLiterals = new Z3SafeLabeledLiterals(z3.GetRelevantLabels());

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

-            return safeLiterals;

-        }

-

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

-        {

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

-            Term term;

-            switch (op)

-            {

-                // formulas  

-                case "AND": term = z3.MkAnd(unwrapChildren); break;

-                case "OR": term = z3.MkOr(unwrapChildren); break;

-                case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break;

-                case "NOT": term = z3.MkNot(unwrapChildren[0]); break;

-                case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break;

-                // terms

-                case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break;

-                case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break;

-                case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break;

-                // terms

-                case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break;

-                case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break;

-                case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break;

-                case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break;

-                case "+": term = z3.MkAdd(unwrapChildren); break;

-                case "-": term = z3.MkSub(unwrapChildren); break;

-                case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break;

-                case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break;

-                case "*": term = z3.MkMul(unwrapChildren); break;

-                default:

-                    {

-                        FuncDecl f = GetFunction(op);

-                        term = z3.MkApp(f, unwrapChildren);

-                    }

-                    break;

-            }

-            Z3TypeSafeTerm typeSafeTerm = Wrap(term);

-            return typeSafeTerm;

-        }

-

-        private FuncDecl GetFunction(string functionName)

-        {

-            Z3TypeSafeConstDecl function;

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

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

-            FuncDecl unwrapFunction = Unwrap(function);

-            return unwrapFunction;

-        }

-

-        public Z3TermAst MakeArraySelect(List<Z3TermAst> args)

-        {

-            Term[] unwrapChildren = Unwrap(args).ToArray();

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

-        }

-

-        public Z3TermAst MakeArrayStore(List<Z3TermAst> args)

-        {

-            Term[] unwrapChildren = Unwrap(args).ToArray();

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

-        }

-    }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index b8aa607f..b129b378 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -45,6 +45,9 @@ namespace Microsoft.Boogie.Z3 {
     public Z3TermAst MakeIntLiteral(string numeral) {

       return new Z3StubTermAst();

     }

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

+      return new Z3StubTermAst();

+    }

     public Z3TermAst MakeTrue() {

       return new Z3StubTermAst();

     }

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index dec25e97..de5ebd8f 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -75,10 +75,10 @@ namespace Microsoft.Boogie.Z3
           }

         }

 

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

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

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

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

+        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 Z3Context container;

 

@@ -87,61 +87,61 @@ namespace Microsoft.Boogie.Z3
             this.container = context;

         }

 

-        private Z3Type GetMapType(MapType mapType)

+        private Sort GetMapType(MapType mapType)

         {

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

+            Context z3 = ((Z3Context)container).z3;

             if (!mapTypes.ContainsKey(mapType))

             {

                 Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1");

-                Z3Type domain = GetType(mapType.Arguments[0]);

-                Z3Type range = GetType(mapType.Result);

-                Z3Type typeAst = BuildMapType(domain, range);

+                Sort domain = GetType(mapType.Arguments[0]);

+                Sort range = GetType(mapType.Result);

+                Sort typeAst = BuildMapType(domain, range);

                 mapTypes.Add(mapType, typeAst);

             }

-            Z3Type result;

+            Sort result;

             bool containsKey = mapTypes.TryGetValue(mapType, out result);

             Debug.Assert(containsKey);

             return result;

         }

 

-        private Z3Type GetBvType(BvType bvType)

+        private Sort GetBvType(BvType bvType)

         {

             if (!bvTypes.ContainsKey(bvType))

             {

-                Z3Type typeAst = BuildBvType(bvType);

+                Sort typeAst = BuildBvType(bvType);

                 bvTypes.Add(bvType, typeAst);

             }

-            Z3Type result;

+            Sort result;

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

             Debug.Assert(containsKey);

             return result;

         }

 

-        private Z3Type GetBasicType(BasicType basicType)

+        private Sort GetBasicType(BasicType basicType)

         {

             if (!basicTypes.ContainsKey(basicType))

             {

-                Z3Type typeAst = BuildBasicType(basicType);

+                Sort typeAst = BuildBasicType(basicType);

                 basicTypes.Add(basicType, typeAst);

             }

-            Z3Type result;

+            Sort result;

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

             Debug.Assert(containsKey);

             return result;

         }

 

-        private Z3Type GetCtorType(CtorType ctorType) {

+        private Sort GetCtorType(CtorType ctorType) {

           if (!ctorTypes.ContainsKey(ctorType)) {

-            Z3Type typeAst = BuildCtorType(ctorType);

+            Sort typeAst = BuildCtorType(ctorType);

             ctorTypes.Add(ctorType, typeAst);

           }

-          Z3Type result;

+          Sort result;

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

           Debug.Assert(containsKey);

           return result;

         }

 

-        public virtual Z3Type GetType(Type boogieType) {

+        public virtual Sort GetType(Type boogieType) {

           System.Type type = boogieType.GetType();

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

             return GetBvType((BvType)boogieType);

@@ -155,28 +155,23 @@ namespace Microsoft.Boogie.Z3
             throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");

         }

 

-        private Z3Type WrapType(Sort typeAst)

+        public Sort BuildMapType(Sort domain, Sort range)

         {

-            return new Z3SafeType(typeAst);

+            Context z3 = ((Z3Context)container).z3;

+            Sort typeAst = z3.MkArraySort(domain, range);

+            return typeAst;

         }

 

-        public Z3Type BuildMapType(Z3Type domain, Z3Type range)

+        public Sort BuildBvType(BvType bvType)

         {

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

-            Sort typeAst = z3.MkArraySort(((Z3SafeType)domain).TypeAst, ((Z3SafeType)range).TypeAst);

-            return WrapType(typeAst);

-        }

-

-        public Z3Type BuildBvType(BvType bvType)

-        {

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

+            Context z3 = ((Z3Context)container).z3;

             Sort typeAst = z3.MkBvSort((uint)bvType.Bits);

-            return WrapType(typeAst);

+            return typeAst;

         }

 

-        public Z3Type BuildBasicType(BasicType basicType)

+        public Sort BuildBasicType(BasicType basicType)

         {

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

+            Context z3 = ((Z3Context)container).z3;

             Sort typeAst;

             if (basicType.IsBool)

             {

@@ -188,18 +183,16 @@ namespace Microsoft.Boogie.Z3
             }

             else

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

-            return WrapType(typeAst);

+            return typeAst;

         }

 

-        public Z3Type BuildCtorType(CtorType ctorType) {

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

+        public Sort BuildCtorType(CtorType ctorType) {

+          Context z3 = ((Z3Context)container).z3;

           Sort typeAst;

           if (ctorType.Arguments.Length > 0)

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

           typeAst = z3.MkSort(ctorType.Decl.Name);

-          return WrapType(typeAst);

+          return typeAst;

         }

     }

-

-    public class Z3Type { }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index c2eeb45f..aa47d7e0 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -11,13 +11,14 @@ using System.Collections.Generic;
 using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

+using Microsoft.Z3;

 

 namespace Microsoft.Boogie.Z3

 {

-    public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>

+    public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>

     {

         private Z3apiOpLineariser OpLinObject = null;

-        private IVCExprOpVisitor<Z3TermAst, LineariserOptions> OpLineariser

+        private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser

         {

             get

             {

@@ -29,36 +30,36 @@ namespace Microsoft.Boogie.Z3
         }

 

         internal readonly UniqueNamer namer;

-        internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;

+        internal readonly Dictionary<VCExprVar, Term> letBindings;

         protected Z3Context cm;

 

         public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)

         {

             this.cm = cm;

             this.namer = namer;

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

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

         }

 

-        public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)

+        public Term Linearise(VCExpr expr, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(expr != null);

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

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

         }

 

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

 

-        public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)

+        public Term Visit(VCExprLiteral node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

 

             if (node == VCExpressionGenerator.True)

-                return cm.MakeTrue();

+                return cm.z3.MkTrue();

             else if (node == VCExpressionGenerator.False)

-                return cm.MakeFalse();

+                return cm.z3.MkFalse();

             else if (node is VCExprIntLit)

-                return cm.MakeIntLiteral(((VCExprIntLit)node).Val.ToString());

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

             else

             {

                 Contract.Assert(false);

@@ -66,7 +67,7 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        public Z3TermAst Visit(VCExprNAry node, LineariserOptions options)

+        public Term Visit(VCExprNAry node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

@@ -76,7 +77,7 @@ namespace Microsoft.Boogie.Z3
             if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))

             {

                 // handle these operators without recursion

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

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

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

 

                 IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

@@ -93,10 +94,10 @@ namespace Microsoft.Boogie.Z3
                 return cm.Make(opString, asts);

             }

 

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

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

         }

 

-        public Z3TermAst Visit(VCExprVar node, LineariserOptions options)

+        public Term Visit(VCExprVar node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

@@ -111,7 +112,7 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options)

+        public Term Visit(VCExprQuantifier node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

@@ -123,11 +124,11 @@ namespace Microsoft.Boogie.Z3
                 List<string> varNames;

                 List<Type> varTypes;

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

-                List<Z3PatternAst> patterns;

-                List<Z3TermAst> no_patterns;

+                List<Pattern> patterns;

+                List<Term> no_patterns;

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

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

-                Z3TermAst result;

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

+                Term result;

                 uint weight = 1;

                 string qid = "";

                 int skolemid = 0;

@@ -153,9 +154,9 @@ namespace Microsoft.Boogie.Z3
 

                 switch (node.Quan)

                 {

-                    case Quantifier.ALL:

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

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

-                    case Quantifier.EX:

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

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

                     default:

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

@@ -180,44 +181,44 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

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

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

         {

-            patterns = new List<Z3PatternAst>();

-            no_patterns = new List<Z3TermAst>();

+            patterns = new List<Pattern>();

+            no_patterns = new List<Term>();

             foreach (VCTrigger trigger in triggers)

             {

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

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

                 foreach (VCExpr expr in trigger.Exprs)

                 {

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

-                    Z3TermAst termAst = Linearise(expr, options);

+                    Term termAst = Linearise(expr, options);

                     exprs.Add(termAst);

                 }

                 if (exprs.Count > 0)

                 {

                     if (trigger.Pos)

                     {

-                        Z3PatternAst pattern = cm.MakePattern(exprs);

+                        Pattern pattern = cm.MakePattern(exprs);

                         patterns.Add(pattern);

                     }

                     else

                     {

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

-                        foreach (Z3TermAst expr in exprs)

+                        foreach (Term expr in exprs)

                             no_patterns.Add(expr);

                     }

                 }

             }

         }

 

-        public Z3TermAst Visit(VCExprLet node, LineariserOptions options)

+        public Term Visit(VCExprLet node, LineariserOptions options)

         {

             foreach (VCExprLetBinding b in node)

             {

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

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

                 letBindings.Add(b.V, defAst);

             }

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

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

             foreach (VCExprLetBinding b in node)

             {

                 letBindings.Remove(b.V);

@@ -227,7 +228,7 @@ namespace Microsoft.Boogie.Z3
 

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

 

-        internal class Z3apiOpLineariser : IVCExprOpVisitor<Z3TermAst, LineariserOptions>

+        internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>

         {

             [ContractInvariantMethod]

             void ObjectInvariant()

@@ -245,13 +246,13 @@ namespace Microsoft.Boogie.Z3
 

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

 

-            private Z3TermAst WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)

+            private Term WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(op != null);

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

 

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

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

                 foreach (VCExpr e in terms)

                 {

                     Contract.Assert(e != null);

@@ -262,51 +263,51 @@ namespace Microsoft.Boogie.Z3
 

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

 

-            public Z3TermAst VisitNotOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitNotOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("NOT", node, options);

             }

 

-            public Z3TermAst VisitEqOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitEqOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("EQ", node, options);

             }

 

-            public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("NEQ", node, options);

             }

 

-            public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitAndOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("AND", node, options);  

             }

 

-            public Z3TermAst VisitOrOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitOrOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("OR", node, options); 

             }

 

-            public Z3TermAst VisitImpliesOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 if (options.InverseImplies)

                 {

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

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

 

                     args.Add(ExprLineariser.Linearise(node[1], options));

-                    List<Z3TermAst> t = new List<Z3TermAst>();

+                    List<Term> t = new List<Term>();

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

                     args.Add(ExprLineariser.cm.Make("NOT", t));

                     return ExprLineariser.cm.Make("OR", args);

@@ -317,7 +318,7 @@ namespace Microsoft.Boogie.Z3
                 }

             }

 

-            public Z3TermAst VisitDistinctOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -328,7 +329,7 @@ namespace Microsoft.Boogie.Z3
                 }

                 else

                 {

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

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

                     foreach (VCExpr e in node)

                     {

                         Contract.Assert(e != null);

@@ -338,7 +339,7 @@ namespace Microsoft.Boogie.Z3
                 }

             }

 

-            public Z3TermAst VisitLabelOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -347,73 +348,103 @@ namespace Microsoft.Boogie.Z3
                 return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); 

             }

 

-            public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

                 foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);

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

                 }

-                return ExprLineariser.cm.MakeArraySelect(args);

+

+                Term[] unwrapChildren = args.ToArray();

+                return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]);

                 // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args);

             }

 

-            public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

                 foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);

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

                 }

-                return ExprLineariser.cm.MakeArrayStore(args);

+

+                Term[] unwrapChildren = args.ToArray();

+                return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);

                 // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args);

             }

 

-            public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitBvOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("$make_bv" + node.Type.BvBits, node, options);

+                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 Z3TermAst VisitBvExtractOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(SimplifyLikeExprLineariser.BvExtractOpName(node), node, options);

+            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 Z3TermAst VisitBvConcatOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(SimplifyLikeExprLineariser.BvConcatOpName(node), node, options);

+            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 Z3TermAst VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

 

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

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

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

                 args.Add(ExprLineariser.Linearise(node[1], options));

                 args.Add(ExprLineariser.Linearise(node[2], options));

                 return ExprLineariser.cm.Make("ITE", args);

             }

 

-            public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(node != null);

                 Contract.Requires(options != null);

                 VCExprCustomOp op = (VCExprCustomOp)node.Op;

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

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

                 foreach (VCExpr arg in node)

                 {

                     args.Add(ExprLineariser.Linearise(arg, options));

@@ -421,7 +452,7 @@ namespace Microsoft.Boogie.Z3
                 return ExprLineariser.cm.Make(op.Name, args);

             }

 

-            public Z3TermAst VisitAddOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitAddOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -435,77 +466,77 @@ namespace Microsoft.Boogie.Z3
                 }

             }

 

-            public Z3TermAst VisitSubOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitSubOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("-", node, options);

             }

 

-            public Z3TermAst VisitMulOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitMulOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("*", node, options);

             }

 

-            public Z3TermAst VisitDivOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitDivOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("/", node, options);

             }

 

-            public Z3TermAst VisitModOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitModOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("%", node, options);

             }

 

-            public Z3TermAst VisitLtOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitLtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<", node, options);

             }

 

-            public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitLeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<=", node, options);

             }

 

-            public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitGtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication(">", node, options);

             }

 

-            public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitGeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication(">=", node, options);

             }

 

-            public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<:", node, options);

             }

 

-            public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

+            public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<::", node, options);

             }

 

-            public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -516,7 +547,7 @@ namespace Microsoft.Boogie.Z3
                 string bvzName = op.Func.FindStringAttribute("external");

                 if (bvzName != null) funcName = bvzName;

 

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

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

                 foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 05cc8f9f..e02243ce 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -169,8 +169,6 @@
     </Compile>

     <Compile Include="ContextLayer.cs" />

     <Compile Include="ProverLayer.cs" />

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

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

     <Compile Include="TypeAdapter.cs">

       <SubType>Code</SubType>

     </Compile>