fixes to z3api

5 files changed, 190 insertions, 347 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index ed45c4fc..390d875d 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -11,6 +11,9 @@ using Microsoft.Z3;
 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Basetypes;

 

+using Z3Model = Microsoft.Z3.Model;

+using BoogieModel = Microsoft.Boogie.Model;

+

 namespace Microsoft.Boogie.Z3

 {

     public class Z3Config

@@ -20,21 +23,6 @@ namespace Microsoft.Boogie.Z3
         private string logFilename;

         private List<string> debugTraces = new List<string>();

 

-        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 SetCounterExample(int counterexample)

         {

             this.counterexamples = counterexample;

@@ -69,102 +57,6 @@ namespace Microsoft.Boogie.Z3
         }

     }

 

-    internal class PartitionMap

-    {

-        private Context ctx;

-        private Model model;

-        private Dictionary<Term, int> termToPartition = new Dictionary<Term, int>();

-        private Dictionary<object, int> valueToPartition = new Dictionary<object, int>();

-        private List<Object> partitionToValue = new List<Object>();

-        private int partitionCounter = 0;

-        public int PartitionCounter { get { return partitionCounter; } }

-

-        public PartitionMap(Context ctx, Model z3Model)

-        { 

-            this.ctx = ctx;

-            this.model = z3Model;

-        }

-

-        public int GetPartition(Term value)

-        {

-            int result;

-            if (!termToPartition.TryGetValue(value, out result))

-            {

-                result = partitionCounter++;

-                termToPartition.Add(value, result);

-                partitionToValue.Add(null);

-                object constant = Evaluate(value);

-                valueToPartition.Add(constant, result);

-                partitionToValue[result] = constant;

-            }

-            return result;

-        }

-

-        private object Evaluate(Term v)

-        {

-            Sort s = v.GetSort();

-            Sort boolSort = ctx.MkBoolSort();

-            Sort intSort = ctx.MkIntSort();

-            ArrayValue av;

-            

-            if (s.Equals(boolSort))

-            {

-                return ctx.GetBoolValue(v);

-            }

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

-              int i;

-              long il;

-              uint u;

-              ulong ul;

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

-                return BigNum.FromInt(i);

-              }

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

-                return BigNum.FromLong(il);

-              }

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

-                return BigNum.FromUInt(u);

-              }

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

-                return BigNum.FromULong(ul);

-              }

-              else {

-                string str = v.ToString();

-                return GetPartition(v);

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

-              }

-            }

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

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

-              List<int> tuple;

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

-                tuple = new List<int>();

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

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

-                arrayValue.Add(tuple);

-              }

-              tuple = new List<int>();

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

-              arrayValue.Add(tuple);

-              return arrayValue;

-            }

-            else {

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

-              return GetPartition(v);

-            }

-        }

-

-        public List<Object> PartitionToValue(Context ctx) 

-        {

-            return partitionToValue;

-        }

-

-        public Dictionary<object, int> ValueToPartition(Context ctx)

-        {

-            return valueToPartition;

-        }

-    }

-

     internal class BacktrackDictionary<K, V>

     {

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

@@ -217,86 +109,11 @@ namespace Microsoft.Boogie.Z3
         }

     }

 

-    internal class BoogieErrorModelBuilder

-    {

-        private Z3Context container;

-        private PartitionMap partitionMap;

-

-        public BoogieErrorModelBuilder(Z3Context container, Model z3Model)

-        {

-            this.container = container;

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

-        }

-        

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

-        {

-            Dictionary<string, int> constantToPartition = new Dictionary<string, int>();

-            foreach (FuncDecl c in z3Model.GetModelConstants())

-            {

-                string name = container.GetDeclName(c);

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

-                constantToPartition.Add(name, pid);

-            }

-            return constantToPartition;

-        }

-

-        private List<List<string>> CreatePartitionToConstant(Dictionary<string, int> constantToPartition)

-        {

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

-            for (int i = 0; i < partitionMap.PartitionCounter; i++)

-            {

-                partitionToConstant.Add(new List<string>());

-            }

-            foreach (string s in constantToPartition.Keys)

-            {

-                partitionToConstant[constantToPartition[s]].Add(s);

-            }

-            return partitionToConstant;

-        }

-

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

-                    }

-                    tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result)));

-                    f_tuples.Add(tuple);

-                }

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

-                else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else)));

-                f_tuples.Add(else_tuple);

-                functionToPartition.Add(f_name, f_tuples);

-            }

-            return functionToPartition;

-        }

-

-        public Z3ErrorModel BuildBoogieModel(Model z3Model)

-        {

-            Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);

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

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

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

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

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

-        }

-    }

-

     public class Z3ErrorModelAndLabels

     {

-        private Z3ErrorModel _errorModel;

+        private ErrorModel _errorModel;

         private List<string> _relevantLabels;

-        public Z3ErrorModel ErrorModel

+        public ErrorModel ErrorModel

         {

             get { return this._errorModel; }

         }

@@ -304,7 +121,7 @@ namespace Microsoft.Boogie.Z3
         {

             get { return this._relevantLabels; }

         }

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

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

         {

             this._errorModel = errorModel;

             this._relevantLabels = relevantLabels;

@@ -461,12 +278,13 @@ namespace Microsoft.Boogie.Z3
         return true;

       }

 

-      private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels) {

+      /*

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

@@ -480,8 +298,9 @@ namespace Microsoft.Boogie.Z3
         LBool outcome = LBool.Undef;

         Debug.Assert(0 < this.config.Counterexamples);

         while (true) {

-          Model z3Model;

+          Z3Model z3Model;

           outcome = z3.CheckAndGetModel(out z3Model);

+          

           log("(check-sat)");

           if (outcome == LBool.False)

             break;

@@ -505,13 +324,27 @@ namespace Microsoft.Boogie.Z3
             }

             labelStrings.Add(labelName);

           }

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

+

+          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 (boogieErrors.Count < this.config.Counterexamples) {

             z3.BlockLiterals(labels);

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

           }

 

+          

+

           labels.Dispose();

           z3Model.Dispose();

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

@@ -538,7 +371,7 @@ namespace Microsoft.Boogie.Z3
         unsatCore = new List<int>();

         LBool outcome = LBool.Undef;

 

-        Model z3Model;

+        Z3Model z3Model;

         Term proof;

         Term[] core;

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

@@ -568,7 +401,16 @@ namespace Microsoft.Boogie.Z3
             }

             labelStrings.Add(labelName);

           }

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

+

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

@@ -668,37 +510,83 @@ namespace Microsoft.Boogie.Z3
         return safeLiterals;

       }

 

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

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

         Term[] unwrapChildren = children.ToArray();

-        Term term;

-        switch (op) {

-          // formulas  

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

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

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

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

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

-          // terms

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

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

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

-          // terms

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

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

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

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

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

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

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

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

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

-          default: {

-              FuncDecl f = GetFunction(op);

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

-            }

-            break;

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

+        }

+

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

         }

-        return term;

+

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

       }

     }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index f691cffc..39acc5db 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -202,7 +202,10 @@ namespace Microsoft.Boogie.Z3
         private static Z3Config BuildConfig(int timeout, bool nativeBv)

         {

             Z3Config config = new Z3Config();

-            config.SetModel(true);

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

             {

@@ -211,7 +214,7 @@ namespace Microsoft.Boogie.Z3
 

             if (0 <= timeout)

             {

-                config.SetSoftTimeout(timeout.ToString());

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

             }

 

             if (CommandLineOptions.Clo.SimplifyLogFilePath != null)

@@ -219,7 +222,7 @@ namespace Microsoft.Boogie.Z3
                 config.SetLogFilename(CommandLineOptions.Clo.SimplifyLogFilePath);

             }

 

-            config.SetTypeCheck(true);

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

             return config;

         }

 

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index de5ebd8f..b0dd1eb4 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -87,21 +87,17 @@ namespace Microsoft.Boogie.Z3
             this.container = context;

         }

 

-        private Sort GetMapType(MapType mapType)

-        {

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

-            if (!mapTypes.ContainsKey(mapType))

-            {

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

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

-                Sort range = GetType(mapType.Result);

-                Sort typeAst = BuildMapType(domain, range);

-                mapTypes.Add(mapType, typeAst);

+        private Sort GetMapType(MapType mapType) {

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

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

+            Type result = mapType.Result;

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

+              GetType(result);

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

             }

-            Sort result;

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

-            Debug.Assert(containsKey);

-            return result;

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

+          }

+          return mapTypes[mapType];

         }

 

         private Sort GetBvType(BvType bvType)

@@ -158,15 +154,13 @@ namespace Microsoft.Boogie.Z3
         public Sort BuildMapType(Sort domain, Sort range)

         {

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

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

-            return typeAst;

+            return z3.MkArraySort(domain, range);

         }

 

         public Sort BuildBvType(BvType bvType)

         {

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

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

-            return typeAst;

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

         }

 

         public Sort BuildBasicType(BasicType basicType)

@@ -188,11 +182,9 @@ namespace Microsoft.Boogie.Z3
 

         public Sort BuildCtorType(CtorType ctorType) {

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

-          Sort typeAst;

           if (ctorType.Arguments.Length > 0)

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

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

-          return typeAst;

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

         }

     }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index aa47d7e0..bf6dab94 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -17,15 +17,15 @@ namespace Microsoft.Boogie.Z3
 {

     public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>

     {

-        private Z3apiOpLineariser OpLinObject = null;

+        private Z3apiOpLineariser opLineariser = null;

         private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser

         {

             get

             {

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

-                if (OpLinObject == null)

-                    OpLinObject = new Z3apiOpLineariser(this);

-                return OpLinObject;

+                if (opLineariser == null)

+                    opLineariser = new Z3apiOpLineariser(this);

+                return opLineariser;

             }

         }

 

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

                 }

 

-                return cm.Make(opString, asts);

+                return cm.Make(op, asts);

             }

 

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

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

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

 

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

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

             {

                 Contract.Requires(options != null);

                 Contract.Requires(op != null);

@@ -267,76 +267,49 @@ namespace Microsoft.Boogie.Z3
             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitEqOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitAndOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitOrOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                if (options.InverseImplies)

-                {

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

-

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

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

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

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

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

-                }

-                else

-                {

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

-                }

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

             }

 

-            public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)

+            public Term 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<Term> args = new List<Term>();

-                    foreach (VCExpr e in node)

-                    {

-                        Contract.Assert(e != null);

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

-                    }

-                    return ExprLineariser.cm.Make("DISTINCT", args);

-                }

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

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

             }

 

             public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)

@@ -358,10 +331,24 @@ namespace Microsoft.Boogie.Z3
                     Contract.Assert(e != null);

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

                 }

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

 

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

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

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

+                Term selectTerm = args[0];

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

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

+                }

+                return selectTerm;

+            }

+

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

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

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

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

+              }

+              else {

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

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

+              }

             }

 

             public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)

@@ -374,10 +361,7 @@ namespace Microsoft.Boogie.Z3
                     Contract.Assert(e != null);

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

                 }

-

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

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

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

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

             }

 

             public Term VisitBvOp(VCExprNAry node, LineariserOptions options)

@@ -431,129 +415,97 @@ namespace Microsoft.Boogie.Z3
             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-

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

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

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

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

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

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

             }

 

             public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(node != null);

                 Contract.Requires(options != null);

-                VCExprCustomOp op = (VCExprCustomOp)node.Op;

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

-                foreach (VCExpr arg in node)

-                {

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

-                }

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

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

             }

 

-            public Term 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 Term VisitAddOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

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

             }

 

             public Term VisitSubOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitMulOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitDivOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitModOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitLtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitLeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitGtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitGeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

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

             }

 

             public Term 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");

-                if (bvzName != null) funcName = bvzName;

-

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

-                foreach (VCExpr e in node)

-                {

-                    Contract.Assert(e != null);

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

-                }

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

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

             }

         }

     }

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index e02243ce..94184957 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -146,6 +146,14 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

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

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

+      <Name>Model</Name>

+    </ProjectReference>

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

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

+      <Name>ParserHelper</Name>

+    </ProjectReference>

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

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

       <Name>VCExpr</Name>