9 files changed, 599 insertions, 842 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index af0926fe..ec28a910 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -192,6 +192,10 @@
       <Project>{A598ED5A-93AD-4125-A555-3921A2F936FA}</Project>
       <Name>TPTP</Name>
     </ProjectReference>
+    <ProjectReference Include="..\Provers\Z3api\Z3api.csproj">
+      <Project>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</Project>
+      <Name>Z3api</Name>
+    </ProjectReference>
     <ProjectReference Include="..\Provers\Z3\Z3.csproj">
       <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
       <Name>Z3</Name>
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>
diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat
index 08a27b9b..e9bc968e 100644
--- a/Test/z3api/runtest.bat
+++ b/Test/z3api/runtest.bat
@@ -3,17 +3,14 @@ setlocal
 
 set BGEXE=..\..\Binaries\Boogie.exe
 
-for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog14.bpl boog16.bpl boog17.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f
 )
-REM boog8.bpl
+
 REM boog12.bpl
-REM boog14.bpl
 REM boog15.bpl
-REM boog16.bpl
-REM boog17.bpl
 
 REM boog19.bpl
 REM boog23.bpl