Added the port of Z3api. It is simply a port to the latest version of Microsoft.Z3.dll and to C#. It does not work yet.

author: qadeer <unknown> 2010-08-20 21:52:05 +0000
committer: qadeer <unknown> 2010-08-20 21:52:05 +0000
commit: 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (patch)
tree: 9ce338c9e4d2ad54d759b434248b7761a8c75b6d
parent: 27cc9c245d21151a78c95cead4801ad130557743 (diff)
8 files changed, 2191 insertions, 0 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 29d8afee..bb127224 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -27,6 +27,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "VCGeneratio
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csproj", "{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3api", "Provers\Z3api\Z3api.csproj", "{966DD87B-A29D-4F3C-9406-F680A61DC0E0}"
+EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
 		Debug|.NET = Debug|.NET
@@ -164,6 +166,16 @@ Global
 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Release|Any CPU.Build.0 = Release|Any CPU
 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
 		{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|.NET.ActiveCfg = Debug|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|.NET.ActiveCfg = Release|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.Build.0 = Release|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Mixed Platforms.Build.0 = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE
@@ -173,5 +185,6 @@ Global
 		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
 		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
+		{966DD87B-A29D-4F3C-9406-F680A61DC0E0} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
 	EndGlobalSection
 EndGlobal
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
new file mode 100644
index 00000000..532b1932
--- /dev/null
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -0,0 +1,385 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+    public class Z3Config
+    {
+        private Config config = new Config();
+        private int counterexamples;
+        private string logFilename;
+        private List<string> debugTraces = new List<string>();
+
+        public void SetPartialModels(bool enabled)
+        {
+            config.SetParamValue("PARTIAL_MODELS", (enabled ? "true" : "false"));
+        }
+        public void SetModelCompletion(bool enabled)
+        {
+            config.SetParamValue("MODEL_VALUE_COMPLETION", (enabled ? "true" : "false"));
+        }
+
+        public void SetHideUnusedPartitions(bool enabled)
+        {
+            config.SetParamValue("HIDE_UNUSED_PARTITIONS", (enabled ? "true" : "false"));
+        }
+
+        public void SetMAM(string mamNumber)
+        {
+            config.SetParamValue("MAM", mamNumber);
+        }
+
+        public void SetModel(bool enabled)
+        {
+            config.SetParamValue("MODEL", (enabled ? "true" : "false"));
+        }
+
+        public void SetSoftTimeout(string timeout)
+        {
+            config.SetParamValue("SOFT_TIMEOUT", timeout);
+        }
+
+        public void SetTypeCheck(bool enabled)
+        {
+            config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false"));
+        }
+
+        public void SetReflectBvOps(bool enabled)
+        {
+            config.SetParamValue("REFLECT_BV_OPS", (enabled ? "true" : "false"));
+        }
+
+        public void SetCounterExample(int counterexample)
+        {
+            this.counterexamples = counterexample;
+        }
+
+        public void SetLogFilename(string filename)
+        {
+            this.logFilename = filename;
+        }
+
+        public Config Config
+        {
+            get { return this.config; }
+        }
+        public int Counterexamples
+        {
+            get { return this.counterexamples; }
+        }
+        public string LogFilename
+        {
+            get { return this.logFilename; }
+        }
+
+        public void EnableDebugTrace(string debugTrace)
+        {
+            this.debugTraces.Add(debugTrace);
+        }
+
+        public List<string> DebugTraces
+        {
+            get { return this.debugTraces; }
+        }
+    }
+
+    public abstract class Z3ContextFactory
+    {
+
+        public static Z3Context BuildZ3Context(Z3Config config, VCExpressionGenerator gen)
+        {
+            return new Z3SafeContext(config, gen);
+        }
+    }
+
+
+    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 vc);
+        void AddConjecture(VCExpr vc);
+        void AddSmtlibString(string smtlibString);
+        string GetDeclName(Z3ConstDeclAst constDeclAst);
+        Z3PatternAst MakePattern(List<Z3TermAst> exprs);
+        Z3TermAst MakeForall(List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);
+        Z3TermAst MakeExists(List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);
+        List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels);
+        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);
+        Z3TermAst MakeBoundVariable(uint deBruijnIndex, 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);
+    }
+
+    internal class PartitionMap
+    {
+        private Dictionary<int, int> partitionToValueHash = new Dictionary<int, int>();
+        private int partitionCounter = FAKE_PARTITION;
+        public int GetPartition(int valueHash)
+        {
+            if (partitionToValueHash.ContainsKey(valueHash))
+            {
+                partitionCounter++;
+                partitionToValueHash.Add(valueHash, partitionCounter);
+            }
+            int partition;
+            partitionToValueHash.TryGetValue(valueHash, out partition);
+            return partition;
+        }
+        public int GetPartitionCount()
+        {
+            return partitionCounter + 1;
+        }
+
+        private const int FAKE_PARTITION = 0;
+        public int GetFakePartition()
+        {
+            return FAKE_PARTITION;
+        }
+    }
+
+    internal class BacktrackDictionary<K, V>
+    {
+        private Dictionary<K, V> dictionary = new Dictionary<K, V>();
+        private Stack<List<K>> keyStack = new Stack<List<K>>();
+
+        public BacktrackDictionary()
+        {
+            CreateBacktrackPoint();
+        }
+
+        public bool TryGetValue(K key, out V val)
+        {
+            return dictionary.TryGetValue(key, out val);
+        }
+
+        public void Add(K key, V v)
+        {
+            if (dictionary.ContainsKey(key))
+            {
+                dictionary.Remove(key);
+            }
+            dictionary.Add(key, v);
+            keyStack.Peek().Add(key);
+        }
+
+        public bool ContainsKey(K k)
+        {
+            return dictionary.ContainsKey(k);
+        }
+
+        public void CreateBacktrackPoint()
+        {
+            keyStack.Push(new List<K>());
+        }
+
+        public void Backtrack()
+        {
+            List<K> keysToErase = keyStack.Pop();
+            foreach (K key in keysToErase)
+            {
+                dictionary.Remove(key);
+            }
+            if (keyStack.Count == 0)
+                this.CreateBacktrackPoint();
+        }
+
+        public IEnumerator GetEnumerator()
+        {
+            return dictionary.Keys.GetEnumerator();
+        }
+    }
+
+    internal class BoogieErrorModelBuilder
+    {
+        private Z3Context container;
+        private PartitionMap partitionMap;
+
+        public BoogieErrorModelBuilder(Z3Context container)
+        {
+            this.container = container;
+            this.partitionMap = new PartitionMap();
+        }
+
+        private Dictionary<string, object> CreateConstantToValue(Model z3Model)
+        {
+            Dictionary<string, object> constantToValue = new Dictionary<string, object>();
+            foreach (FuncDecl c in z3Model.GetModelConstants())
+            {
+                string c_name = container.GetDeclName(new Z3TypeSafeConstDecl(c));
+                Term v = z3Model.Eval(c, new Term[0]);
+                Sort s = v.GetSort();
+                Context ctx = new Context(null); // placeholder.
+                Sort boolSort = ctx.MkBoolSort();
+                Sort intSort = ctx.MkIntSort();
+
+                if (s == boolSort)
+                {
+                    constantToValue.Add(c_name, ctx.GetBoolValue(v));
+                }
+                else if (s == intSort)
+                {
+                    int i;
+                    if (ctx.TryGetNumeralInt(v, out i))
+                        constantToValue.Add(c_name, i);
+                    // TBD: 
+                    // ctx.GetNumeralValueString(v)?
+                }
+                else
+                {
+                    constantToValue.Add(c_name, null);
+                }
+            }
+            return constantToValue;
+        }
+
+        private Dictionary<string, int> CreateConstantToPartition(Model z3Model)
+        {
+            Dictionary<string, int> constantToPartition = new Dictionary<string, int>();
+            foreach (FuncDecl c in z3Model.GetModelConstants())
+            {
+                string c_name = container.GetDeclName(new Z3TypeSafeConstDecl(c));
+                constantToPartition.Add(c_name, partitionMap.GetPartition(z3Model.Eval(c, new Term[0]).GetHashCode()));
+            }
+            return constantToPartition;
+        }
+
+        private Dictionary<string, List<List<int>>> CreateFunctionToPartition(Model z3Model)
+        {
+            Dictionary<string, List<List<int>>> functionToPartition = new Dictionary<string, List<List<int>>>();
+
+            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));
+                FunctionGraph graph = kv.Value;
+                foreach (FunctionEntry entry in graph.Entries)
+                {
+                    List<int> tuple = new List<int>();
+                    foreach (Term v in entry.Arguments)
+                    {
+                        tuple.Add(partitionMap.GetPartition(z3Model.Eval(v).GetHashCode()));
+                    }
+                    tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result).GetHashCode()));
+                    f_tuples.Add(tuple);
+                }
+                List<int> else_tuple = new List<int>();
+                else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else).GetHashCode()));
+                f_tuples.Add(else_tuple);
+                functionToPartition.Add(f_name, f_tuples);
+            }
+            return functionToPartition;
+        }
+
+        private List<List<string>> ReverseConstantToPartition(Dictionary<string, int> map, int partitionCount)
+        {
+            List<string>[] reverse = new List<string>[partitionCount];
+            foreach (KeyValuePair<string, int> entry in map)
+            {
+                List<string> v = reverse[entry.Value];
+                if (v == null)
+                {
+                    v = new List<string>();
+                    reverse[entry.Value] = v;
+                }
+                v.Add(entry.Key);
+            }
+
+            List<List<string>> result = new List<List<string>>();
+            for (int i = 0; i < reverse.Length; i++)
+            {
+                if (reverse[i] == null)
+                    result.Add(new List<string>());
+                else
+                    result.Add(reverse[i]);
+            }
+            return result;
+        }
+
+        private List<Object> CreatePartitionToValue(Dictionary<string, int> constantToPartition, Dictionary<string, object> constantToValue, int partitionCount)
+        {
+            Object[] partitionToValue = new Object[partitionCount];
+            foreach (string constantName in constantToValue.Keys)
+            {
+                int partition;
+                object objectValue;
+                constantToPartition.TryGetValue(constantName, out partition);
+                constantToValue.TryGetValue(constantName, out objectValue);
+                partitionToValue[partition] = objectValue;
+            }
+            List<Object> result = new List<Object>();
+            for (int j = 0; j < partitionToValue.Length; j++)
+            {
+                result.Add(partitionToValue[j]);
+            }
+            return result;
+        }
+
+        private Dictionary<object, int> CreateValueToPartition(Model z3Model)
+        {
+            // TODO Implement this method
+            return new Dictionary<object, int>();
+        }
+
+        public Z3ErrorModel BuildBoogieModel(Model z3Model)
+        {
+            partitionMap = new PartitionMap();
+
+            Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);
+            Dictionary<string, object> constantToValue = CreateConstantToValue(z3Model);
+            Dictionary<string, List<List<int>>> functionToPartition = CreateFunctionToPartition(z3Model);
+            Dictionary<object, int> valueToPartition = CreateValueToPartition(z3Model);
+
+            int partitionCount = partitionMap.GetPartitionCount();
+            List<List<string>> partitionToConstant = ReverseConstantToPartition(constantToPartition, partitionCount);
+            List<Object> partitionToValue = CreatePartitionToValue(constantToPartition, constantToValue, partitionCount);
+
+            return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition);
+        }
+
+    }
+
+    public class Z3ErrorModelAndLabels
+    {
+        private Z3ErrorModel _errorModel;
+        private List<string> _relevantLabels;
+        public Z3ErrorModel ErrorModel
+        {
+            get { return this._errorModel; }
+        }
+        public List<string> RelevantLabels
+        {
+            get { return this._relevantLabels; }
+        }
+        public Z3ErrorModelAndLabels(Z3ErrorModel errorModel, List<string> relevantLabels)
+        {
+            this._errorModel = errorModel;
+            this._relevantLabels = relevantLabels;
+        }
+    }
+}
+\ No newline at end of file
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
new file mode 100644
index 00000000..02362edf
--- /dev/null
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -0,0 +1,253 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+using TypeAst = System.IntPtr;
+using TermAst = System.IntPtr;
+using ConstDeclAst = System.IntPtr;
+using ConstAst = System.IntPtr;
+using Value = System.IntPtr;
+using PatternAst = System.IntPtr;
+
+namespace Microsoft.Boogie.Z3
+{
+    public class Z3ThreadTheoremProver : ProverInterface
+    {
+        protected DeclFreeProverContext ctx;
+        protected VCExpressionGenerator gen;
+        public override ProverContext Context
+        {
+            get { return this.ctx; }
+        }
+        public override VCExpressionGenerator VCExprGen
+        {
+            get { return this.gen; }
+        }
+
+        private int timeout;
+        private Z3Context cm;
+
+        public Z3ThreadTheoremProver(Z3InstanceOptions proverOptions)
+            : base()
+        {
+            gen = new VCExpressionGenerator();
+
+            string codebaseString = Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
+            string backgroundPredicates;
+
+            // Initialize '_backgroundPredicates'
+            string univBackPredPath = Path.Combine(codebaseString,
+                // yes, using .NeedsTypes here is an ugly hack...
+                "Z3API_UnivBackPred.smt");
+            using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
+            {
+                backgroundPredicates = reader.ReadToEnd();
+            }
+
+            Z3Config config = BuildConfig(timeout, true);
+            Z3Context cm = Z3ContextFactory.BuildZ3Context(config, gen);
+            Z3ThreadProverContext ctx = new Z3ThreadProverContext(gen, cm);
+
+            this.cm = cm;
+            cm.AddSmtlibString(backgroundPredicates);
+            this.z3ContextIsUsed = false;
+        }
+
+        private static Z3Config BuildConfig(int timeout, bool nativeBv)
+        {
+            Z3Config config = new Z3Config();
+            config.SetPartialModels(true);
+            config.SetModelCompletion(false);
+            config.SetHideUnusedPartitions(false);
+            config.SetModel(true);
+
+            if (0 <= CommandLineOptions.Clo.ProverCCLimit)
+            {
+                config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);
+            }
+
+            if (0 <= timeout)
+            {
+                config.SetSoftTimeout(timeout.ToString());
+            }
+
+            config.SetTypeCheck(true);
+            if (nativeBv)
+                config.SetReflectBvOps(true);
+
+            return config;
+        }
+
+        private bool z3ContextIsUsed;
+
+        public void PushAxiom(VCExpr axiom)
+        {
+            cm.CreateBacktrackPoint();
+            cm.AddAxiom((VCExpr)axiom);
+        }
+        private void PushConjecture(VCExpr conjecture)
+        {
+            cm.CreateBacktrackPoint();
+            cm.AddConjecture((VCExpr)conjecture);
+        }
+
+        public void PrepareCheck(string descriptiveName, VCExpr vc)
+        {
+            PushAxiom(ctx.Axioms);
+            PushConjecture(vc);
+        }
+
+        public void BeginPreparedCheck()
+        {
+            outcome = Outcome.Undetermined;
+            outcome = cm.Check(out z3LabelModels);
+        }
+
+        public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
+        {
+            if (z3ContextIsUsed)
+            {
+                cm.Backtrack();
+            }
+            else
+            {
+                cm.AddAxiom((VCExpr)ctx.Axioms);
+                z3ContextIsUsed = true;
+            }
+
+            cm.CreateBacktrackPoint();
+            cm.AddConjecture((VCExpr)vc);
+
+            BeginPreparedCheck();
+        }
+
+        private Outcome outcome;
+        private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();
+        private UnexpectedProverOutputException proverException = null;
+
+        [NoDefaultContract]
+        public override Outcome CheckOutcome(ErrorHandler handler)
+        {
+            if (outcome == Outcome.Invalid)
+            {
+                foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
+                {
+                    List<string> unprefixedLabels = RemovePreffixes(z3LabelModel.RelevantLabels);
+                    handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
+                }
+            }
+            return outcome;
+        }
+
+        public void CreateBacktrackPoint()
+        {
+            cm.CreateBacktrackPoint();
+        }
+        override public void Pop()
+        {
+            cm.Backtrack();
+        }
+
+        private List<string> RemovePreffixes(List<string> labels)
+        {
+            List<string> result = new List<string>();
+            foreach (string label in labels)
+            {
+                if (label.StartsWith("+"))
+                {
+                    result.Add(label.Substring(1));
+                }
+                else if (label.StartsWith("|"))
+                {
+                    result.Add(label.Substring(1));
+                }
+                else if (label.StartsWith("@"))
+                {
+                    result.Add(label.Substring(1));
+                }
+                else
+                    throw new Exception("Unknown preffix in label " + label);
+            }
+            return result;
+        }
+
+    }
+
+    public class Z3ThreadProverContext : DeclFreeProverContext
+    {
+
+        private Z3Context cm;
+
+        public Z3ThreadProverContext(VCExpressionGenerator gen, Z3Context cm)
+            : base(gen, null)
+        {
+            this.cm = cm;
+        }
+
+        public override void DeclareType(TypeCtorDecl t, string attributes)
+        {
+            base.DeclareType(t, attributes);
+            cm.DeclareType(t.Name);
+        }
+
+        public override void DeclareConstant(Constant c, bool uniq, string attributes)
+        {
+            base.DeclareConstant(c, uniq, attributes);
+            cm.DeclareConstant(c.Name, c.TypedIdent.Type);
+        }
+
+
+        public override void DeclareFunction(Function f, string attributes)
+        {
+            base.DeclareFunction(f, attributes);
+            List<Type> domain = new List<Type>();
+            foreach (Variable v in f.InParams)
+            {
+                domain.Add(v.TypedIdent.Type);
+            }
+            if (f.OutParams.Length != 1)
+                throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters.");
+            Type range = f.OutParams[0].TypedIdent.Type;
+
+            cm.DeclareFunction(f.Name, domain, range);
+        }
+
+        public override void DeclareGlobalVariable(GlobalVariable v, string attributes)
+        {
+            base.DeclareGlobalVariable(v, attributes);
+            cm.DeclareConstant(v.Name, v.TypedIdent.Type);
+        }
+    }
+}
+
+namespace Microsoft.Boogie.Z3api
+{
+
+    public class Factory : ProverFactory
+    {
+        public override object SpawnProver(ProverOptions popts, object ctxt)
+        {
+            Z3InstanceOptions options = (Z3InstanceOptions) popts;
+            if (CommandLineOptions.Clo.BracketIdsInVC < 0)
+            {
+                CommandLineOptions.Clo.BracketIdsInVC = 0;
+            }
+
+            return new Z3ThreadTheoremProver(options);
+        }
+
+        public override object NewProverContext(ProverOptions options)
+        {
+            throw new NotImplementedException();
+        }
+    }
+}
+\ No newline at end of file
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
new file mode 100644
index 00000000..26e7385d
--- /dev/null
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -0,0 +1,596 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+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>();
+
+        private Context z3;
+        private Z3Config config;
+
+        public void CreateBacktrackPoint()
+        {
+            symbols.CreateBacktrackPoint();
+            constants.CreateBacktrackPoint();
+            functions.CreateBacktrackPoint();
+            labels.CreateBacktrackPoint();
+            z3.Push();
+        }
+
+        public void Backtrack()
+        {
+            z3.Pop();
+            labels.Backtrack();
+            functions.Backtrack();
+            constants.Backtrack();
+            symbols.Backtrack();
+        }
+
+        public void AddAxiom(VCExpr vc)
+        {
+            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);
+            Z3TermAst z3ast = (Z3TermAst)vc.Accept(visitor, null);
+            Term term = Unwrap(z3ast);
+            z3.AssertCnstr(term);
+        }
+
+        public void AddConjecture(VCExpr vc)
+        {
+            VCExpr not_vc = (VCExpr)this.gen.Not(vc);
+            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);
+            Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, null);
+            Term term = Unwrap(z3ast);
+            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)
+            {
+                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;
+        }
+
+        private const int DEFAULT_QUANTIFIER_WEIGHT = 0;
+
+        public Z3TermAst MakeForall(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);
+            List<Sort> z3Types = GetTypes(boogieTypes);
+            List<Symbol> symbols = GetSymbols(varNames);
+            Term unwrapBody = Unwrap(body);
+
+            Term termAst = z3.MkQuantifier(true,
+                             DEFAULT_QUANTIFIER_WEIGHT,
+                             unwrapPatterns.ToArray(),
+                             unwrapNoPatterns.ToArray(),
+                             z3Types.ToArray(),
+                             symbols.ToArray(),
+                             unwrapBody);
+
+            return Wrap(termAst);
+        }
+
+        public Z3TermAst MakeExists(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);
+            List<Sort> z3Types = GetTypes(boogieTypes);
+            List<Symbol> symbols = GetSymbols(varNames);
+            Term unwrapBody = Unwrap(body);
+
+            Term termAst = z3.MkQuantifier(false,
+                                                  DEFAULT_QUANTIFIER_WEIGHT,
+                                                  unwrapPatterns.ToArray(),
+                                                  unwrapNoPatterns.ToArray(),
+                                                  z3Types.ToArray(),
+                                                  symbols.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;
+        }
+
+        public List<string> BuildConflictClause(Z3LabeledLiterals z3relevantLabels)
+        {
+            List<string> lbls = new List<string>();
+            LabeledLiterals relevantLabels = ((Z3SafeLabeledLiterals)z3relevantLabels).LabeledLiterals;
+            uint num_labels = relevantLabels.GetNumLabels();
+            for (uint i = 0; i < num_labels; ++i)
+            {
+                Symbol sym = relevantLabels.GetLabel(i);
+                string labelName = z3.GetSymbolString(sym);
+                if (labelName.StartsWith("@"))
+                {
+                    relevantLabels.Disable(i);
+                }
+                lbls.Add(labelName);
+            }
+            z3.BlockLiterals(relevantLabels);
+
+            return lbls;
+        }
+
+        private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels)
+        {
+            BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this);
+            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)
+        {
+            boogieErrors = new List<Z3ErrorModelAndLabels>();
+            LBool outcome = LBool.Undef;
+            z3.Push();
+            while (boogieErrors.Count < this.config.Counterexamples)
+            {
+                Model z3Model;
+                //System.Console.WriteLine("Check Begin");
+                outcome = z3.CheckAndGetModel(out z3Model);
+                //System.Console.WriteLine("Check End");
+                if (outcome == LBool.True)
+                {
+                    Debug.Assert(z3Model != null);
+
+                    LabeledLiterals labels = z3.GetRelevantLabels();
+                    List<string> labelStrings = BuildConflictClause(new Z3SafeLabeledLiterals(labels));
+                    boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
+                    labels.Dispose();
+
+                    if (z3Model != null)
+                        z3Model.Dispose();
+                }
+                else
+                    break;
+            }
+            z3.Pop();
+
+            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 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");
+        }
+
+        private VCExpressionGenerator gen;
+
+        internal Z3SafeContext(Z3Config config, VCExpressionGenerator gen)
+        {
+            Context z3 = new Context(config.Config);
+            // TBD: z3.EnableArithmetic();
+            if (config.LogFilename != null)
+                z3.OpenLog(config.LogFilename);
+            foreach (string tag in config.DebugTraces)
+                z3.EnableDebugTrace(tag);
+            this.z3 = z3;
+            this.config = config;
+            this.tm = new Z3TransformerTypeCache(new Z3SafeTypeBuilder(z3), new IntTransformer());
+            this.gen = gen;
+        }
+
+        public void DeclareType(string 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));
+        }
+
+        public Z3TermAst MakeBoundVariable(uint deBruijnIndex, Type boogieType)
+        {
+            Z3Type typeAst = tm.GetType(boogieType);
+            Sort unwrapTypeAst = Unwrap(typeAst);
+
+            Term boundVariable = z3.MkBound(deBruijnIndex, unwrapTypeAst);
+            Z3TermAst wrappedBoundVariable = Wrap(boundVariable);
+            return wrappedBoundVariable;
+        }
+
+        private Z3TypeCachedBuilder tm;
+
+        public void DeclareFunction(string functionName, List<Type> domain, Type range)
+        {
+            Symbol symbolAst = GetSymbol(functionName);
+
+            List<Sort> domainAst = new List<Sort>();
+            foreach (Type domainType in domain)
+            {
+                Z3Type type = tm.GetType(domainType);
+                Sort unwrapType = Unwrap(type);
+                domainAst.Add(unwrapType);
+            }
+            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);
+        }
+
+        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());
+            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 class Z3SafeTypeBuilder : Z3TypeBuilder
+    {
+
+        protected Context z3;
+
+        public Z3SafeTypeBuilder(Context z3)
+        {
+            this.z3 = z3;
+        }
+
+        private Z3Type WrapType(Sort typeAst)
+        {
+            return new Z3SafeType(typeAst);
+        }
+
+        public Z3Type BuildBvType(BvType bvType)
+        {
+            Sort typeAst = z3.MkBvSort((uint)bvType.Bits);
+            return WrapType(typeAst);
+        }
+
+        public Z3Type BuildBasicType(BasicType basicType)
+        {
+            Sort typeAst;
+            if (basicType.IsBool)
+            {
+                typeAst = z3.MkBoolSort();
+            }
+            else if (basicType.IsInt)
+            {
+                typeAst = z3.MkIntSort();
+            }
+            else
+                throw new Exception("Unknown Basic Type " + basicType.ToString());
+            return WrapType(typeAst);
+        }
+
+    }
+}
+\ No newline at end of file
diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
new file mode 100644
index 00000000..80f1776e
--- /dev/null
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -0,0 +1,74 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3 {
+  public class Z3StubContext:Z3Context {
+    class Z3StubPatternAst: Z3PatternAst {}
+    class Z3StubTermAst: Z3TermAst {}
+    class Z3StubLabeledLiterals: Z3LabeledLiterals {}
+  
+    public void CreateBacktrackPoint(){}
+    public void Backtrack(){}
+    public void AddAxiom(VCExpr vc) {}
+    public void AddConjecture(VCExpr vc){}
+    public void AddSmtlibString(string smtlibString) {}
+    public string GetDeclName(Z3ConstDeclAst constDeclAst) {
+      return "";
+    }
+    public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {
+      return new Z3StubPatternAst();
+    }
+    public Z3TermAst MakeForall(List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeExists(List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {
+      return new Z3StubTermAst();
+    }
+    public List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels) {
+      return new List<string>();
+    }
+    public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {
+      boogieErrors = new List<Z3ErrorModelAndLabels>();
+      return ProverInterface.Outcome.Undetermined;
+    }
+    public void TypeCheckBool(Z3TermAst t){}
+    public void TypeCheckInt(Z3TermAst t){}
+    public void DeclareType(string typeName) {}
+    public void DeclareConstant(string constantName, Type boogieType) {}
+    public Z3TermAst MakeBoundVariable(uint deBruijnIndex,Type boogieType) {
+      return new Z3StubTermAst();
+    }
+    public void DeclareFunction(string functionName, List<Type> domain, Type range) {}
+    public Z3TermAst GetConstant(string constantName, Type constantType) {
+      return new Z3StubTermAst();
+    }    
+    public Z3TermAst MakeIntLiteral(string numeral) {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeTrue() {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeFalse() {
+      return new Z3StubTermAst();
+    }
+    public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) {
+      return new Z3StubTermAst();
+    }
+    public Z3LabeledLiterals GetRelevantLabels() {
+      return new Z3StubLabeledLiterals();
+    }
+    public Z3TermAst Make(string op, List<Z3TermAst> children) {
+      return new Z3StubTermAst();
+    }
+  }
+}
+\ No newline at end of file
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
new file mode 100644
index 00000000..553205b1
--- /dev/null
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -0,0 +1,163 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Z3;
+using Microsoft.Z3;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+    internal class Z3TypeCachedBuilder
+    {
+        private class BvTypeComparator : IEqualityComparer<BvType>
+        {
+            public bool Equals(BvType x, BvType y)
+            {
+                return x.Bits == y.Bits;
+            }
+            public int GetHashCode(BvType bvType)
+            {
+                return bvType.Bits;
+            }
+        }
+
+        private class BasicTypeComparator : IEqualityComparer<BasicType>
+        {
+            public bool Equals(BasicType x, BasicType y)
+            {
+                return (x.IsBool == y.IsBool) &&
+                       (x.IsInt == y.IsInt);
+            }
+
+            public int GetHashCode(BasicType basicType)
+            {
+                if (basicType.IsBool)
+                    return 1;
+                else if (basicType.IsInt)
+                    return 2;
+                else
+                    throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");
+            }
+        }
+
+        private Z3TypeBuilder builder;
+        private Dictionary<BvType, Z3Type> bvTypes = new Dictionary<BvType, Z3Type>(new BvTypeComparator());
+        private Dictionary<BasicType, Z3Type> basicTypes = new Dictionary<BasicType, Z3Type>(new BasicTypeComparator());
+
+        public Z3TypeCachedBuilder(Z3TypeBuilder builder)
+        {
+            this.builder = builder;
+        }
+
+        private Z3Type GetBvType(BvType bvType)
+        {
+            if (bvTypes.ContainsKey(bvType))
+            {
+                Z3Type typeAst = builder.BuildBvType(bvType);
+                bvTypes.Add(bvType, typeAst);
+            }
+            Z3Type result;
+            bool containsKey = bvTypes.TryGetValue(bvType, out result);
+            Debug.Assert(containsKey);
+            return result;
+        }
+
+        private Z3Type GetBasicType(BasicType basicType)
+        {
+            if (basicTypes.ContainsKey(basicType))
+            {
+                Z3Type typeAst = builder.BuildBasicType(basicType);
+                basicTypes.Add(basicType, typeAst);
+            }
+            Z3Type result;
+            bool containsKey = basicTypes.TryGetValue(basicType, out result);
+            Debug.Assert(containsKey);
+            return result;
+        }
+
+        public virtual Z3Type GetType(Type boogieType)
+        {
+            if (boogieType.GetType().Equals(typeof(BvType)))
+                return GetBvType((BvType)boogieType);
+            else if (boogieType.GetType().Equals(typeof(BasicType)))
+                return GetBasicType((BasicType)boogieType);
+            else
+                throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
+        }
+    }
+
+    public class Z3Type { }
+
+    interface Z3TypeBuilder
+    {
+        Z3Type BuildBvType(BvType bvType);
+        Z3Type BuildBasicType(BasicType basicType);
+    }
+
+
+    internal class Z3TransformerTypeCache : Z3TypeCachedBuilder
+    {
+
+        private BoogieTypeTransformer transformer;
+
+        public Z3TransformerTypeCache(Z3TypeBuilder builder, BoogieTypeTransformer transformer)
+            : base(builder)
+        {
+            this.transformer = transformer;
+        }
+
+        public override Z3Type GetType(Type boogieType)
+        {
+            Type resolvedBoogieType = transformer.TransformType(boogieType);
+            return base.GetType(resolvedBoogieType);
+        }
+    }
+
+    internal abstract class BoogieTypeTransformer
+    {
+
+        protected abstract Type TransformBvType(BvType boogieType);
+        protected abstract Type TransformBasicType(BasicType boogieType);
+
+        public Type TransformType(Type boogieType)
+        {
+            return Dispatch(boogieType);
+        }
+
+        private Type Dispatch(Type boogieType)
+        {
+            if (boogieType.GetType().Equals(typeof(BvType)))
+                return TransformBvType((BvType)boogieType);
+            else if (boogieType.GetType().Equals(typeof(BasicType)))
+                return TransformBasicType((BasicType)boogieType);
+            else
+                throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
+        }
+
+    }
+
+    internal class IntTransformer : BoogieTypeTransformer
+    {
+
+        protected override Type TransformBvType(BvType bvType)
+        {
+            // registerBvType(bvType.Bits)
+            return BasicType.Int;
+        }
+
+        protected override Type TransformBasicType(BasicType boogieType)
+        {
+            if (boogieType.IsBool)
+            {
+                // registerBool()
+            }
+            return BasicType.Int;
+        }
+    }
+}
+\ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
new file mode 100644
index 00000000..ca32a824
--- /dev/null
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -0,0 +1,610 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+    // Lineariser for expressions. The result (bool) is currently not used for anything
+    public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>
+    {
+        private Z3apiOpLineariser OpLinObject = null;
+        private IVCExprOpVisitor<Z3TermAst, LineariserOptions> OpLineariser
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
+                if (OpLinObject == null)
+                    OpLinObject = new Z3apiOpLineariser(this);
+                return OpLinObject;
+            }
+        }
+
+        internal readonly UniqueNamer Namer;
+        private readonly TextWriter wr;
+
+        protected Z3Context cm;
+
+        protected Stack<Dictionary<string, VCExpr>> lets;
+        protected Stack<List<string>> binders;
+
+        public Z3apiExprLineariser(Z3Context cm)
+        {
+            this.cm = cm;
+            Stack<Dictionary<string, VCExpr>> lets = new Stack<Dictionary<string, VCExpr>>();
+            Stack<List<string>> binders = new Stack<List<string>>();
+        }
+
+        public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(expr != null);
+            return expr.Accept<Z3TermAst, LineariserOptions>(this, options);
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        private bool DeBruijnIndex(string variableName, out int deBruijnIndex)
+        {
+            deBruijnIndex = -1;
+            foreach (List<string> binder in binders)
+            {
+                for (int i = binder.Count - 1; i >= 0; i--)
+                {
+                    deBruijnIndex++;
+                    if (binder[i].Equals(variableName))
+                        return true;
+                }
+            }
+            deBruijnIndex = -1;
+            return false;
+        }
+
+        protected Z3TermAst FindDefinition(string variableName, Type variableType)
+        {
+            Z3TermAst termAst;
+            int deBruijnIndex;
+            if (DeBruijnIndex(variableName, out deBruijnIndex))
+            {
+                return cm.MakeBoundVariable((uint)deBruijnIndex, variableType);
+            }
+            else
+            {
+                termAst = cm.GetConstant(variableName, variableType);
+                return termAst;
+            }
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+
+            if (node == VCExpressionGenerator.True)
+                return cm.MakeTrue();
+            else if (node == VCExpressionGenerator.False)
+                return cm.MakeFalse();
+            else if (node is VCExprIntLit)
+                return cm.MakeIntLiteral(((VCExprIntLit)node).Val.ToString());
+            else
+            {
+                Contract.Assert(false);
+                throw new cce.UnreachableException();
+            }
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        public Z3TermAst Visit(VCExprNAry node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+            VCExprOp op = node.Op;
+            Contract.Assert(op != null);
+
+            if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))
+            {
+                // handle these operators without recursion
+                List<Z3TermAst> asts = new List<Z3TermAst>();
+                string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";
+
+                IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
+                Contract.Assert(enumerator != null);
+                while (enumerator.MoveNext())
+                {
+                    VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+                    if (naryExpr == null || !naryExpr.Op.Equals(op))
+                    {
+                        asts.Add(Linearise(cce.NonNull((VCExpr)enumerator.Current), options));
+                    }
+                }
+
+                return cm.Make(opString, asts);
+            }
+
+            return node.Accept<Z3TermAst, LineariserOptions>(OpLineariser, options);
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        public Z3TermAst Visit(VCExprVar node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+
+            return FindDefinition(node.Name, node.Type);
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options)
+        {
+            Contract.Requires(options != null);
+            Contract.Requires(node != null);
+            Contract.Assert(node.TypeParameters.Count == 0);
+
+            binders.Push(new List<string>());
+            try
+            {
+                List<string> varNames;
+                List<Type> varTypes;
+                VisitBounds(node.BoundVars, out varNames, out varTypes);
+                List<Z3PatternAst> patterns;
+                List<Z3TermAst> no_patterns;
+                VisitTriggers(node.Triggers, options, out patterns, out no_patterns);
+                Z3TermAst body = Linearise(node.Body, options);
+                Z3TermAst result;
+
+                /*
+                if (options.QuantifierIds)
+                {
+                    // only needed for Z3
+                    VCQuantifierInfos infos = node.Infos;
+                    Contract.Assert(infos != null);
+                    if (infos.qid != null)
+                    {
+                        wr.Write("(QID ");
+                        wr.Write(infos.qid);
+                        wr.Write(") ");
+                    }
+                    if (0 <= infos.uniqueId)
+                    {
+                        wr.Write("(SKOLEMID ");
+                        wr.Write(infos.uniqueId);
+                        wr.Write(") ");
+                    }
+                }
+
+                if (options.UseWeights)
+                {
+                    int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
+                    if (weight != 1)
+                    {
+                        wr.Write("(WEIGHT ");
+                        wr.Write(weight);
+                        wr.Write(") ");
+                    }
+                }
+                */
+
+                switch (node.Quan)
+                {
+                    case Quantifier.ALL:
+                        result = cm.MakeForall(varNames, varTypes, patterns, no_patterns, body); break;
+                    case Quantifier.EX:
+                        result = cm.MakeExists(varNames, varTypes, patterns, no_patterns, body); break;
+                    default:
+                        throw new Exception("unknown quantifier kind " + node.Quan);
+                }
+                return result;
+            }
+            finally
+            {
+                binders.Pop();
+            }
+        }
+        
+        private void VisitBounds(List<VCExprVar> boundVars, out List<string> varNames, out List<Type> varTypes)
+        {
+            varNames = new List<string>();
+            varTypes = new List<Type>();
+            foreach (VCExprVar var in boundVars)
+            {
+                varNames.Add(var.Name);
+                varTypes.Add(var.Type);
+                binders.Peek().Add(var.Name);
+            }
+        }
+
+        private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Z3PatternAst> patterns, out List<Z3TermAst> no_patterns)
+        {
+            patterns = new List<Z3PatternAst>();
+            no_patterns = new List<Z3TermAst>();
+            foreach (VCTrigger trigger in triggers)
+            {
+                List<Z3TermAst> exprs = new List<Z3TermAst>();
+                foreach (VCExpr expr in trigger.Exprs)
+                {
+                    System.Diagnostics.Debug.Assert(expr != null);
+                    Z3TermAst termAst = Linearise(expr, options);
+                    exprs.Add(termAst);
+                }
+                if (exprs.Count > 0)
+                {
+                    if (trigger.Pos)
+                    {
+                        Z3PatternAst pattern = cm.MakePattern(exprs);
+                        patterns.Add(pattern);
+                    }
+                    else
+                    {
+                        foreach (Z3TermAst expr in exprs)
+                            no_patterns.Add(expr);
+                    }
+                }
+            }
+        }
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        public Z3TermAst Visit(VCExprLet node, LineariserOptions options)
+        {
+            try
+            {
+                Dictionary<string, VCExpr> let = new Dictionary<string, VCExpr>();
+                lets.Push(let);
+                foreach (VCExprLetBinding b in node)
+                {
+                    let.Add(b.V.Name, b.E);
+                }
+                Z3TermAst letAST = Linearise(node.Body, options);
+                return letAST;
+            }
+            finally
+            {
+                lets.Pop();
+            }
+        }
+
+  
+
+        /////////////////////////////////////////////////////////////////////////////////////
+
+        // Lineariser for operator terms. The result (bool) is currently not used for anything
+        internal class Z3apiOpLineariser : IVCExprOpVisitor<Z3TermAst, LineariserOptions/*!*/>
+        {
+            [ContractInvariantMethod]
+            void ObjectInvariant()
+            {
+                Contract.Invariant(ExprLineariser != null);
+                Contract.Invariant(wr != null);
+            }
+
+            private readonly Z3apiExprLineariser/*!*/ ExprLineariser;
+            private readonly TextWriter/*!*/ wr;
+
+            public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser)
+            {
+                Contract.Requires(ExprLineariser != null);
+                this.ExprLineariser = ExprLineariser;
+            }
+
+            ///////////////////////////////////////////////////////////////////////////////////
+
+            private Z3TermAst 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>();
+                foreach (VCExpr e in terms)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                return ExprLineariser.cm.Make(op, args);
+            }
+
+            ///////////////////////////////////////////////////////////////////////////////////
+
+            public Z3TermAst 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)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                if (node[0].Type.IsBool)
+                {
+                    Contract.Assert(node[1].Type.IsBool);
+                    // use equivalence
+                    return WriteApplication("IFF", node, options);
+                }
+                else
+                {
+                    Contract.Assert(!node[1].Type.IsBool);
+                    // use equality and write the arguments as terms
+                    return WriteApplication("EQ", node, options);
+                }
+            }
+
+            public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+
+                if (node[0].Type.IsBool)
+                {
+                    Contract.Assert(node[1].Type.IsBool);
+                    // use equivalence and negate the whole thing
+                    List<Z3TermAst> args = new List<Z3TermAst>();
+                    args.Add(WriteApplication("IFF", node, options));
+                    return ExprLineariser.cm.Make("NOT", args);
+                }
+                else
+                {
+                    // use equality and write the arguments as terms
+                    return WriteApplication("NEQ", node, options);
+                }
+            }
+
+            public Z3TermAst 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)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("OR", node, options); 
+            }
+
+            public Z3TermAst VisitImpliesOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                if (options.InverseImplies)
+                {
+                    List<Z3TermAst> args = new List<Z3TermAst>();
+
+                    args.Add(ExprLineariser.Linearise(node[1], options));
+                    List<Z3TermAst> t = new List<Z3TermAst>();
+                    t.Add(ExprLineariser.Linearise(node[0], options));
+                    args.Add(ExprLineariser.cm.Make("NOT", t));
+                    return ExprLineariser.cm.Make("OR", args);
+                }
+                else
+                {
+                    return WriteApplication("IMPLIES", node, options);
+                }
+            }
+
+            public Z3TermAst VisitDistinctOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+
+                if (node.Length < 2)
+                {
+                    return ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+                }
+                else
+                {
+                    List<Z3TermAst> args = new List<Z3TermAst>();
+                    foreach (VCExpr e in node)
+                    {
+                        Contract.Assert(e != null);
+                        args.Add(ExprLineariser.Linearise(e, options));
+                    }
+                    return ExprLineariser.cm.Make("DISTINCT", args);
+                }
+            }
+
+            public Z3TermAst VisitLabelOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                VCExprLabelOp op = (VCExprLabelOp)node.Op;
+                Contract.Assert(op != null);
+                return ExprLineariser.Linearise(node[0], options); 
+            }
+
+            public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                List<Z3TermAst> args = new List<Z3TermAst>();
+                foreach (VCExpr/*!*/ e in node)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args);
+            }
+
+            public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                List<Z3TermAst> args = new List<Z3TermAst>();
+                foreach (VCExpr e in node)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args);
+            }
+
+            public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("$make_bv" + node.Type.BvBits, node, options);
+            }
+
+            public Z3TermAst VisitBvExtractOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(SimplifyLikeExprLineariser.BvExtractOpName(node), node, options);
+            }
+
+            public Z3TermAst VisitBvConcatOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication(SimplifyLikeExprLineariser.BvConcatOpName(node), node, options);
+            }
+
+            public Z3TermAst VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+
+                List<Z3TermAst> args = new List<Z3TermAst>();
+                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)
+            {
+                Contract.Requires(node != null);
+                Contract.Requires(options != null);
+                VCExprCustomOp op = (VCExprCustomOp)node.Op;
+                List<Z3TermAst> args = new List<Z3TermAst>();
+                foreach (VCExpr arg in node)
+                {
+                    args.Add(ExprLineariser.Linearise(arg, options));
+                }
+                return ExprLineariser.cm.Make(op.Name, args);
+            }
+
+            public Z3TermAst VisitAddOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                if (CommandLineOptions.Clo.ReflectAdd)
+                {
+                    return WriteApplication("Reflect$Add", node, options);
+                }
+                else
+                {
+                    return WriteApplication("+", node, options);
+                }
+            }
+
+            public Z3TermAst VisitSubOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("-", node, options);
+            }
+
+            public Z3TermAst VisitMulOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("*", node, options);
+            }
+
+            public Z3TermAst VisitDivOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("/", node, options);
+            }
+
+            public Z3TermAst VisitModOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("%", node, options);
+            }
+
+            public Z3TermAst VisitLtOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("intLess", node, options);  // arguments are always terms
+            }
+
+            public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("intAtMost", node, options);  // arguments are always terms
+            }
+
+            public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("intGreater", node, options);  // arguments are always terms
+            }
+
+            public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("intAtLeast", node, options);  // arguments are always terms
+            }
+
+            public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("<:", node, options);               // arguments are always terms
+            }
+
+            public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                return WriteApplication("<::", node, options);               // arguments are always terms
+            }
+
+            public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
+            {
+                Contract.Requires(options != null);
+                Contract.Requires(node != null);
+                VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
+                Contract.Assert(op != null);
+                string funcName = op.Func.Name;
+                Contract.Assert(funcName != null);
+                string bvzName = op.Func.FindStringAttribute("external");
+                string printedName = ExprLineariser.Namer.GetName(op.Func, funcName);
+                Contract.Assert(printedName != null);
+                if (bvzName != null) printedName = bvzName;
+
+                List<Z3TermAst> args = new List<Z3TermAst>();
+                foreach (VCExpr e in node)
+                {
+                    Contract.Assert(e != null);
+                    args.Add(ExprLineariser.Linearise(e, options));
+                }
+                return ExprLineariser.cm.Make(printedName, args);
+            }
+        }
+    }
+}
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
new file mode 100644
index 00000000..e8d785a5
--- /dev/null
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -0,0 +1,97 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+    <ProductVersion>9.0.21022</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>Z3api</RootNamespace>
+    <AssemblyName>Z3api</AssemblyName>
+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
+    <FileAlignment>512</FileAlignment>
+    <StartupObject>
+    </StartupObject>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <OutputPath>bin\Debug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <OutputPath>bin\Release\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+  </PropertyGroup>
+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
+  <ItemGroup>
+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+      <SpecificVersion>False</SpecificVersion>
+      <HintPath>..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>
+    </Reference>
+    <Reference Include="Microsoft.Z3, Version=2.0.3662.37897, Culture=neutral, PublicKeyToken=9c8d792caae602a2, processorArchitecture=x86">
+      <SpecificVersion>False</SpecificVersion>
+      <HintPath>..\..\..\Binaries\Microsoft.Z3.dll</HintPath>
+    </Reference>
+    <Reference Include="System" />
+    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+      <SpecificVersion>False</SpecificVersion>
+      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
+    </Reference>
+    <Reference Include="System.Core">
+      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    </Reference>
+    <Reference Include="System.Data" />
+    <Reference Include="System.XML" />
+  </ItemGroup>
+  <ItemGroup>
+    <ProjectReference Include="..\..\AIFramework\AIFramework.sscproj">
+      <Project>{24B55172-AD8B-47D1-8952-5A95CFDB9B31}</Project>
+      <Name>AIFramework</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\Basetypes\Basetypes.sscproj">
+      <Project>{0C692837-77EC-415F-BF04-395E3ED06E9A}</Project>
+      <Name>Basetypes</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\Core\Core.sscproj">
+      <Project>{47BC34F1-A173-40BE-84C2-9332B4418387}</Project>
+      <Name>Core</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
+      <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+      <Name>VCExpr</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+      <Name>VCGeneration</Name>
+    </ProjectReference>
+    <ProjectReference Include="..\Z3\Z3.csproj">
+      <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
+      <Name>Z3</Name>
+    </ProjectReference>
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="ContextLayer.cs" />
+    <Compile Include="ProverLayer.cs" />
+    <Compile Include="SafeContext.cs" />
+    <Compile Include="StubContext.cs" />
+    <Compile Include="TypeAdapter.cs" />
+    <Compile Include="VCExprVisitor.cs" />
+  </ItemGroup>
+</Project>
+\ No newline at end of file
author	qadeer <unknown>	2010-08-20 21:52:05 +0000
committer	qadeer <unknown>	2010-08-20 21:52:05 +0000
commit	0d77cf304b9bd2b2152fe1a733e4533536c883c0 (patch)
tree	9ce338c9e4d2ad54d759b434248b7761a8c75b6d
parent	27cc9c245d21151a78c95cead4801ad130557743 (diff)