fixed z3api so that it works on small examples now.

6 files changed, 193 insertions, 180 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index e3ba1fa7..64533c02 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -15,10 +15,6 @@ namespace Microsoft.Boogie.Z3
 {

     public class Z3Config

     {

-        ~Z3Config()

-        {

-            config.Dispose();

-        }

         private Config config = new Config();

         private int counterexamples;

         private string logFilename;

@@ -92,15 +88,14 @@ namespace Microsoft.Boogie.Z3
         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);

+        Z3TermAst MakeForall(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);

+        Z3TermAst MakeExists(uint weight, 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);

@@ -109,6 +104,8 @@ namespace Microsoft.Boogie.Z3
         Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child);

         Z3LabeledLiterals GetRelevantLabels();

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

+        Z3TermAst MakeArraySelect(List<Z3TermAst> args);

+        Z3TermAst MakeArrayStore(List<Z3TermAst> args);

     }

 

     internal class PartitionMap

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index f3dfab69..7c41f25c 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -30,6 +30,12 @@ namespace Microsoft.Boogie.Z3
             this.z3ContextIsUsed = false;

         }

 

+        public override void Close()

+        {

+            base.Close();

+            ((Z3apiProverContext)Context).cm.z3.Dispose();

+            ((Z3apiProverContext)Context).cm.config.Config.Dispose();

+        }

         private bool z3ContextIsUsed;

 

         public void PushAxiom(VCExpr axiom)

@@ -39,6 +45,7 @@ namespace Microsoft.Boogie.Z3
             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

             cm.AddAxiom((VCExpr)axiom, linOptions);

         }

+

         private void PushConjecture(VCExpr conjecture)

         {

             Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

@@ -60,6 +67,11 @@ namespace Microsoft.Boogie.Z3
             outcome = cm.Check(out z3LabelModels);

         }

 

+        public override void PushVCExpression(VCExpr vc)

+        {

+            PushAxiom(vc);

+        }

+

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

         {

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

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 70b7f35c..9ce303f4 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -67,7 +67,6 @@ namespace Microsoft.Boogie.Z3
 

     public class Z3SafeLabeledLiterals : Z3LabeledLiterals

     {

-

         private LabeledLiterals labeledLiterals;

         public Z3SafeLabeledLiterals(LabeledLiterals labeledLiterals)

         {

@@ -86,12 +85,10 @@ namespace Microsoft.Boogie.Z3
         internal BacktrackDictionary<string, Z3TypeSafeConstDecl> functions = new BacktrackDictionary<string, Z3TypeSafeConstDecl>();

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

 

-        ~Z3SafeContext()

-        {

-            z3.Dispose();

-        }

         public Context z3;

-        private Z3Config config;

+        public Z3Config config;

+        private VCExpressionGenerator gen;

+        private Z3TypeCachedBuilder tm;

 

         public void CreateBacktrackPoint()

         {

@@ -233,47 +230,60 @@ namespace Microsoft.Boogie.Z3
             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)

+        public Z3TermAst MakeForall(uint weight, 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);

+            // List<Term> unwrapNoPatterns = Unwrap(no_patterns);

+            // List<Sort> z3Types = GetTypes(boogieTypes);

+            // List<Symbol> symbols = GetSymbols(varNames);

             Term unwrapBody = Unwrap(body);

 

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

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

+            {

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

+                bound.Add(Unwrap(t));

+            }

+            Term termAst = z3.MkForall(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody);

+            /*

             Term termAst = z3.MkQuantifier(true,

-                             DEFAULT_QUANTIFIER_WEIGHT,

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

+        public Z3TermAst MakeExists(uint weight, 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);

+            // List<Term> unwrapNoPatterns = Unwrap(no_patterns);

+            // List<Sort> z3Types = GetTypes(boogieTypes);

+            // List<Symbol> symbols = GetSymbols(varNames);

             Term unwrapBody = Unwrap(body);

 

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

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

+            {

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

+                bound.Add(Unwrap(t));

+            }

+            Term termAst = z3.MkExists(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody);

+            /*

             Term termAst = z3.MkQuantifier(false,

-                                                  DEFAULT_QUANTIFIER_WEIGHT,

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

@@ -380,8 +390,6 @@ namespace Microsoft.Boogie.Z3
                 throw new Exception("Failed Int Typecheck");

         }

 

-        private VCExpressionGenerator gen;

-

         public Z3SafeContext(Z3Config config, VCExpressionGenerator gen)

         {

             Context z3 = new Context(config.Config);

@@ -392,7 +400,7 @@ namespace Microsoft.Boogie.Z3
                 z3.EnableDebugTrace(tag);

             this.z3 = z3;

             this.config = config;

-            this.tm = new Z3TypeCachedBuilder(new Z3SafeTypeBuilder(z3));

+            this.tm = new Z3TypeCachedBuilder(this);

             this.gen = gen;

         }

 

@@ -410,18 +418,6 @@ namespace Microsoft.Boogie.Z3
             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);

@@ -504,6 +500,7 @@ namespace Microsoft.Boogie.Z3
             labels.Add(labelName, wrapLabeledExpr);

             return wrapLabeledExpr;

         }

+

         public Z3LabeledLiterals GetRelevantLabels()

         {

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

@@ -555,43 +552,17 @@ namespace Microsoft.Boogie.Z3
             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)

+        public Z3TermAst MakeArraySelect(List<Z3TermAst> args)

         {

-            return new Z3SafeType(typeAst);

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

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

         }

 

-        public Z3Type BuildBvType(BvType bvType)

+        public Z3TermAst MakeArrayStore(List<Z3TermAst> args)

         {

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

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

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

         }

-

     }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index e4dd9318..0284d219 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -28,10 +28,10 @@ namespace Microsoft.Boogie.Z3 {
     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) {

+    public Z3TermAst MakeForall(uint weight, 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) {

+    public Z3TermAst MakeExists(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

       return new Z3StubTermAst();

     }

     public List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels) {

@@ -45,9 +45,6 @@ namespace Microsoft.Boogie.Z3 {
     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();

@@ -70,5 +67,13 @@ namespace Microsoft.Boogie.Z3 {
     public Z3TermAst Make(string op, List<Z3TermAst> children) {

       return new Z3StubTermAst();

     }

+    public Z3TermAst MakeArraySelect(List<Z3TermAst> args)

+    {

+        return new Z3StubTermAst();

+    }

+    public Z3TermAst MakeArrayStore(List<Z3TermAst> args)

+    {

+        return new Z3StubTermAst();

+    }

   }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index 280e93e9..0d79bd5a 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -15,6 +15,26 @@ namespace Microsoft.Boogie.Z3
 {

     internal class Z3TypeCachedBuilder

     {

+        private class MapTypeComparator : IEqualityComparer<MapType>

+        {

+            public bool Equals(MapType x, MapType y)

+            {

+                if (x.MapArity != y.MapArity)

+                    return false;

+                for (int i = 0; i < x.MapArity; i++)

+                {

+                    if (!Equals(x.Arguments[i], y.Arguments[i]))

+                        return false;

+                }

+                return Equals(x.Result, y.Result);

+

+            }

+            public int GetHashCode(MapType mapType)

+            {

+                return mapType.GetHashCode();

+            }

+        }

+

         private class BvTypeComparator : IEqualityComparer<BvType>

         {

             public bool Equals(BvType x, BvType y)

@@ -46,20 +66,38 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        private Z3TypeBuilder builder;

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

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

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

+        private Z3Context container;

+

+        public Z3TypeCachedBuilder(Z3Context context)

+        {

+            this.container = context;

+        }

 

-        public Z3TypeCachedBuilder(Z3TypeBuilder builder)

+        private Z3Type GetMapType(MapType mapType)

         {

-            this.builder = builder;

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

+            if (!mapTypes.ContainsKey(mapType))

+            {

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

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

+                Z3Type range = GetType(mapType.Result);

+                Z3Type typeAst = BuildMapType(domain, range);

+                mapTypes.Add(mapType, typeAst);

+            }

+            Z3Type result;

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

+            Debug.Assert(containsKey);

+            return result;

         }

 

         private Z3Type GetBvType(BvType bvType)

         {

             if (!bvTypes.ContainsKey(bvType))

             {

-                Z3Type typeAst = builder.BuildBvType(bvType);

+                Z3Type typeAst = BuildBvType(bvType);

                 bvTypes.Add(bvType, typeAst);

             }

             Z3Type result;

@@ -72,7 +110,7 @@ namespace Microsoft.Boogie.Z3
         {

             if (!basicTypes.ContainsKey(basicType))

             {

-                Z3Type typeAst = builder.BuildBasicType(basicType);

+                Z3Type typeAst = BuildBasicType(basicType);

                 basicTypes.Add(basicType, typeAst);

             }

             Z3Type result;

@@ -87,16 +125,48 @@ namespace Microsoft.Boogie.Z3
                 return GetBvType((BvType)boogieType);

             else if (boogieType.GetType().Equals(typeof(BasicType)))

                 return GetBasicType((BasicType)boogieType);

+            else if (boogieType.GetType().Equals(typeof(MapType)))

+                return GetMapType((MapType)boogieType);

             else

                 throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");

         }

-    }

 

-    public class Z3Type { }

+        private Z3Type WrapType(Sort typeAst)

+        {

+            return new Z3SafeType(typeAst);

+        }

 

-    interface Z3TypeBuilder

-    {

-        Z3Type BuildBvType(BvType bvType);

-        Z3Type BuildBasicType(BasicType basicType);

+        public Z3Type BuildMapType(Z3Type domain, Z3Type range)

+        {

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

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

+            return WrapType(typeAst);

+        }

+

+        public Z3Type BuildBvType(BvType bvType)

+        {

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

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

+            return WrapType(typeAst);

+        }

+

+        public Z3Type BuildBasicType(BasicType basicType)

+        {

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

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

+        }

     }

+

+    public class Z3Type { }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index 25b674a7..b2a84c8f 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -28,13 +28,15 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        internal readonly UniqueNamer Namer;

+        internal readonly UniqueNamer namer;

+        internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;

         protected Z3Context cm;

 

         public Z3apiExprLineariser(Z3Context cm)

         {

             this.cm = cm;

-            this.Namer = new UniqueNamer();

+            this.namer = new UniqueNamer();

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

         }

 

         public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)

@@ -64,8 +66,6 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        /////////////////////////////////////////////////////////////////////////////////////

-

         public Z3TermAst Visit(VCExprNAry node, LineariserOptions options)

         {

             Contract.Requires(options != null);

@@ -96,25 +96,28 @@ namespace Microsoft.Boogie.Z3
             return node.Accept<Z3TermAst, LineariserOptions>(OpLineariser, options);

         }

 

-        /////////////////////////////////////////////////////////////////////////////////////

-

         public Z3TermAst Visit(VCExprVar node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

-            string varName = Namer.GetName(node, node.Name);

-            return cm.GetConstant(varName, node.Type);

+            if (letBindings.ContainsKey(node))

+            {

+                return letBindings[node];

+            }

+            else

+            {

+                string varName = namer.GetName(node, node.Name);

+                return cm.GetConstant(varName, node.Type);

+            }

         }

 

-        /////////////////////////////////////////////////////////////////////////////////////

-

         public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

             Contract.Assert(node.TypeParameters.Count == 0);

 

-            Namer.PushScope();

+            namer.PushScope();

             try

             {

                 List<string> varNames;

@@ -125,6 +128,7 @@ namespace Microsoft.Boogie.Z3
                 VisitTriggers(node.Triggers, options, out patterns, out no_patterns);

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

                 Z3TermAst result;

+                uint weight = 1;

 

                 /*

                 if (options.QuantifierIds)

@@ -145,25 +149,19 @@ namespace Microsoft.Boogie.Z3
                         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(") ");

-                    }

+                    weight = (uint) QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);

                 }

-                */

 

                 switch (node.Quan)

                 {

                     case Quantifier.ALL:

-                        result = cm.MakeForall(varNames, varTypes, patterns, no_patterns, body); break;

+                        result = cm.MakeForall(weight, varNames, varTypes, patterns, no_patterns, body); break;

                     case Quantifier.EX:

-                        result = cm.MakeExists(varNames, varTypes, patterns, no_patterns, body); break;

+                        result = cm.MakeExists(weight, varNames, varTypes, patterns, no_patterns, body); break;

                     default:

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

                 }

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

             finally

             {

-                Namer.PopScope();

+                namer.PopScope();

             }

         }

         

@@ -181,7 +179,7 @@ namespace Microsoft.Boogie.Z3
             varTypes = new List<Type>();

             foreach (VCExprVar var in boundVars)

             {

-                string varName = Namer.GetLocalName(var, var.Name);

+                string varName = namer.GetLocalName(var, var.Name);

                 varNames.Add(varName);

                 varTypes.Add(var.Type);

             }

@@ -209,6 +207,7 @@ namespace Microsoft.Boogie.Z3
                     }

                     else

                     {

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

                         foreach (Z3TermAst expr in exprs)

                             no_patterns.Add(expr);

                     }

@@ -216,51 +215,32 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        /////////////////////////////////////////////////////////////////////////////////////

-

         public Z3TermAst Visit(VCExprLet node, LineariserOptions options)

         {

-            Namer.PushScope();

-            try

+            foreach (VCExprLetBinding b in node)

             {

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

-                foreach (VCExprLetBinding b in node)

-                {

-                    string varName = Namer.GetLocalName(b.V, b.V.Name);

-                    Z3TermAst varAst = cm.GetConstant(varName, b.V.Type);

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

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

-                    args.Add(varAst);

-                    args.Add(defAst);

-                    equations.Add(cm.Make("EQ", args));

-                }

-                System.Diagnostics.Debug.Assert(equations.Count > 0);

-                Z3TermAst eqAst = cm.Make("AND", equations);

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

-                t.Add(eqAst);

-                t.Add(Linearise(node.Body, options));

-                return cm.Make("IMPLIES", t);

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

+                letBindings.Add(b.V, defAst);

             }

-            finally

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

+            foreach (VCExprLetBinding b in node)

             {

-                Namer.PopScope();

+                letBindings.Remove(b.V);

             }

+            return letAst;

         }  

 

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

 

-        // Lineariser for operator terms. The result (bool) is currently not used for anything

-        internal class Z3apiOpLineariser : IVCExprOpVisitor<Z3TermAst, LineariserOptions/*!*/>

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

+            private readonly Z3apiExprLineariser ExprLineariser;

 

             public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser)

             {

@@ -298,38 +278,14 @@ namespace Microsoft.Boogie.Z3
             {

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

-                }

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

-                }

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

             }

 

             public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options)

@@ -393,7 +349,7 @@ namespace Microsoft.Boogie.Z3
                 Contract.Requires(node != null);

                 VCExprLabelOp op = (VCExprLabelOp)node.Op;

                 Contract.Assert(op != null);

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

+                return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); 

             }

 

             public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options)

@@ -401,12 +357,13 @@ namespace Microsoft.Boogie.Z3
                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

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

-                foreach (VCExpr/*!*/ e in node)

+                foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);

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

                 }

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

+                return ExprLineariser.cm.MakeArraySelect(args);

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

             }

 

             public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options)

@@ -419,7 +376,8 @@ namespace Microsoft.Boogie.Z3
                     Contract.Assert(e != null);

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

                 }

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

+                return ExprLineariser.cm.MakeArrayStore(args);

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

             }

 

             public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options)

@@ -455,7 +413,7 @@ namespace Microsoft.Boogie.Z3
                 return ExprLineariser.cm.Make("ITE", args);

             }

 

-            public Z3TermAst VisitCustomOp(VCExprNAry/*!*/ node, LineariserOptions/*!*/ options)

+            public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(node != null);

                 Contract.Requires(options != null);

@@ -514,42 +472,42 @@ namespace Microsoft.Boogie.Z3
             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("<", node, options);  // arguments are always terms

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

             }

 

             public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("<=", node, options);  // arguments are always terms

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

             }

 

             public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication(">", node, options);  // arguments are always terms

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

             }

 

             public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication(">=", node, options);  // arguments are always terms

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

             }

 

             public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("<:", node, options);               // arguments are always terms

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

             }

 

             public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("<::", node, options);               // arguments are always terms

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

             }

 

             public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

@@ -561,7 +519,7 @@ namespace Microsoft.Boogie.Z3
                 string funcName = op.Func.Name;

                 Contract.Assert(funcName != null);

                 string bvzName = op.Func.FindStringAttribute("external");

-                string printedName = ExprLineariser.Namer.GetName(op.Func, funcName);

+                string printedName = ExprLineariser.namer.GetName(op.Func, funcName);

                 Contract.Assert(printedName != null);

                 if (bvzName != null) printedName = bvzName;