further refactoring

4 files changed, 501 insertions, 631 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 390d875d..f0aa3906 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -14,579 +14,448 @@ using Microsoft.Basetypes;
 using Z3Model = Microsoft.Z3.Model;

 using BoogieModel = Microsoft.Boogie.Model;

 

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

-        }

+namespace Microsoft.Boogie.Z3 {

+  public class Z3apiProverContext : DeclFreeProverContext {

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

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

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

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

+

+    public Config config;

+    public Context z3;

+

+    private Z3TypeCachedBuilder tm;

+    private UniqueNamer namer;

+    private StreamWriter z3log;

+

+    private int counterexamples;

+    private string logFilename;

+    private List<string> debugTraces;

+

+    public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)

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

+      int timeout = opts.Timeout * 1000;

+      config = new Config();

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

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

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

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

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

+      if (0 <= timeout) {

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

+      }

 

-        public List<string> DebugTraces

-        {

-            get { return this.debugTraces; }

-        }

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

+        this.counterexamples = CommandLineOptions.Clo.ProverCCLimit;

+      }

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

+        logFilename = CommandLineOptions.Clo.SimplifyLogFilePath;

+      }

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

+

+      z3 = new Context(config);

+      z3.SetPrintMode(PrintMode.Smtlib2Compliant);

+      if (logFilename != null)

+        z3.OpenLog(logFilename);

+      foreach (string tag in debugTraces)

+        z3.EnableDebugTrace(tag);

+

+      this.z3log = null;

+      this.tm = new Z3TypeCachedBuilder(this);

+      this.namer = new UniqueNamer();

     }

 

-    internal class BacktrackDictionary<K, V>

-    {

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

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

-

-        public BacktrackDictionary()

-        {

-            CreateBacktrackPoint();

-        }

-

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

-        {

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

-        }

-

-        public void Add(K key, V v)

-        {

-            if (dictionary.ContainsKey(key))

-            {

-                dictionary.Remove(key);

-            }

-            dictionary.Add(key, v);

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

-        }

-

-        public bool ContainsKey(K k)

-        {

-            return dictionary.ContainsKey(k);

-        }

-

-        public void CreateBacktrackPoint()

-        {

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

-        }

-

-        public void Backtrack()

-        {

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

-            foreach (K key in keysToErase)

-            {

-                dictionary.Remove(key);

-            }

-            if (keyStack.Count == 0)

-                this.CreateBacktrackPoint();

-        }

-

-        public IEnumerator GetEnumerator()

-        {

-            return dictionary.Keys.GetEnumerator();

-        }

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

+      base.DeclareType(t, attributes);

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

     }

 

-    public class Z3ErrorModelAndLabels

-    {

-        private ErrorModel _errorModel;

-        private List<string> _relevantLabels;

-        public ErrorModel ErrorModel

-        {

-            get { return this._errorModel; }

-        }

-        public List<string> RelevantLabels

-        {

-            get { return this._relevantLabels; }

-        }

-        public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels)

-        {

-            this._errorModel = errorModel;

-            this._relevantLabels = relevantLabels;

-        }

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

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

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

     }

 

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

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

       }

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

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

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

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

+

+      string functionName = f.Name;

+      Symbol symbolAst = GetSymbol(functionName);

+      var domainStr = "";

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

+      foreach (Type domainType in domain) {

+        Sort type = tm.GetType(domainType);

+        domainAst.Add(type);

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

       }

+      Sort rangeAst = tm.GetType(range);

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

+      functions.Add(functionName, constDeclAst);

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

+    }

 

-      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 override void DeclareGlobalVariable(GlobalVariable v, string attributes) {

+      base.DeclareGlobalVariable(v, attributes);

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

+    }

 

-      public void CloseLog() {

-        z3.CloseLog();

-        if (z3log != null) {

-          z3log.Close();

-        }

-        z3log = null;

-      }

+    public override string Lookup(VCExprVar var) {

+      return namer.Lookup(var);

+    }

 

-      public void CreateBacktrackPoint() {

-        symbols.CreateBacktrackPoint();

-        constants.CreateBacktrackPoint();

-        functions.CreateBacktrackPoint();

-        labels.CreateBacktrackPoint();

-        z3.Push();

-        log("(push)");

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

-        z3.Pop();

-        labels.Backtrack();

-        functions.Backtrack();

-        constants.Backtrack();

-        symbols.Backtrack();

-        log("(pop)");

+    public void CloseLog() {

+      z3.CloseLog();

+      if (z3log != null) {

+        z3log.Close();

       }

+      z3log = null;

+    }

 

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

+      symbols.CreateBacktrackPoint();

+      constants.CreateBacktrackPoint();

+      functions.CreateBacktrackPoint();

+      labels.CreateBacktrackPoint();

+      z3.Push();

+      log("(push)");

+    }

 

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

+      z3.Pop();

+      labels.Backtrack();

+      functions.Backtrack();

+      constants.Backtrack();

+      symbols.Backtrack();

+      log("(pop)");

+    }

 

-      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 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 string GetDeclName(FuncDecl constDeclAst) {

-        Symbol symbol = z3.GetDeclName(constDeclAst);

-        return z3.GetSymbolString(symbol);

-      }

+    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 Pattern MakePattern(List<Term> exprs) {

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

-        return pattern;

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

       }

-

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

+      foreach (Term assumption in assumptions) {

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

+        z3.AssertCnstr(assumption);

       }

+    }

 

-      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 List<Sort> GetTypes(List<Type> boogieTypes) {

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

+      foreach (Type boogieType in boogieTypes) {

+        Sort type = tm.GetType(boogieType);

+        z3Types.Add(type);

       }

+      return z3Types;

+    }

 

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

-        Debug.Assert(l != null);

-        if (r == null)

-          return false;

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

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

-      }

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

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

+          return false;

+      return true;

+    }

 

-      /*

-      private Z3ErrorModelAndLabels BuildZ3ErrorModel(Z3Model 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 + ",");

       }

-      */

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

-          Z3Model z3Model;

-          outcome = z3.CheckAndGetModel(out z3Model);

-          

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

-          if (outcome == LBool.False)

-            break;

-

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

-            // Blame this on timeout

-            return ProverInterface.Outcome.TimeOut;

-          }

-

-          Debug.Assert(z3Model != null);

-          LabeledLiterals labels = z3.GetRelevantLabels();

-          Debug.Assert(labels != null);

-

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

-          uint numLabels = labels.GetNumLabels();

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

-            Symbol sym = labels.GetLabel(i);

-            string labelName = z3.GetSymbolString(sym);

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

-              labels.Disable(i);

-            }

-            labelStrings.Add(labelName);

-          }

-

-          var sw = new StringWriter();

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

-          z3Model.Display(sw);

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

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

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

-

-

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

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

+    }

 

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

+      Symbol symbolAst = GetSymbol(constantName);

+      Sort typeAst = tm.GetType(boogieType);

 

-          boogieErrors.Add(e);

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

+      constants.Add(constantName, constAst);

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

+    }

 

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

-            z3.BlockLiterals(labels);

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

-          }

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

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

+      boogieErrors = new List<Z3ErrorModelAndLabels>();

+      LBool outcome = LBool.Undef;

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

+      while (true) {

+        Z3Model z3Model;

+        outcome = z3.CheckAndGetModel(out z3Model);

 

-          

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

+        if (outcome == LBool.False)

+          break;

 

-          labels.Dispose();

-          z3Model.Dispose();

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

-            break;

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

+          // Blame this on timeout

+          return ProverInterface.Outcome.TimeOut;

         }

 

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

+        Debug.Assert(z3Model != null);

+        LabeledLiterals labels = z3.GetRelevantLabels();

+        Debug.Assert(labels != null);

 

-        Z3Model z3Model;

-        Term proof;

-        Term[] core;

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

-        var logstring = "";

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

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

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

-          assumption_terms[i] = z3ast;

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

-        }

-

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

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

-

-        if (outcome != LBool.False) {

-          Debug.Assert(z3Model != null);

-          LabeledLiterals labels = z3.GetRelevantLabels();

-          Debug.Assert(labels != null);

-

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

-          uint numLabels = labels.GetNumLabels();

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

-            Symbol sym = labels.GetLabel(i);

-            string labelName = z3.GetSymbolString(sym);

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

-              labels.Disable(i);

-            }

-            labelStrings.Add(labelName);

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

+        uint numLabels = labels.GetNumLabels();

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

+          Symbol sym = labels.GetLabel(i);

+          string labelName = z3.GetSymbolString(sym);

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

+            labels.Disable(i);

           }

+          labelStrings.Add(labelName);

+        }

 

-          var sw = new StringWriter();

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

-          z3Model.Display(sw);

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

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

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

-

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

-          boogieErrors.Add(e);

+        var sw = new StringWriter();

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

+        z3Model.Display(sw);

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

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

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

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

+        boogieErrors.Add(e);

 

-          labels.Dispose();

-          z3Model.Dispose();

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

+          z3.BlockLiterals(labels);

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

         }

 

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

-        }

+        labels.Dispose();

+        z3Model.Dispose();

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

+          break;

       }

 

-      public void DeclareType(string typeName) {

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

+      if (boogieErrors.Count > 0) {

+        return ProverInterface.Outcome.Invalid;

       }

-

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

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

+        return ProverInterface.Outcome.Valid;

       }

-

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

+      else {

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

+        return ProverInterface.Outcome.Undetermined;

       }

+    }

 

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

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

-        foreach (string symbolName in symbolNames)

-          symbols.Add(GetSymbol(symbolName));

-        return symbols;

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

+        out List<Z3ErrorModelAndLabels> boogieErrors,

+        out List<int> unsatCore) {

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

+      boogieErrors = new List<Z3ErrorModelAndLabels>();

+      unsatCore = new List<int>();

+      LBool outcome = LBool.Undef;

+

+      Z3Model z3Model;

+      Term proof;

+      Term[] core;

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

+      var logstring = "";

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

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

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

+        assumption_terms[i] = z3ast;

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

       }

 

-      private Symbol GetSymbol(string symbolName) {

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

-          Symbol symbolAst = z3.MkSymbol(symbolName);

-          symbols.Add(symbolName, symbolAst);

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

         }

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

+        var sw = new StringWriter();

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

+        z3Model.Display(sw);

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

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

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

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

+        boogieErrors.Add(e);

 

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

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

-        return typeSafeTerm;

+        labels.Dispose();

+        z3Model.Dispose();

       }

 

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

+      if (boogieErrors.Count > 0) {

+        return ProverInterface.Outcome.Invalid;

       }

-

-      public LabeledLiterals GetRelevantLabels() {

-        LabeledLiterals safeLiterals = z3.GetRelevantLabels();

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

-        return safeLiterals;

+      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 Term Make(VCExprOp op, List<Term> children) {

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

-        VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;

-        if (boogieFunctionOp != null) {

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

-          return z3.MkApp(f, unwrapChildren);

-        }

-        VCExprDistinctOp distinctOp = op as VCExprDistinctOp;

-        if (distinctOp != null) {

-          return z3.MkDistinct(unwrapChildren);

-        }

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

+    }

 

-        if (op == VCExpressionGenerator.AndOp) {

-          return z3.MkAnd(unwrapChildren);

-        }

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

+      Term typeSafeTerm;

+      if (!constants.ContainsKey(constantName))

+        this.DeclareConstant(constantName, constantType);

 

-        if (op == VCExpressionGenerator.OrOp) {

-          return z3.MkOr(unwrapChildren);

-        }

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

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

+      return typeSafeTerm;

+    }

 

-        if (op == VCExpressionGenerator.ImpliesOp) {

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

-        }

+    public FuncDecl GetFunction(string functionName) {

+      FuncDecl f;

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

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

+      return f;

+    }

 

-        if (op == VCExpressionGenerator.NotOp) {

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

-        }

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

+    }

 

-        if (op == VCExpressionGenerator.EqOp) {

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

-        }

+    public LabeledLiterals GetRelevantLabels() {

+      LabeledLiterals safeLiterals = z3.GetRelevantLabels();

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

+      return safeLiterals;

+    }

+  }

 

-        if (op == VCExpressionGenerator.NeqOp) {

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

-        }

+  internal class BacktrackDictionary<K, V> {

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

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

 

-        if (op == VCExpressionGenerator.LtOp) {

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

-        }

+    public BacktrackDictionary() {

+      CreateBacktrackPoint();

+    }

 

-        if (op == VCExpressionGenerator.LeOp) {

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

-        }

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

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

+    }

 

-        if (op == VCExpressionGenerator.GtOp) {

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

-        }

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

+      if (dictionary.ContainsKey(key)) {

+        dictionary.Remove(key);

+      }

+      dictionary.Add(key, v);

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

+    }

 

-        if (op == VCExpressionGenerator.GeOp) {

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

-        }

+    public bool ContainsKey(K k) {

+      return dictionary.ContainsKey(k);

+    }

 

-        if (op == VCExpressionGenerator.AddOp) {

-          return z3.MkAdd(unwrapChildren);

-        }

+    public void CreateBacktrackPoint() {

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

+    }

 

-        if (op == VCExpressionGenerator.SubOp) {

-          return z3.MkSub(unwrapChildren);

-        }

+    public void Backtrack() {

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

+      foreach (K key in keysToErase) {

+        dictionary.Remove(key);

+      }

+      if (keyStack.Count == 0)

+        this.CreateBacktrackPoint();

+    }

 

-        if (op == VCExpressionGenerator.DivOp) {

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

-        }

+    public IEnumerator GetEnumerator() {

+      return dictionary.Keys.GetEnumerator();

+    }

+  }

 

-        if (op == VCExpressionGenerator.MulOp) {

-          return z3.MkMul(unwrapChildren);

-        }

+  public class Z3ErrorModelAndLabels {

+    private ErrorModel _errorModel;

+    private List<string> _relevantLabels;

+    public ErrorModel ErrorModel {

+      get { return this._errorModel; }

+    }

+    public List<string> RelevantLabels {

+      get { return this._relevantLabels; }

+    }

+    public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels) {

+      this._errorModel = errorModel;

+      this._relevantLabels = relevantLabels;

+    }

+  }

 

-        if (op == VCExpressionGenerator.ModOp) {

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

-        }

 

-        if (op == VCExpressionGenerator.IfThenElseOp) {

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

-        }

 

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

-      }

-    }

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

         {

             base.Close();

-            Z3Context cm = context.cm;

-            cm.CloseLog();

-            cm.z3.Dispose();

-            cm.config.Config.Dispose();

+            context.CloseLog();

+            context.z3.Dispose();

+            context.config.Dispose();

         }

 

         public void PushAxiom(VCExpr axiom)

         {

-            Z3Context cm = context.cm;

-            cm.CreateBacktrackPoint();

+            context.CreateBacktrackPoint();

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

-            cm.AddAxiom(axiom, linOptions);

-            

+            context.AddAxiom(axiom, linOptions);

         }

 

         private void PushConjecture(VCExpr conjecture)

         {

-            Z3Context cm = context.cm;

-            cm.CreateBacktrackPoint();

+            context.CreateBacktrackPoint();

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

-            cm.AddConjecture(conjecture, linOptions);

+            context.AddConjecture(conjecture, linOptions);

         }

 

         public override void PushVCExpression(VCExpr vc)

@@ -78,61 +74,53 @@ namespace Microsoft.Boogie.Z3
 

         public void CreateBacktrackPoint()

         {

-            Z3Context cm = context.cm;

-            cm.CreateBacktrackPoint();

+            context.CreateBacktrackPoint();

         }

 

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

         {

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

-            Z3Context cm = context.cm;

             Push();

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

-            cm.AddConjecture(vc, linOptions);

-            outcome = cm.Check(out z3LabelModels);

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

+            context.AddConjecture(vc, linOptions);

+            outcome = context.Check(out z3LabelModels);

             Pop();

         }

   

         public override void Check()

         {

-            Z3Context cm = context.cm;

-            outcome = cm.Check(out z3LabelModels);

+            outcome = context.Check(out z3LabelModels);

         }

 

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

         {

-            Z3Context cm = context.cm;

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

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

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

         }

 

         public override void Push()

         {

-            Z3Context cm = context.cm;

-            cm.CreateBacktrackPoint();

+            context.CreateBacktrackPoint();

         }

 

         public override void Pop()

         {

-            Z3Context cm = context.cm;

-            cm.Backtrack();

+            context.Backtrack();

         }

 

         public override void Assert(VCExpr vc, bool polarity)

         {

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

-            Z3Context cm = context.cm;

             if (polarity)

-                cm.AddAxiom(vc, linOptions);

+                context.AddAxiom(vc, linOptions);

             else

-                cm.AddConjecture(vc, linOptions);

+                context.AddConjecture(vc, linOptions);

         }

 

         public override void AssertAxioms()

         {

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

-            Z3Context cm = context.cm;

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

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

         }

 

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

@@ -188,82 +176,6 @@ namespace Microsoft.Boogie.Z3
             return result;

         }

     }

-

-    public class Z3apiProverContext : DeclFreeProverContext

-    {

-        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 Z3Context(this, config, gen);

-        }

-        private static Z3Config BuildConfig(int timeout, bool nativeBv)

-        {

-            Z3Config config = new Z3Config();

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

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

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

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

-

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

-            {

-                config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);

-            }

-

-            if (0 <= timeout)

-            {

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

-            }

-

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

-            {

-                config.SetLogFilename(CommandLineOptions.Clo.SimplifyLogFilePath);

-            }

-

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

-            return config;

-        }

-

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

-        }

-

-        public override string Lookup(VCExprVar var)

-        {

-            return cm.Namer.Lookup(var);

-        }

-    }

 }

 

 namespace Microsoft.Boogie.Z3api

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index b0dd1eb4..e1c6de0b 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -80,15 +80,15 @@ namespace Microsoft.Boogie.Z3
         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;

+        private Z3apiProverContext container;

 

-        public Z3TypeCachedBuilder(Z3Context context)

+        public Z3TypeCachedBuilder(Z3apiProverContext context)

         {

             this.container = context;

         }

 

         private Sort GetMapType(MapType mapType) {

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

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

           if (!mapTypes.ContainsKey(mapType)) {

             Type result = mapType.Result;

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

@@ -153,19 +153,19 @@ namespace Microsoft.Boogie.Z3
 

         public Sort BuildMapType(Sort domain, Sort range)

         {

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

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

             return z3.MkArraySort(domain, range);

         }

 

         public Sort BuildBvType(BvType bvType)

         {

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

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

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

         }

 

         public Sort BuildBasicType(BasicType basicType)

         {

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

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

             Sort typeAst;

             if (basicType.IsBool)

             {

@@ -181,7 +181,7 @@ namespace Microsoft.Boogie.Z3
         }

 

         public Sort BuildCtorType(CtorType ctorType) {

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

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

           if (ctorType.Arguments.Length > 0)

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

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

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index bf6dab94..149a23f1 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -31,9 +31,9 @@ namespace Microsoft.Boogie.Z3
 

         internal readonly UniqueNamer namer;

         internal readonly Dictionary<VCExprVar, Term> letBindings;

-        protected Z3Context cm;

+        protected Z3apiProverContext cm;

 

-        public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)

+        public Z3apiExprLineariser(Z3apiProverContext cm, UniqueNamer namer)

         {

             this.cm = cm;

             this.namer = namer;

@@ -49,6 +49,86 @@ namespace Microsoft.Boogie.Z3
 

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

 

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

+          Context z3 = cm.z3;

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

+          VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;

+          if (boogieFunctionOp != null) {

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

+            return z3.MkApp(f, unwrapChildren);

+          }

+          VCExprDistinctOp distinctOp = op as VCExprDistinctOp;

+          if (distinctOp != null) {

+            return z3.MkDistinct(unwrapChildren);

+          }

+

+          if (op == VCExpressionGenerator.AndOp) {

+            return z3.MkAnd(unwrapChildren);

+          }

+

+          if (op == VCExpressionGenerator.OrOp) {

+            return z3.MkOr(unwrapChildren);

+          }

+

+          if (op == VCExpressionGenerator.ImpliesOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.NotOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.EqOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.NeqOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.LtOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.LeOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.GtOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.GeOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.AddOp) {

+            return z3.MkAdd(unwrapChildren);

+          }

+

+          if (op == VCExpressionGenerator.SubOp) {

+            return z3.MkSub(unwrapChildren);

+          }

+

+          if (op == VCExpressionGenerator.DivOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.MulOp) {

+            return z3.MkMul(unwrapChildren);

+          }

+

+          if (op == VCExpressionGenerator.ModOp) {

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

+          }

+

+          if (op == VCExpressionGenerator.IfThenElseOp) {

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

+          }

+

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

+        }

+

         public Term Visit(VCExprLiteral node, LineariserOptions options)

         {

             Contract.Requires(options != null);

@@ -91,7 +171,7 @@ namespace Microsoft.Boogie.Z3
                     }

                 }

 

-                return cm.Make(op, asts);

+                return Make(op, asts);

             }

 

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

@@ -155,9 +235,9 @@ namespace Microsoft.Boogie.Z3
                 switch (node.Quan)

                 {

                     case Microsoft.Boogie.VCExprAST.Quantifier.ALL:

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

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

                     case Microsoft.Boogie.VCExprAST.Quantifier.EX:

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

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

                     default:

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

                 }

@@ -168,7 +248,18 @@ namespace Microsoft.Boogie.Z3
                 namer.PopScope();

             }

         }

-        

+

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

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

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

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

+            bound.Add(t);

+          }

+

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

+          return termAst;

+        }

+

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

         {

             varNames = new List<string>();

@@ -196,17 +287,15 @@ namespace Microsoft.Boogie.Z3
                 }

                 if (exprs.Count > 0)

                 {

-                    if (trigger.Pos)

-                    {

-                        Pattern pattern = cm.MakePattern(exprs);

-                        patterns.Add(pattern);

-                    }

-                    else

-                    {

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

-                        foreach (Term expr in exprs)

-                            no_patterns.Add(expr);

-                    }

+                  if (trigger.Pos) {

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

+                    patterns.Add(pattern);

+                  }

+                  else {

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

+                    foreach (Term expr in exprs)

+                      no_patterns.Add(expr);

+                  }

                 }

             }

         }

@@ -258,7 +347,7 @@ namespace Microsoft.Boogie.Z3
                     Contract.Assert(e != null);

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

                 }

-                return ExprLineariser.cm.Make(op, args);

+                return ExprLineariser.Make(op, args);

             }

 

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