7 files changed, 3379 insertions, 3379 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs
index d8f17a3c..d73fc28b 100644
--- a/Source/AIFramework/VariableMap/ConstantAbstraction.cs
+++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs
@@ -1,251 +1,251 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Collections;
-  using System.Diagnostics;
-  //using System.Compiler.Analysis;
-  using Microsoft.Basetypes;
-
-  /// <summary>
-  /// Represents an invariant over constant variable assignments.
-  /// </summary>
-  public class ConstantLattice : MicroLattice {
-    enum Value {
-      Top,
-      Bottom,
-      Constant
-    }
-
-    private class Elt : Element {
-      public Value domainValue;
-      public BigNum constantValue; // valid iff domainValue == Value.Constant
-
-      public Elt(Value v) {
-        this.domainValue = v;
-      }
-
-      public Elt(BigNum i) {
-        this.domainValue = Value.Constant;
-        this.constantValue = i;
-      }
-
-      public bool IsConstant {
-        get {
-          return this.domainValue == Value.Constant;
-        }
-      }
-
-      public BigNum Constant {
-        get {
-          return this.constantValue;
-        }
-      } // only when IsConstant
-
-      [Pure]
-      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
-      }
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        if (this.IsConstant)
-          return new Elt(constantValue);
-        else
-          return new Elt(domainValue);
-      }
-    }
-
-    readonly IIntExprFactory/*!*/ factory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(factory != null);
-    }
-
-
-    public ConstantLattice(IIntExprFactory/*!*/ factory) {
-      Contract.Requires(factory != null);
-      this.factory = factory;
-      // base();
-    }
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.Top);
-      }
-    }
-
-    public override Element/*!*/ Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.Bottom);
-      }
-    }
-
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null); 
-      Elt e = (Elt)element;
-      return e.domainValue == Value.Top;
-    }
-
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.domainValue == Value.Bottom;
-    }
-
-    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
-      return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
-    }
-
-    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
-      return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
-    }
-
-    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      return Join(first, second);
-    }
-
-    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
-    {
-      //Contract.Requires(first!= null);
-      //Contract.Requires(second != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return a.Constant.Equals(b.Constant);
-    }
-
-    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      //Contract.Requires(var != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
-    }
-
-    public override IExpr GetFoldExpr(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      Contract.Assert(e.domainValue == Value.Constant);
-      return factory.Const(e.constantValue);
-    }
-
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
-    }
-
-    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-
-      IFunApp nary = e as IFunApp;
-      if (nary != null) {
-        if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
-          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
-          Contract.Assert(args != null);
-          Contract.Assert(args.Count == 2);
-          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-          // Look for "x == const" or "const == x".
-          try {
-            if (arg0 is IVariable) {
-              BigNum z;
-              if (Fold(arg1, out z)) {
-                return new Elt(z);
-              }
-            } else if (arg1 is IVariable) {
-              BigNum z;
-              if (Fold(arg0, out z)) {
-                return new Elt(z);
-              }
-            }
-          } catch (System.ArithmeticException) {
-            // fall through and return Top.  (Note, an alternative design may
-            // consider returning Bottom.)
-          }
-        }
-      }
-      return Top;
-    }
-
-    /// <summary>
-    /// Returns true if "expr" represents a constant integer expressions, in which case
-    /// "z" returns as that integer.  Otherwise, returns false, in which case "z" should
-    /// not be used by the caller.
-    ///
-    /// This method throws an System.ArithmeticException in the event that folding the
-    /// constant expression results in an arithmetic overflow or division by zero.
-    /// </summary>
-    private bool Fold(IExpr/*!*/ expr, out BigNum z) {
-      Contract.Requires(expr != null);
-      IFunApp e = expr as IFunApp;
-      if (e == null) {
-        z = BigNum.ZERO;
-        return false;
-      }
-
-      if (e.FunctionSymbol is IntSymbol) {
-        z = ((IntSymbol)e.FunctionSymbol).Value;
-        return true;
-
-      } else if (e.FunctionSymbol.Equals(Int.Negate)) {
-        IList/*<IExpr!>*//*!*/ args = e.Arguments;
-        Contract.Assert(args != null);
-        Contract.Assert(args.Count == 1);
-        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-
-        if (Fold(arg0, out z)) {
-          z = z.Neg;
-          return true;
-        }
-
-      } else if (e.Arguments.Count == 2) {
-        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
-        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(e.Arguments[1]);
-        BigNum z0, z1;
-        if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
-          if (e.FunctionSymbol.Equals(Int.Add)) {
-            z = z0 + z1;
-          } else if (e.FunctionSymbol.Equals(Int.Sub)) {
-            z = z0 - z1;
-          } else if (e.FunctionSymbol.Equals(Int.Mul)) {
-            z = z0 * z1;
-          } else if (e.FunctionSymbol.Equals(Int.Div)) {
-            z = z0 / z1;
-          } else if (e.FunctionSymbol.Equals(Int.Mod)) {
-            z = z0 % z1;
-          } else {
-            z = BigNum.ZERO;
-            return false;
-          }
-          return true;
-        }
-      }
-
-      z = BigNum.ZERO;
-      return false;
-    }
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Diagnostics.Contracts;
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Collections;
+  using System.Diagnostics;
+  //using System.Compiler.Analysis;
+  using Microsoft.Basetypes;
+
+  /// <summary>
+  /// Represents an invariant over constant variable assignments.
+  /// </summary>
+  public class ConstantLattice : MicroLattice {
+    enum Value {
+      Top,
+      Bottom,
+      Constant
+    }
+
+    private class Elt : Element {
+      public Value domainValue;
+      public BigNum constantValue; // valid iff domainValue == Value.Constant
+
+      public Elt(Value v) {
+        this.domainValue = v;
+      }
+
+      public Elt(BigNum i) {
+        this.domainValue = Value.Constant;
+        this.constantValue = i;
+      }
+
+      public bool IsConstant {
+        get {
+          return this.domainValue == Value.Constant;
+        }
+      }
+
+      public BigNum Constant {
+        get {
+          return this.constantValue;
+        }
+      } // only when IsConstant
+
+      [Pure]
+      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+      }
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        if (this.IsConstant)
+          return new Elt(constantValue);
+        else
+          return new Elt(domainValue);
+      }
+    }
+
+    readonly IIntExprFactory/*!*/ factory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(factory != null);
+    }
+
+
+    public ConstantLattice(IIntExprFactory/*!*/ factory) {
+      Contract.Requires(factory != null);
+      this.factory = factory;
+      // base();
+    }
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.Top);
+      }
+    }
+
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.Bottom);
+      }
+    }
+
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null); 
+      Elt e = (Elt)element;
+      return e.domainValue == Value.Top;
+    }
+
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.domainValue == Value.Bottom;
+    }
+
+    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
+      return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
+    }
+
+    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
+      return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
+    }
+
+    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return Join(first, second);
+    }
+
+    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+    {
+      //Contract.Requires(first!= null);
+      //Contract.Requires(second != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return a.Constant.Equals(b.Constant);
+    }
+
+    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      //Contract.Requires(var != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
+    }
+
+    public override IExpr GetFoldExpr(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      Contract.Assert(e.domainValue == Value.Constant);
+      return factory.Const(e.constantValue);
+    }
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+    }
+
+    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+
+      IFunApp nary = e as IFunApp;
+      if (nary != null) {
+        if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
+          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+          Contract.Assert(args != null);
+          Contract.Assert(args.Count == 2);
+          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+          // Look for "x == const" or "const == x".
+          try {
+            if (arg0 is IVariable) {
+              BigNum z;
+              if (Fold(arg1, out z)) {
+                return new Elt(z);
+              }
+            } else if (arg1 is IVariable) {
+              BigNum z;
+              if (Fold(arg0, out z)) {
+                return new Elt(z);
+              }
+            }
+          } catch (System.ArithmeticException) {
+            // fall through and return Top.  (Note, an alternative design may
+            // consider returning Bottom.)
+          }
+        }
+      }
+      return Top;
+    }
+
+    /// <summary>
+    /// Returns true if "expr" represents a constant integer expressions, in which case
+    /// "z" returns as that integer.  Otherwise, returns false, in which case "z" should
+    /// not be used by the caller.
+    ///
+    /// This method throws an System.ArithmeticException in the event that folding the
+    /// constant expression results in an arithmetic overflow or division by zero.
+    /// </summary>
+    private bool Fold(IExpr/*!*/ expr, out BigNum z) {
+      Contract.Requires(expr != null);
+      IFunApp e = expr as IFunApp;
+      if (e == null) {
+        z = BigNum.ZERO;
+        return false;
+      }
+
+      if (e.FunctionSymbol is IntSymbol) {
+        z = ((IntSymbol)e.FunctionSymbol).Value;
+        return true;
+
+      } else if (e.FunctionSymbol.Equals(Int.Negate)) {
+        IList/*<IExpr!>*//*!*/ args = e.Arguments;
+        Contract.Assert(args != null);
+        Contract.Assert(args.Count == 1);
+        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+
+        if (Fold(arg0, out z)) {
+          z = z.Neg;
+          return true;
+        }
+
+      } else if (e.Arguments.Count == 2) {
+        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
+        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(e.Arguments[1]);
+        BigNum z0, z1;
+        if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
+          if (e.FunctionSymbol.Equals(Int.Add)) {
+            z = z0 + z1;
+          } else if (e.FunctionSymbol.Equals(Int.Sub)) {
+            z = z0 - z1;
+          } else if (e.FunctionSymbol.Equals(Int.Mul)) {
+            z = z0 * z1;
+          } else if (e.FunctionSymbol.Equals(Int.Div)) {
+            z = z0 / z1;
+          } else if (e.FunctionSymbol.Equals(Int.Mod)) {
+            z = z0 % z1;
+          } else {
+            z = BigNum.ZERO;
+            return false;
+          }
+          return true;
+        }
+      }
+
+      z = BigNum.ZERO;
+      return false;
+    }
+  }
+}
diff --git a/Source/AIFramework/VariableMap/ConstantExpressions.cs b/Source/AIFramework/VariableMap/ConstantExpressions.cs
index fcf49b25..185c700e 100644
--- a/Source/AIFramework/VariableMap/ConstantExpressions.cs
+++ b/Source/AIFramework/VariableMap/ConstantExpressions.cs
@@ -1,538 +1,538 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-  /////////////////////////////////////////////////////////////////////////////////
-  // The Abstract domain for determining "constant" expressions
-  // i.e. It determines which expression are statically binded
-  /////////////////////////////////////////////////////////////////////////////////
-/*
-using System;
-
-namespace Microsoft.AbstractInterpretationFramework
-{
-  using Microsoft.Contracts;
-  using System.Collections.Generic;
-  using Microsoft.AbstractInterpretationFramework;
-
-  /// <summary> 
-  /// This is an abstract domain for inferring constant expressions 
-  /// </summary>
-
-  public class ConstantExpressions : Lattice
-  {
-    /// <summary>
-    /// An abstract element is made of two maps: 
-    ///   + A map from variables to expressions \cup top ( i.e. for each variable, the expression it is binded )
-    ///   + A map from variables to set of variabes      ( i.e. for each variable, the set of variables that depends on its value )
-    /// </summary>
-    private class AbstractElement: Element 
-    {
-      private Dictionary<IVariable!, BindExpr> variableBindings;
-      private Dictionary<IVariable!, List<IVariable>> variableDependences;
-      
-      static private AbstractElement! bottom;
-      static public Element! Bottom 
-      {
-        get
-        {
-          if(bottom == null)
-          {
-            bottom = new AbstractElement();
-            bottom.variableBindings = null;
-            bottom.variableDependences = null;
-          }
-          assert bottom.variableBindings == null && bottom.variableDependences == null;
-          return bottom;
-        }
-      }        
-   
-      static public Element! Top
-      {
-        get
-        {
-          return new AbstractElement();
-        }
-      }
-      
-      AbstractElement() 
-      {
-        this.variableBindings = new Dictionary<IVariable!, BindExpr>();
-        this.variableDependences = new Dictionary<IVariable!, List<IVariable>>();
-      }
-      
-      /// <summary>
-      /// Our abstract element is top if and only if it has any constraint on variables
-      /// </summary>
-      public bool IsTop
-      {
-        get
-        {
-          return this.variableBindings.Keys.Count == 0 && this.variableDependences.Keys.Count == 0;
-        }      
-      }
-
-      /// <summary>
-      /// Our abstract element is bottom if and only if the maps are null
-      /// </summary>
-      public bool IsBottom
-      {
-        get
-        {    
-          assert (this.variableBindings == null) <==> (this.variableDependences == null);
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+  /////////////////////////////////////////////////////////////////////////////////
+  // The Abstract domain for determining "constant" expressions
+  // i.e. It determines which expression are statically binded
+  /////////////////////////////////////////////////////////////////////////////////
+/*
+using System;
+
+namespace Microsoft.AbstractInterpretationFramework
+{
+  using Microsoft.Contracts;
+  using System.Collections.Generic;
+  using Microsoft.AbstractInterpretationFramework;
+
+  /// <summary> 
+  /// This is an abstract domain for inferring constant expressions 
+  /// </summary>
+
+  public class ConstantExpressions : Lattice
+  {
+    /// <summary>
+    /// An abstract element is made of two maps: 
+    ///   + A map from variables to expressions \cup top ( i.e. for each variable, the expression it is binded )
+    ///   + A map from variables to set of variabes      ( i.e. for each variable, the set of variables that depends on its value )
+    /// </summary>
+    private class AbstractElement: Element 
+    {
+      private Dictionary<IVariable!, BindExpr> variableBindings;
+      private Dictionary<IVariable!, List<IVariable>> variableDependences;
+      
+      static private AbstractElement! bottom;
+      static public Element! Bottom 
+      {
+        get
+        {
+          if(bottom == null)
+          {
+            bottom = new AbstractElement();
+            bottom.variableBindings = null;
+            bottom.variableDependences = null;
+          }
+          assert bottom.variableBindings == null && bottom.variableDependences == null;
+          return bottom;
+        }
+      }        
+   
+      static public Element! Top
+      {
+        get
+        {
+          return new AbstractElement();
+        }
+      }
+      
+      AbstractElement() 
+      {
+        this.variableBindings = new Dictionary<IVariable!, BindExpr>();
+        this.variableDependences = new Dictionary<IVariable!, List<IVariable>>();
+      }
+      
+      /// <summary>
+      /// Our abstract element is top if and only if it has any constraint on variables
+      /// </summary>
+      public bool IsTop
+      {
+        get
+        {
+          return this.variableBindings.Keys.Count == 0 && this.variableDependences.Keys.Count == 0;
+        }      
+      }
+
+      /// <summary>
+      /// Our abstract element is bottom if and only if the maps are null
+      /// </summary>
+      public bool IsBottom
+      {
+        get
+        {    
+          assert (this.variableBindings == null) <==> (this.variableDependences == null);
           return this.variableBindings == null && this.variableDependences == null;
-        }      
-      }
-
-      /// <summary>
-      /// The pointwise join...
-      /// </summary>
-      public static AbstractElement! Join(AbstractElement! left, AbstractElement! right)
-      {
+        }      
+      }
+
+      /// <summary>
+      /// The pointwise join...
+      /// </summary>
+      public static AbstractElement! Join(AbstractElement! left, AbstractElement! right)
+      {
         AbstractElement! result = new AbstractElement();
-        
-        // Put all the variables in the left
-        foreach(IVariable! var in left.variableBindings.Keys)
-        {
-          BindExpr leftVal = left.variableBindings[var];
-          assert leftVal != null;
-          
-          BindExpr rightVal = right.variableBindings[var];
-
-          if(rightVal== null)   // the expression is not there
-          {
+        
+        // Put all the variables in the left
+        foreach(IVariable! var in left.variableBindings.Keys)
+        {
+          BindExpr leftVal = left.variableBindings[var];
+          assert leftVal != null;
+          
+          BindExpr rightVal = right.variableBindings[var];
+
+          if(rightVal== null)   // the expression is not there
+          {
             result.variableBindings.Add(var, leftVal);
-          }
-          else    // both abstract elements have a definition for the variable....
-          {
-            result.variableBindings.Add(var, BindExpr.Join(leftVal, rightVal));
-          }
-        }
-      
-        // Put all the variables in the right
-        foreach(IVariable! var in right.variableBindings.Keys)
-        {
-          BindExpr rightVal = right.variableBindings[var];
-          assert rightVal != null;
-          
-          BindExpr leftVal = left.variableBindings[var];
-          
-          if(rightVal== null)   // the expression is not there
-          {
+          }
+          else    // both abstract elements have a definition for the variable....
+          {
+            result.variableBindings.Add(var, BindExpr.Join(leftVal, rightVal));
+          }
+        }
+      
+        // Put all the variables in the right
+        foreach(IVariable! var in right.variableBindings.Keys)
+        {
+          BindExpr rightVal = right.variableBindings[var];
+          assert rightVal != null;
+          
+          BindExpr leftVal = left.variableBindings[var];
+          
+          if(rightVal== null)   // the expression is not there
+          {
             result.variableBindings.Add(var, rightVal);
-          }
-          else    // both abstract elements have a definition for the variable....
-          {
-            result.variableBindings.Add(var, BindExpr.Join(rightVal, leftVal));
-          }
-        }        
-
-        // Join the dependencies...
-        foreach(IVariable! var in left.variableDependences.Keys)
-        {
-          List<IVariable> dependencies = left.variableDependences[var];
-          List<IVariable> dup = new List<IVariable>(dependencies);
-          
-          result.variableDependences.Add(var, dup);
-        }
-
-        foreach(IVariable! var in right.variableDependences.Keys)
-        {
-          if(result.variableDependences.ContainsKey(var))
-          {
-            List<IVariable> dependencies = result.variableDependences[var];
-            dependencies.AddRange(right.variableDependences[var]);
-          } 
-          else
-          {
-            List<IVariable> dependencies = right.variableDependences[var];
-            List<IVariable> dup = new List<IVariable>(dependencies);
-          
-            result.variableDependences.Add(var, dup);
-          }
-        }
-
-        // Normalize... i.e. for the variables such thas they point to an unknown expression (top) we have to update also their values
-        result.Normalize();
-
-        return result;
-      }
-      
-
-      ///<summary>
-      /// Normalize the current abstract element, in that it propagetes the "dynamic" information throughtout the abstract element
-      ///</summary>
-      public void Normalize() 
-      {
-        if(this.IsBottom)
-          return;
-        if(this.IsTop)
-          return;
-        assert this.variableBindings != null;
-        
-        bool atFixpoint = false;
-
-        while(!atFixpoint)
-        {
-          atFixpoint = true;                          // guess that we've got the fixpoint...
-
-          foreach(IVariable x in this.variableBindings.Keys) 
-          {
-            if(this.variableBindings[x].IsTop)  // It means that the variable is tied to a dynamic expression
-            {
-              foreach(IVariable y in this.variableDependences[x])   // The all the variables that depend on x are also dynamic...
-              {
-                assert x != y;                  // A variable cannot depend on itself...
-                if(!this.variableBindings[y].IsTop)
-                {
-                  this.variableBindings[y] = BindExpr.Top;
-                  atFixpoint = false;                // the assumption that we were at the fixpoint was false, we have still to propagate some information...   
-                }
-              }
-            }
-          }
-        }
-      }
-
-      /// <summary>
-      /// The pointwise meet...
-      /// </summary>
-      public static AbstractElement! Meet(AbstractElement! left, AbstractElement! right)
-      {
-        AbstractElement! result = new AbstractElement();
-
-        // Put the variables that are both in left and right
-        foreach(IVariable var in left.variableBindings.Keys)
-        {
-          if(right.variableBindings.ContainsKey(var))
-          {
-            result.variableBindings.Add(var, BindExpr.Meet(left.variableBindings[var], right.variableBindings[var]));
-          }
-        }
-      
-        // Intersect the dependencies
-        foreach(IVariable var in result.variableBindings.Keys)
-        {
-          List<IVariable> depLeft = left.variableDependences[var];
-          List<IVariable> depRight = right.variableDependences[var];
-
-          // Intersect the two sets
+          }
+          else    // both abstract elements have a definition for the variable....
+          {
+            result.variableBindings.Add(var, BindExpr.Join(rightVal, leftVal));
+          }
+        }        
+
+        // Join the dependencies...
+        foreach(IVariable! var in left.variableDependences.Keys)
+        {
+          List<IVariable> dependencies = left.variableDependences[var];
+          List<IVariable> dup = new List<IVariable>(dependencies);
+          
+          result.variableDependences.Add(var, dup);
+        }
+
+        foreach(IVariable! var in right.variableDependences.Keys)
+        {
+          if(result.variableDependences.ContainsKey(var))
+          {
+            List<IVariable> dependencies = result.variableDependences[var];
+            dependencies.AddRange(right.variableDependences[var]);
+          } 
+          else
+          {
+            List<IVariable> dependencies = right.variableDependences[var];
+            List<IVariable> dup = new List<IVariable>(dependencies);
+          
+            result.variableDependences.Add(var, dup);
+          }
+        }
+
+        // Normalize... i.e. for the variables such thas they point to an unknown expression (top) we have to update also their values
+        result.Normalize();
+
+        return result;
+      }
+      
+
+      ///<summary>
+      /// Normalize the current abstract element, in that it propagetes the "dynamic" information throughtout the abstract element
+      ///</summary>
+      public void Normalize() 
+      {
+        if(this.IsBottom)
+          return;
+        if(this.IsTop)
+          return;
+        assert this.variableBindings != null;
+        
+        bool atFixpoint = false;
+
+        while(!atFixpoint)
+        {
+          atFixpoint = true;                          // guess that we've got the fixpoint...
+
+          foreach(IVariable x in this.variableBindings.Keys) 
+          {
+            if(this.variableBindings[x].IsTop)  // It means that the variable is tied to a dynamic expression
+            {
+              foreach(IVariable y in this.variableDependences[x])   // The all the variables that depend on x are also dynamic...
+              {
+                assert x != y;                  // A variable cannot depend on itself...
+                if(!this.variableBindings[y].IsTop)
+                {
+                  this.variableBindings[y] = BindExpr.Top;
+                  atFixpoint = false;                // the assumption that we were at the fixpoint was false, we have still to propagate some information...   
+                }
+              }
+            }
+          }
+        }
+      }
+
+      /// <summary>
+      /// The pointwise meet...
+      /// </summary>
+      public static AbstractElement! Meet(AbstractElement! left, AbstractElement! right)
+      {
+        AbstractElement! result = new AbstractElement();
+
+        // Put the variables that are both in left and right
+        foreach(IVariable var in left.variableBindings.Keys)
+        {
+          if(right.variableBindings.ContainsKey(var))
+          {
+            result.variableBindings.Add(var, BindExpr.Meet(left.variableBindings[var], right.variableBindings[var]));
+          }
+        }
+      
+        // Intersect the dependencies
+        foreach(IVariable var in result.variableBindings.Keys)
+        {
+          List<IVariable> depLeft = left.variableDependences[var];
+          List<IVariable> depRight = right.variableDependences[var];
+
+          // Intersect the two sets
           result.variableDependences.Add(var, depLeft);
-          foreach(IVariable v in depRight) 
-          {
-            if(!result.variableDependences.ContainsKey(v))
-            {
+          foreach(IVariable v in depRight) 
+          {
+            if(!result.variableDependences.ContainsKey(v))
+            {
               result.variableDependences.Remove(v);
-            }
-          }              
-        } 
-
-        // Now we remove the dependencies with variables not in variableBindings
+            }
+          }              
+        } 
+
+        // Now we remove the dependencies with variables not in variableBindings
         List<IVariable>! varsToRemove = new List<IVariable>();
-    
-       foreach(IVariable var in result.
-          
-
-      }
-
-      /// <summary>
-      /// Clone the current abstract element
-      /// </summary>
-      public override Element! Clone() 
-      {
-        AbstractElement cloned = new AbstractElement();
-        foreach(IVariable var in this.variableBindings.Keys)
-        {
-          cloned.variableBindings.Add(var, this.variableBindings[var]);
-        }
-
-        foreach(IVariable var in this.variableDependences.Keys)
-        {
-          List<IVariable> dependingVars = this.variableDependences[var];
-          List<IVariable> clonedDependingVars = new List<IVariable>(dependingVars);
+    
+       foreach(IVariable var in result.
+          
+
+      }
+
+      /// <summary>
+      /// Clone the current abstract element
+      /// </summary>
+      public override Element! Clone() 
+      {
+        AbstractElement cloned = new AbstractElement();
+        foreach(IVariable var in this.variableBindings.Keys)
+        {
+          cloned.variableBindings.Add(var, this.variableBindings[var]);
+        }
+
+        foreach(IVariable var in this.variableDependences.Keys)
+        {
+          List<IVariable> dependingVars = this.variableDependences[var];
+          List<IVariable> clonedDependingVars = new List<IVariable>(dependingVars);
           cloned.variableDependences.Add(var, clonedDependingVars);
-        }
-      }
-
-      /// <summary>
-      /// Return the variables that have a binding
-      /// </summary>
-      public override ICollection<IVariable!>! FreeVariables() 
-      {
-        List<IVariable!> vars = new List<IVariable!>(this.variableBindings.Keys);
-
-        return vars;
-      }
-
-      public override string! ToString() 
-      {
+        }
+      }
+
+      /// <summary>
+      /// Return the variables that have a binding
+      /// </summary>
+      public override ICollection<IVariable!>! FreeVariables() 
+      {
+        List<IVariable!> vars = new List<IVariable!>(this.variableBindings.Keys);
+
+        return vars;
+      }
+
+      public override string! ToString() 
+      {
         string! retString = "";
-        retString += "Bindings";
-        
-        foreach(IVariable var in this.variableBindings.Keys)
-        {
-          string! toAdd = var.ToString() + " -> " + this.variableBindings[var];
-          retString += toAdd + ",";
-        }
-        
-        retString += "\nDependencies";
-        foreach(IVariable var in this.variableDependences.Keys)
-        {
-          string! toAdd = var.ToString() + " -> " + this.variableDependences[var];
-          retString += toAdd + ",";
-        }
-
-        return retString;
-      }  
-    }     
-
-    public override Element! Top 
-    {
-      get
-      {
-        return AbstractElement.Top;
-      }
-    }
-
-    public override Element! Bottom
-    {
-      get
-      {
-        return AbstractElement.Bottom;
-      }
-    }
-
-    public override bool IsTop(Element! e)
-    {
-      assert e is AbstractElement;
-      AbstractElement! absElement = (AbstractElement) e;
-      
-      return absElement.IsTop;
-    }
-
-    public override bool IsBottom(Element! e)
-    {
-      assert e is AbstractElement;
-      AbstractElement absElement = (AbstractElement) e;
-      return absElement.IsBottom;
-    }       
-
-    /// <summary>
-    /// Perform the pointwise join of the two abstract elements
-    /// </summary>
-    public override Element! NontrivialJoin(Element! a, Element! b)
-    {
-      assert a is AbstractElement;
-      assert b is AbstractElement;
-
-      AbstractElement! left = (AbstractElement!) a;
-      AbstractElement! right = (AbstractElement!) b;
-
-      return AbstractElement.Join(left, right);
-    }
-
-    /// <summary>
-    /// Perform the pointwise meet of two abstract elements
-    /// </summary>
-    public override Element! NontrivialMeet(Element! a, Element!b)
-    {
-      assert a is AbstractElement;
-      assert b is AbstractElement;
-
-      AbstractElement! left = (AbstractElement!) a;
-      AbstractElement! right = (AbstractElement!) b;
-
-      return AbstractElement.Meet(left, right);
-    }
-
-    
-  }
-
-  /// <summary>
-  /// A wrapper in order to have the algebraic datatype BindExpr := IExpr | Top
-  /// </summary>
-  abstract class BindExpr 
-  {    
-    /// <summary>
-    /// True iff this expression is instance of BindExprTop
-    /// </summary>
-    public bool IsTop
-    {
-      get
-      {
-        return this is BindExprTop;
-      }
-    }
-
-    static public BindExpr Top
-    {
-      get
-      {
-        return BindExprTop.UniqueTop;
-      }
-    }
-
-    /// <summary>
-    /// True iff this expression is instance of BindExprBottom
-    /// </summary>  
-    public bool IsBottom
-    {
-      get
-      {
-        return this is BindExprBottom;
-      }
-    }
-
-    static public BindExpr Bottom
-    {
-      get
-      {
-        return BindExprBottom.UniqueBottom;
-      }
-    }
-    
-    public static BindExpr! Join(BindExpr! left, BindExpr! right)
-    {
-      if(left.IsTop || right.IsTop)
-      {
-        return BindExpr.Top;
-      }
-      else if(left.IsBottom)
-      {
-        return right;
-      }
-      else if(right.IsBottom)
-      {
-        return left;
-      }
-      else if(left.EmbeddedExpr != right.EmbeddedExpr)
-      {
-        return BindExpr.Top;
-      }
-      else  // left.EmbeddedExpr == right.EmbeddedExpr
-      {
-        return left;
-      }      
-    }
-
-    public static BindExpr! Meet(BindExpr! left, BindExpr! right)
-    {
-      if(left.IsTop)
-      {
-        return right;
-      } 
-      else if(right.IsTop)
-      {
-        return right;
-      }
-      else if(left.IsBottom || right.IsBottom)
-      {
-        return BindExpr.Bottom;
-      }
-      else if(left.EmbeddedExpr != right.EmbeddedExpr)
-      {
-        return BindExpr.Bottom;
-      }
-      else  // left.EmbeddedExpr == right.EmbeddedExpr
-      {
-        return left;
-      }      
-    }
-
-    abstract public IExpr! EmbeddedExpr
-    {
-      get;
-    }
-
-  }
-  
-  /// <summary>
-  /// A wrapper for an integer
-  /// </summary>
-  class Expr : BindExpr
-  {
-    private IExpr! exp;
-    
-    public Expr(IExpr! exp) 
-    {
-      this.exp = exp;
-    }
-
-    override public IExpr! EmbeddedExpr 
-    {
-      get 
-      {
-        return this.exp;
-      }
-    }
-
-    public override string! ToString()
-    {
-      return this.exp.ToString();
-    }
-  }
-
-  /// <summary>
-  /// The dynamic expression 
-  /// </summary>
-  class BindExprTop : BindExpr
-  {
-    private BindExprTop top = new BindExprTop();
-    static public BindExprTop! UniqueTop
-    {
-      get
-      {
-        return this.top;
-      }
-    }
-
-    private BindExprTop() {}
-
-    override public IExpr! EmbeddedExpr
-    {
-      get
-      {
-        assert false;     // If we get there, we have an error
-      }
-    }
-
-    public override string! ToString() 
-    {
-      return "<dynamic expression>";
-    }
-  }
-
-  /// <summary>
-  /// The unreachable expression
-  /// </summary>    
-  class BindExprBottom : BindExpr
-  {
-    private BindExprBottom! bottom = new BindExprBottom();
-    static public BindExprBottom! UniqueBottom
-    {
-      get
-      {
-        return this.bottom;
-      }
-    }
-    
-    private BindExprBottom() {}
-
-    override public IExpr! EmbeddedExpr
-    {
-      get
-      {
-        assert false;
-      }
-    }
-  
-    public override string! ToString() 
-    {
-      return "<unreachable expression>";
-    }
-  }
-
-} // end namespace Microsoft.AbstractInterpretationFramework
+        retString += "Bindings";
+        
+        foreach(IVariable var in this.variableBindings.Keys)
+        {
+          string! toAdd = var.ToString() + " -> " + this.variableBindings[var];
+          retString += toAdd + ",";
+        }
+        
+        retString += "\nDependencies";
+        foreach(IVariable var in this.variableDependences.Keys)
+        {
+          string! toAdd = var.ToString() + " -> " + this.variableDependences[var];
+          retString += toAdd + ",";
+        }
+
+        return retString;
+      }  
+    }     
+
+    public override Element! Top 
+    {
+      get
+      {
+        return AbstractElement.Top;
+      }
+    }
+
+    public override Element! Bottom
+    {
+      get
+      {
+        return AbstractElement.Bottom;
+      }
+    }
+
+    public override bool IsTop(Element! e)
+    {
+      assert e is AbstractElement;
+      AbstractElement! absElement = (AbstractElement) e;
+      
+      return absElement.IsTop;
+    }
+
+    public override bool IsBottom(Element! e)
+    {
+      assert e is AbstractElement;
+      AbstractElement absElement = (AbstractElement) e;
+      return absElement.IsBottom;
+    }       
+
+    /// <summary>
+    /// Perform the pointwise join of the two abstract elements
+    /// </summary>
+    public override Element! NontrivialJoin(Element! a, Element! b)
+    {
+      assert a is AbstractElement;
+      assert b is AbstractElement;
+
+      AbstractElement! left = (AbstractElement!) a;
+      AbstractElement! right = (AbstractElement!) b;
+
+      return AbstractElement.Join(left, right);
+    }
+
+    /// <summary>
+    /// Perform the pointwise meet of two abstract elements
+    /// </summary>
+    public override Element! NontrivialMeet(Element! a, Element!b)
+    {
+      assert a is AbstractElement;
+      assert b is AbstractElement;
+
+      AbstractElement! left = (AbstractElement!) a;
+      AbstractElement! right = (AbstractElement!) b;
+
+      return AbstractElement.Meet(left, right);
+    }
+
+    
+  }
+
+  /// <summary>
+  /// A wrapper in order to have the algebraic datatype BindExpr := IExpr | Top
+  /// </summary>
+  abstract class BindExpr 
+  {    
+    /// <summary>
+    /// True iff this expression is instance of BindExprTop
+    /// </summary>
+    public bool IsTop
+    {
+      get
+      {
+        return this is BindExprTop;
+      }
+    }
+
+    static public BindExpr Top
+    {
+      get
+      {
+        return BindExprTop.UniqueTop;
+      }
+    }
+
+    /// <summary>
+    /// True iff this expression is instance of BindExprBottom
+    /// </summary>  
+    public bool IsBottom
+    {
+      get
+      {
+        return this is BindExprBottom;
+      }
+    }
+
+    static public BindExpr Bottom
+    {
+      get
+      {
+        return BindExprBottom.UniqueBottom;
+      }
+    }
+    
+    public static BindExpr! Join(BindExpr! left, BindExpr! right)
+    {
+      if(left.IsTop || right.IsTop)
+      {
+        return BindExpr.Top;
+      }
+      else if(left.IsBottom)
+      {
+        return right;
+      }
+      else if(right.IsBottom)
+      {
+        return left;
+      }
+      else if(left.EmbeddedExpr != right.EmbeddedExpr)
+      {
+        return BindExpr.Top;
+      }
+      else  // left.EmbeddedExpr == right.EmbeddedExpr
+      {
+        return left;
+      }      
+    }
+
+    public static BindExpr! Meet(BindExpr! left, BindExpr! right)
+    {
+      if(left.IsTop)
+      {
+        return right;
+      } 
+      else if(right.IsTop)
+      {
+        return right;
+      }
+      else if(left.IsBottom || right.IsBottom)
+      {
+        return BindExpr.Bottom;
+      }
+      else if(left.EmbeddedExpr != right.EmbeddedExpr)
+      {
+        return BindExpr.Bottom;
+      }
+      else  // left.EmbeddedExpr == right.EmbeddedExpr
+      {
+        return left;
+      }      
+    }
+
+    abstract public IExpr! EmbeddedExpr
+    {
+      get;
+    }
+
+  }
+  
+  /// <summary>
+  /// A wrapper for an integer
+  /// </summary>
+  class Expr : BindExpr
+  {
+    private IExpr! exp;
+    
+    public Expr(IExpr! exp) 
+    {
+      this.exp = exp;
+    }
+
+    override public IExpr! EmbeddedExpr 
+    {
+      get 
+      {
+        return this.exp;
+      }
+    }
+
+    public override string! ToString()
+    {
+      return this.exp.ToString();
+    }
+  }
+
+  /// <summary>
+  /// The dynamic expression 
+  /// </summary>
+  class BindExprTop : BindExpr
+  {
+    private BindExprTop top = new BindExprTop();
+    static public BindExprTop! UniqueTop
+    {
+      get
+      {
+        return this.top;
+      }
+    }
+
+    private BindExprTop() {}
+
+    override public IExpr! EmbeddedExpr
+    {
+      get
+      {
+        assert false;     // If we get there, we have an error
+      }
+    }
+
+    public override string! ToString() 
+    {
+      return "<dynamic expression>";
+    }
+  }
+
+  /// <summary>
+  /// The unreachable expression
+  /// </summary>    
+  class BindExprBottom : BindExpr
+  {
+    private BindExprBottom! bottom = new BindExprBottom();
+    static public BindExprBottom! UniqueBottom
+    {
+      get
+      {
+        return this.bottom;
+      }
+    }
+    
+    private BindExprBottom() {}
+
+    override public IExpr! EmbeddedExpr
+    {
+      get
+      {
+        assert false;
+      }
+    }
+  
+    public override string! ToString() 
+    {
+      return "<unreachable expression>";
+    }
+  }
+
+} // end namespace Microsoft.AbstractInterpretationFramework
 */
 \ No newline at end of file
diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs
index 78bd61a0..edda7c1e 100644
--- a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs
+++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs
@@ -1,511 +1,511 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Collections;
-  using System.Diagnostics;
-  //using System.Compiler.Analysis;
-  //using Microsoft.SpecSharp.Collections;
-  using System.Diagnostics.Contracts;
-
-  /// <summary>
-  /// Represents information about the dynamic type of a variable.  In particular, for a
-  /// variable "v", represents either Bottom, "typeof(v)==T" for some type T, or a set
-  /// of constraints "typeof(v) subtype of T_i for some number of T_i's.
-  /// </summary>
-  public class DynamicTypeLattice : MicroLattice {
-    enum What {
-      Bottom,
-      Exact,
-      Bounds
-    }
-
-    private class Elt : Element {
-      // Representation:
-      // - Bottom is represented by:  what==What.Bottom
-      // - An exact type T is represented by: what==What.Exact && ty==T
-      // - A set of type constraints T0, T1, T2, ..., T{n-1} is represented by:
-      //    -- if n==0:  what==What.Bounds && ty==null && manyBounds==null
-      //    -- if n==1:  what==What.Bounds && ty==T0 && manyBounds==null
-      //    -- if n>=2:  what==What.Bounds && ty==null &&
-      //                 manyBounds!=null && manyBounds.Length==n &&
-      //                 manyBounds[0]==T0 && manyBounds[1]==T1 && ... && manyBounds[n-1]==T{n-1}
-      //   The reason for keeping the one-and-only bound in "ty" in case n==1 is to try
-      //   to prevent the need for allocating a whole array of bounds, since 1 bound is
-      //   bound to be common.
-      // In the representation, there are no redundant bounds in manyBounds.
-      // It is assumed that the types can can occur as exact bounds form a single-inheritance
-      // hierarchy.  That is, if T0 and T1 are types that can occur as exact types, then
-      // there is no v such that typeof(v) is a subtype of both T0 and T1, unless T0 and T1 are
-      // the same type.
-      public readonly What what;
-      public readonly IExpr ty;
-      [Rep]
-      public readonly IExpr[] manyBounds;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-
-        Contract.Invariant(what != What.Bottom || ty == null && manyBounds == null);
-        Contract.Invariant(manyBounds == null || what == What.Bounds);
-        Contract.Invariant(manyBounds == null || Contract.ForAll(0, manyBounds.Length, i => manyBounds[i] != null));
-      }
-      public Elt(What what, IExpr ty) {
-        Contract.Requires(what != What.Bottom || ty == null);
-        Contract.Requires(what != What.Exact || ty != null);
-        this.what = what;
-        this.ty = ty;
-        this.manyBounds = null;
-      }
-
-      public Elt(IExpr[]/*!*/ bounds) {
-        Contract.Requires(bounds != null);
-        Contract.Requires(Contract.ForAll(0, bounds.Length, i => bounds[i] != null));
-        this.what = What.Bounds;
-        if (bounds.Length == 0) {
-          this.ty = null;
-          this.manyBounds = null;
-        } else if (bounds.Length == 1) {
-          this.ty = bounds[0];
-          this.manyBounds = null;
-        } else {
-          this.ty = null;
-          this.manyBounds = bounds;
-        }
-      }
-
-      /// <summary>
-      /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list.
-      /// </summary>
-      [NotDelayed]
-      public Elt(ArrayList /*IExpr*//*!*/ bounds, int n) {
-        Contract.Requires(bounds != null);
-        Contract.Requires(0 <= n && n <= bounds.Count);
-        this.what = What.Bounds;
-        if (n > 1) {
-          this.manyBounds = new IExpr[n];
-        }
-        int k = 0;
-        foreach (IExpr bound in bounds) {
-          if (bound != null) {
-            Contract.Assert(k != n);
-            if (n == 1) {
-              Contract.Assert(this.ty == null);
-              this.ty = bound;
-            } else {
-              Contract.Assume(manyBounds != null);
-              manyBounds[k] = bound;
-            }
-            k++;
-          }
-        }
-        Contract.Assert(k == n);
-      }
-
-      public int BoundsCount {
-        get {
-          Contract.Ensures(0 <= Contract.Result<int>());
-          if (manyBounds != null) {
-            return manyBounds.Length;
-          } else if (ty != null) {
-            return 1;
-          } else {
-            return 0;
-          }
-        }
-      }
-
-      [Pure]
-      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
-      }
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        if (this.manyBounds != null)
-          return new Elt(this.manyBounds);
-        else
-          return new Elt(this.what, this.ty);
-      }
-    }
-
-    readonly ITypeExprFactory/*!*/ factory;
-    readonly IPropExprFactory/*!*/ propFactory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(factory != null);
-      Contract.Invariant(propFactory != null);
-    }
-
-
-    public DynamicTypeLattice(ITypeExprFactory/*!*/ factory, IPropExprFactory/*!*/ propFactory) {
-      Contract.Requires(propFactory != null);
-      Contract.Requires(factory != null);
-      this.factory = factory;
-      this.propFactory = propFactory;
-      // base();
-    }
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(What.Bounds, null);
-      }
-    }
-
-    public override Element/*!*/ Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(What.Bottom, null);
-      }
-    }
-
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
-    }
-
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.what == What.Bottom;
-    }
-
-    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
-      if (a.what == What.Exact && b.what == What.Exact) {
-        Contract.Assert(a.ty != null && b.ty != null);
-        if (factory.IsTypeEqual(a.ty, b.ty)) {
-          return a;
-        } else {
-          return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));
-        }
-      }
-
-      // The result is going to be a Bounds, since at least one of the operands is a Bounds.
-      Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount);  // a preconditions is that neither operand is Top
-      int n = a.BoundsCount + b.BoundsCount;
-
-      // Special case:  a and b each has exactly one bound
-      if (n == 2) {
-        Contract.Assert(a.ty != null && b.ty != null);
-        IExpr join = factory.JoinTypes(a.ty, b.ty);
-        Contract.Assert(join != null);
-        if (join == a.ty && a.what == What.Bounds) {
-          return a;
-        } else if (join == b.ty && b.what == What.Bounds) {
-          return b;
-        } else {
-          return new Elt(What.Bounds, join);
-        }
-      }
-
-      // General case
-      ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);  // final size
-      ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n);  // a guess at the size, but could be as big as size(a)*size(b)
-      if (a.ty != null) {
-        allBounds.Add(a.ty);
-      } else {
-        allBounds.AddRange(cce.NonNull(a.manyBounds));
-      }
-      int bStart = allBounds.Count;
-      if (b.ty != null) {
-        allBounds.Add(b.ty);
-      } else {
-        allBounds.AddRange(cce.NonNull(b.manyBounds));
-      }
-      // compute the join of each pair, putting non-redundant joins into "result"
-      for (int i = 0; i < bStart; i++) {
-        IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
-        for (int j = bStart; j < allBounds.Count; j++) {
-          IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
-
-          IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
-          Contract.Assert(join != null);
-
-          int k = 0;
-          while (k < result.Count) {
-            IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);
-            if (factory.IsSubType(join, r)) {
-              // "join" is more restrictive than a bound already placed in "result",
-              // so toss out "join" and compute the join of the next pair
-              goto NEXT_PAIR;
-            } else if (factory.IsSubType(r, join)) {
-              // "join" is less restrictive than a bound already placed in "result",
-              // so toss out that old bound
-              result.RemoveAt(k);
-            } else {
-              k++;
-            }
-          }
-          result.Add(join);
-        NEXT_PAIR: {
-          }
-        }
-      }
-      return new Elt(result, result.Count);
-    }
-
-
-    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
-
-      if (a.what == What.Exact && b.what == What.Exact) {
-        Contract.Assert(a.ty != null && b.ty != null);
-        if (factory.IsTypeEqual(a.ty, b.ty)) {
-          return a;
-        } else {
-          return Bottom;
-        }
-
-      } else if (a.what == What.Exact || b.what == What.Exact) {
-        // One is Bounds, the other Exact.  Make b be the Bounds one.
-        if (a.what == What.Bounds) {
-          Elt tmp = a;
-          a = b;
-          b = tmp;
-        }
-        Contract.Assert(a.what == What.Exact && b.what == What.Bounds);
-        // Check the exact type against all bounds.  If the exact type is more restrictive
-        // than all bounds, then return it.  If some bound is not met by the exact type, return
-        // bottom.
-        Contract.Assert(a.ty != null);
-        if (b.ty != null && !factory.IsSubType(a.ty, b.ty)) {
-          return Bottom;
-        }
-        if (b.manyBounds != null) {
-          foreach (IExpr/*!*/ bound in b.manyBounds) {
-            Contract.Assert(bound != null);
-            if (!factory.IsSubType(a.ty, bound)) {
-              return Bottom;
-            }
-          }
-        }
-        return a;
-      } else {
-        // Both operands are Bounds.
-        Contract.Assert(a.what == What.Bounds && b.what == What.Bounds);
-
-        // Take all the bounds, but prune those bounds that follow from others.
-        Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount);  // a preconditions is that neither operand is Top
-        int n = a.BoundsCount + b.BoundsCount;
-        // Special case:  a and b each has exactly one bound
-        if (n == 2) {
-          Contract.Assert(a.ty != null && b.ty != null);
-          if (factory.IsSubType(a.ty, b.ty)) {
-            // a is more restrictive
-            return a;
-          } else if (factory.IsSubType(b.ty, a.ty)) {
-            // b is more restrictive
-            return b;
-          } else {
-            IExpr[]/*!*/ bounds = new IExpr[2];
-            bounds[0] = a.ty;
-            bounds[1] = b.ty;
-            return new Elt(bounds);
-          }
-        }
-
-        // General case
-        ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);
-        if (a.ty != null) {
-          allBounds.Add(a.ty);
-        } else {
-          allBounds.AddRange(cce.NonNull(a.manyBounds));
-        }
-        int bStart = allBounds.Count;
-        if (b.ty != null) {
-          allBounds.Add(b.ty);
-        } else {
-          allBounds.AddRange(cce.NonNull(b.manyBounds));
-        }
-        for (int i = 0; i < bStart; i++) {
-          IExpr/*!*/ aBound = cce.NonNull((IExpr)allBounds[i]);
-          for (int j = bStart; j < allBounds.Count; j++) {
-            IExpr bBound = (IExpr/*! Wouldn't the non-null typing in the original Spec# code had made bBound never null, 
-                                              * thus negating the need for the continue statement?*/
-                                                                                        )allBounds[j];
-            if (bBound == null) {
-              continue;
-            } else if (factory.IsSubType(aBound, bBound)) {
-              // a is more restrictive, so blot out the b bound
-              allBounds[j] = null;
-              n--;
-            } else if (factory.IsSubType(bBound, aBound)) {
-              // b is more restrictive, so blot out the a bound
-              allBounds[i] = null;
-              n--;
-              goto CONTINUE_OUTER_LOOP;
-            }
-          }
-        CONTINUE_OUTER_LOOP: {
-          }
-        }
-        Contract.Assert(1 <= n);
-        return new Elt(allBounds, n);
-      }
-    }
-
-    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      return Join(first, second);
-    }
-
-    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
-    {
-      //Contract.Requires(first != null);
-      //Contract.Requires(second != null);
-      Elt/*!*/ a = (Elt/*!*/)cce.NonNull(first);
-      Elt/*!*/ b = (Elt/*!*/)cce.NonNull(second);
-      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
-
-      if (a.what == What.Exact && b.what == What.Exact) {
-        Contract.Assert(a.ty != null && b.ty != null);
-        return factory.IsTypeEqual(a.ty, b.ty);
-      } else if (b.what == What.Exact) {
-        return false;
-      } else if (a.what == What.Exact) {
-        Contract.Assert(a.ty != null);
-        if (b.ty != null) {
-          return factory.IsSubType(a.ty, b.ty);
-        } else {
-          return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound));
-        }
-      } else {
-        Contract.Assert(a.what == What.Bounds && b.what == What.Bounds);
-        Contract.Assert(a.ty != null || a.manyBounds != null);  // a precondition is that a is not Top
-        Contract.Assert(b.ty != null || b.manyBounds != null);  // a precondition is that b is not Top
-        // Return true iff: for each constraint in b, there is a stricter constraint in a.
-        if (a.ty != null && b.ty != null) {
-          return factory.IsSubType(a.ty, b.ty);
-        } else if (a.ty != null) {
-          return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound));
-        } else if (b.ty != null) {
-          return Contract.Exists(a.manyBounds, bound => factory.IsSubType(bound, b.ty));
-        } else {
-          return Contract.ForAll(b.manyBounds, bBound => Contract.Exists(a.manyBounds, aBound => factory.IsSubType(aBound, bBound)));
-        }
-      }
-    }
-
-    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      //Contract.Requires(var != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      Elt e = (Elt)element;
-      switch (e.what) {
-        case What.Bottom:
-          return propFactory.False;
-        case What.Exact:
-          return factory.IsExactlyA(var, cce.NonNull(e.ty));
-        case What.Bounds:
-          if (e.ty == null && e.manyBounds == null) {
-            return propFactory.True;
-          } else if (e.ty != null) {
-            return factory.IsA(var, e.ty);
-          } else {
-            IExpr/*!*/ p = factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds)[0]);
-            for (int i = 1; i < e.manyBounds.Length; i++) {
-              p = propFactory.And(p, factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds[i])));
-            }
-            return p;
-          }
-        default: {
-            Contract.Assert(false);
-            throw new cce.UnreachableException();
-          }
-          throw new System.Exception();
-      }
-    }
-
-    public override IExpr GetFoldExpr(Element/*!*/ e) {
-      //Contract.Requires(e != null);
-      // cannot fold into an expression that can be substituted for the variable
-      return null;
-    }
-
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
-      if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
-        Contract.Assert(args.Count == 2);
-        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-        // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
-        if (isEq && factory.IsTypeConstant(arg0)) {
-          // swap the arguments
-          IExpr/*!*/ tmp = arg0;
-          arg0 = arg1;
-          arg1 = tmp;
-        } else if (!factory.IsTypeConstant(arg1)) {
-          return false;
-        }
-        IFunApp typeofExpr = arg0 as IFunApp;
-        if (typeofExpr != null &&
-            typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
-          Contract.Assert(typeofExpr.Arguments.Count == 1);
-          if (typeofExpr.Arguments[0] is IVariable) {
-            // we have a match
-            return true;
-          }
-        }
-      }
-      return false;
-    }
-
-    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      IFunApp nary = e as IFunApp;
-      if (nary != null) {
-
-        bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
-        if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
-          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
-          Contract.Assert(args != null);
-          Contract.Assert(args.Count == 2);
-          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-          // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
-          if (isEq && factory.IsTypeConstant(arg0)) {
-            // swap the arguments
-            IExpr/*!*/ tmp = arg0;
-            arg0 = arg1;
-            arg1 = tmp;
-          } else if (!factory.IsTypeConstant(arg1)) {
-            return Top;
-          }
-          IFunApp typeofExpr = arg0 as IFunApp;
-          if (typeofExpr != null &&
-              typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
-            Contract.Assert(typeofExpr.Arguments.Count == 1);
-            if (typeofExpr.Arguments[0] is IVariable) {
-              // we have a match
-              return new Elt(isEq ? What.Exact : What.Bounds, arg1);
-            }
-          }
-        }
-      }
-      return Top;
-    }
-
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Collections;
+  using System.Diagnostics;
+  //using System.Compiler.Analysis;
+  //using Microsoft.SpecSharp.Collections;
+  using System.Diagnostics.Contracts;
+
+  /// <summary>
+  /// Represents information about the dynamic type of a variable.  In particular, for a
+  /// variable "v", represents either Bottom, "typeof(v)==T" for some type T, or a set
+  /// of constraints "typeof(v) subtype of T_i for some number of T_i's.
+  /// </summary>
+  public class DynamicTypeLattice : MicroLattice {
+    enum What {
+      Bottom,
+      Exact,
+      Bounds
+    }
+
+    private class Elt : Element {
+      // Representation:
+      // - Bottom is represented by:  what==What.Bottom
+      // - An exact type T is represented by: what==What.Exact && ty==T
+      // - A set of type constraints T0, T1, T2, ..., T{n-1} is represented by:
+      //    -- if n==0:  what==What.Bounds && ty==null && manyBounds==null
+      //    -- if n==1:  what==What.Bounds && ty==T0 && manyBounds==null
+      //    -- if n>=2:  what==What.Bounds && ty==null &&
+      //                 manyBounds!=null && manyBounds.Length==n &&
+      //                 manyBounds[0]==T0 && manyBounds[1]==T1 && ... && manyBounds[n-1]==T{n-1}
+      //   The reason for keeping the one-and-only bound in "ty" in case n==1 is to try
+      //   to prevent the need for allocating a whole array of bounds, since 1 bound is
+      //   bound to be common.
+      // In the representation, there are no redundant bounds in manyBounds.
+      // It is assumed that the types can can occur as exact bounds form a single-inheritance
+      // hierarchy.  That is, if T0 and T1 are types that can occur as exact types, then
+      // there is no v such that typeof(v) is a subtype of both T0 and T1, unless T0 and T1 are
+      // the same type.
+      public readonly What what;
+      public readonly IExpr ty;
+      [Rep]
+      public readonly IExpr[] manyBounds;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+
+        Contract.Invariant(what != What.Bottom || ty == null && manyBounds == null);
+        Contract.Invariant(manyBounds == null || what == What.Bounds);
+        Contract.Invariant(manyBounds == null || Contract.ForAll(0, manyBounds.Length, i => manyBounds[i] != null));
+      }
+      public Elt(What what, IExpr ty) {
+        Contract.Requires(what != What.Bottom || ty == null);
+        Contract.Requires(what != What.Exact || ty != null);
+        this.what = what;
+        this.ty = ty;
+        this.manyBounds = null;
+      }
+
+      public Elt(IExpr[]/*!*/ bounds) {
+        Contract.Requires(bounds != null);
+        Contract.Requires(Contract.ForAll(0, bounds.Length, i => bounds[i] != null));
+        this.what = What.Bounds;
+        if (bounds.Length == 0) {
+          this.ty = null;
+          this.manyBounds = null;
+        } else if (bounds.Length == 1) {
+          this.ty = bounds[0];
+          this.manyBounds = null;
+        } else {
+          this.ty = null;
+          this.manyBounds = bounds;
+        }
+      }
+
+      /// <summary>
+      /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list.
+      /// </summary>
+      [NotDelayed]
+      public Elt(ArrayList /*IExpr*//*!*/ bounds, int n) {
+        Contract.Requires(bounds != null);
+        Contract.Requires(0 <= n && n <= bounds.Count);
+        this.what = What.Bounds;
+        if (n > 1) {
+          this.manyBounds = new IExpr[n];
+        }
+        int k = 0;
+        foreach (IExpr bound in bounds) {
+          if (bound != null) {
+            Contract.Assert(k != n);
+            if (n == 1) {
+              Contract.Assert(this.ty == null);
+              this.ty = bound;
+            } else {
+              Contract.Assume(manyBounds != null);
+              manyBounds[k] = bound;
+            }
+            k++;
+          }
+        }
+        Contract.Assert(k == n);
+      }
+
+      public int BoundsCount {
+        get {
+          Contract.Ensures(0 <= Contract.Result<int>());
+          if (manyBounds != null) {
+            return manyBounds.Length;
+          } else if (ty != null) {
+            return 1;
+          } else {
+            return 0;
+          }
+        }
+      }
+
+      [Pure]
+      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+      }
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        if (this.manyBounds != null)
+          return new Elt(this.manyBounds);
+        else
+          return new Elt(this.what, this.ty);
+      }
+    }
+
+    readonly ITypeExprFactory/*!*/ factory;
+    readonly IPropExprFactory/*!*/ propFactory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(factory != null);
+      Contract.Invariant(propFactory != null);
+    }
+
+
+    public DynamicTypeLattice(ITypeExprFactory/*!*/ factory, IPropExprFactory/*!*/ propFactory) {
+      Contract.Requires(propFactory != null);
+      Contract.Requires(factory != null);
+      this.factory = factory;
+      this.propFactory = propFactory;
+      // base();
+    }
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(What.Bounds, null);
+      }
+    }
+
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(What.Bottom, null);
+      }
+    }
+
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
+    }
+
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.what == What.Bottom;
+    }
+
+    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
+      if (a.what == What.Exact && b.what == What.Exact) {
+        Contract.Assert(a.ty != null && b.ty != null);
+        if (factory.IsTypeEqual(a.ty, b.ty)) {
+          return a;
+        } else {
+          return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));
+        }
+      }
+
+      // The result is going to be a Bounds, since at least one of the operands is a Bounds.
+      Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount);  // a preconditions is that neither operand is Top
+      int n = a.BoundsCount + b.BoundsCount;
+
+      // Special case:  a and b each has exactly one bound
+      if (n == 2) {
+        Contract.Assert(a.ty != null && b.ty != null);
+        IExpr join = factory.JoinTypes(a.ty, b.ty);
+        Contract.Assert(join != null);
+        if (join == a.ty && a.what == What.Bounds) {
+          return a;
+        } else if (join == b.ty && b.what == What.Bounds) {
+          return b;
+        } else {
+          return new Elt(What.Bounds, join);
+        }
+      }
+
+      // General case
+      ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);  // final size
+      ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n);  // a guess at the size, but could be as big as size(a)*size(b)
+      if (a.ty != null) {
+        allBounds.Add(a.ty);
+      } else {
+        allBounds.AddRange(cce.NonNull(a.manyBounds));
+      }
+      int bStart = allBounds.Count;
+      if (b.ty != null) {
+        allBounds.Add(b.ty);
+      } else {
+        allBounds.AddRange(cce.NonNull(b.manyBounds));
+      }
+      // compute the join of each pair, putting non-redundant joins into "result"
+      for (int i = 0; i < bStart; i++) {
+        IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
+        for (int j = bStart; j < allBounds.Count; j++) {
+          IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
+
+          IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
+          Contract.Assert(join != null);
+
+          int k = 0;
+          while (k < result.Count) {
+            IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);
+            if (factory.IsSubType(join, r)) {
+              // "join" is more restrictive than a bound already placed in "result",
+              // so toss out "join" and compute the join of the next pair
+              goto NEXT_PAIR;
+            } else if (factory.IsSubType(r, join)) {
+              // "join" is less restrictive than a bound already placed in "result",
+              // so toss out that old bound
+              result.RemoveAt(k);
+            } else {
+              k++;
+            }
+          }
+          result.Add(join);
+        NEXT_PAIR: {
+          }
+        }
+      }
+      return new Elt(result, result.Count);
+    }
+
+
+    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
+
+      if (a.what == What.Exact && b.what == What.Exact) {
+        Contract.Assert(a.ty != null && b.ty != null);
+        if (factory.IsTypeEqual(a.ty, b.ty)) {
+          return a;
+        } else {
+          return Bottom;
+        }
+
+      } else if (a.what == What.Exact || b.what == What.Exact) {
+        // One is Bounds, the other Exact.  Make b be the Bounds one.
+        if (a.what == What.Bounds) {
+          Elt tmp = a;
+          a = b;
+          b = tmp;
+        }
+        Contract.Assert(a.what == What.Exact && b.what == What.Bounds);
+        // Check the exact type against all bounds.  If the exact type is more restrictive
+        // than all bounds, then return it.  If some bound is not met by the exact type, return
+        // bottom.
+        Contract.Assert(a.ty != null);
+        if (b.ty != null && !factory.IsSubType(a.ty, b.ty)) {
+          return Bottom;
+        }
+        if (b.manyBounds != null) {
+          foreach (IExpr/*!*/ bound in b.manyBounds) {
+            Contract.Assert(bound != null);
+            if (!factory.IsSubType(a.ty, bound)) {
+              return Bottom;
+            }
+          }
+        }
+        return a;
+      } else {
+        // Both operands are Bounds.
+        Contract.Assert(a.what == What.Bounds && b.what == What.Bounds);
+
+        // Take all the bounds, but prune those bounds that follow from others.
+        Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount);  // a preconditions is that neither operand is Top
+        int n = a.BoundsCount + b.BoundsCount;
+        // Special case:  a and b each has exactly one bound
+        if (n == 2) {
+          Contract.Assert(a.ty != null && b.ty != null);
+          if (factory.IsSubType(a.ty, b.ty)) {
+            // a is more restrictive
+            return a;
+          } else if (factory.IsSubType(b.ty, a.ty)) {
+            // b is more restrictive
+            return b;
+          } else {
+            IExpr[]/*!*/ bounds = new IExpr[2];
+            bounds[0] = a.ty;
+            bounds[1] = b.ty;
+            return new Elt(bounds);
+          }
+        }
+
+        // General case
+        ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);
+        if (a.ty != null) {
+          allBounds.Add(a.ty);
+        } else {
+          allBounds.AddRange(cce.NonNull(a.manyBounds));
+        }
+        int bStart = allBounds.Count;
+        if (b.ty != null) {
+          allBounds.Add(b.ty);
+        } else {
+          allBounds.AddRange(cce.NonNull(b.manyBounds));
+        }
+        for (int i = 0; i < bStart; i++) {
+          IExpr/*!*/ aBound = cce.NonNull((IExpr)allBounds[i]);
+          for (int j = bStart; j < allBounds.Count; j++) {
+            IExpr bBound = (IExpr/*! Wouldn't the non-null typing in the original Spec# code had made bBound never null, 
+                                              * thus negating the need for the continue statement?*/
+                                                                                        )allBounds[j];
+            if (bBound == null) {
+              continue;
+            } else if (factory.IsSubType(aBound, bBound)) {
+              // a is more restrictive, so blot out the b bound
+              allBounds[j] = null;
+              n--;
+            } else if (factory.IsSubType(bBound, aBound)) {
+              // b is more restrictive, so blot out the a bound
+              allBounds[i] = null;
+              n--;
+              goto CONTINUE_OUTER_LOOP;
+            }
+          }
+        CONTINUE_OUTER_LOOP: {
+          }
+        }
+        Contract.Assert(1 <= n);
+        return new Elt(allBounds, n);
+      }
+    }
+
+    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return Join(first, second);
+    }
+
+    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+    {
+      //Contract.Requires(first != null);
+      //Contract.Requires(second != null);
+      Elt/*!*/ a = (Elt/*!*/)cce.NonNull(first);
+      Elt/*!*/ b = (Elt/*!*/)cce.NonNull(second);
+      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
+
+      if (a.what == What.Exact && b.what == What.Exact) {
+        Contract.Assert(a.ty != null && b.ty != null);
+        return factory.IsTypeEqual(a.ty, b.ty);
+      } else if (b.what == What.Exact) {
+        return false;
+      } else if (a.what == What.Exact) {
+        Contract.Assert(a.ty != null);
+        if (b.ty != null) {
+          return factory.IsSubType(a.ty, b.ty);
+        } else {
+          return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound));
+        }
+      } else {
+        Contract.Assert(a.what == What.Bounds && b.what == What.Bounds);
+        Contract.Assert(a.ty != null || a.manyBounds != null);  // a precondition is that a is not Top
+        Contract.Assert(b.ty != null || b.manyBounds != null);  // a precondition is that b is not Top
+        // Return true iff: for each constraint in b, there is a stricter constraint in a.
+        if (a.ty != null && b.ty != null) {
+          return factory.IsSubType(a.ty, b.ty);
+        } else if (a.ty != null) {
+          return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound));
+        } else if (b.ty != null) {
+          return Contract.Exists(a.manyBounds, bound => factory.IsSubType(bound, b.ty));
+        } else {
+          return Contract.ForAll(b.manyBounds, bBound => Contract.Exists(a.manyBounds, aBound => factory.IsSubType(aBound, bBound)));
+        }
+      }
+    }
+
+    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      //Contract.Requires(var != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      Elt e = (Elt)element;
+      switch (e.what) {
+        case What.Bottom:
+          return propFactory.False;
+        case What.Exact:
+          return factory.IsExactlyA(var, cce.NonNull(e.ty));
+        case What.Bounds:
+          if (e.ty == null && e.manyBounds == null) {
+            return propFactory.True;
+          } else if (e.ty != null) {
+            return factory.IsA(var, e.ty);
+          } else {
+            IExpr/*!*/ p = factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds)[0]);
+            for (int i = 1; i < e.manyBounds.Length; i++) {
+              p = propFactory.And(p, factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds[i])));
+            }
+            return p;
+          }
+        default: {
+            Contract.Assert(false);
+            throw new cce.UnreachableException();
+          }
+          throw new System.Exception();
+      }
+    }
+
+    public override IExpr GetFoldExpr(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      // cannot fold into an expression that can be substituted for the variable
+      return null;
+    }
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+      if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
+        Contract.Assert(args.Count == 2);
+        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+        // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
+        if (isEq && factory.IsTypeConstant(arg0)) {
+          // swap the arguments
+          IExpr/*!*/ tmp = arg0;
+          arg0 = arg1;
+          arg1 = tmp;
+        } else if (!factory.IsTypeConstant(arg1)) {
+          return false;
+        }
+        IFunApp typeofExpr = arg0 as IFunApp;
+        if (typeofExpr != null &&
+            typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
+          Contract.Assert(typeofExpr.Arguments.Count == 1);
+          if (typeofExpr.Arguments[0] is IVariable) {
+            // we have a match
+            return true;
+          }
+        }
+      }
+      return false;
+    }
+
+    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      IFunApp nary = e as IFunApp;
+      if (nary != null) {
+
+        bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+        if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
+          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+          Contract.Assert(args != null);
+          Contract.Assert(args.Count == 2);
+          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+          // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
+          if (isEq && factory.IsTypeConstant(arg0)) {
+            // swap the arguments
+            IExpr/*!*/ tmp = arg0;
+            arg0 = arg1;
+            arg1 = tmp;
+          } else if (!factory.IsTypeConstant(arg1)) {
+            return Top;
+          }
+          IFunApp typeofExpr = arg0 as IFunApp;
+          if (typeofExpr != null &&
+              typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
+            Contract.Assert(typeofExpr.Arguments.Count == 1);
+            if (typeofExpr.Arguments[0] is IVariable) {
+              // we have a match
+              return new Elt(isEq ? What.Exact : What.Bounds, arg1);
+            }
+          }
+        }
+      }
+      return Top;
+    }
+
+  }
+}
diff --git a/Source/AIFramework/VariableMap/Intervals.cs b/Source/AIFramework/VariableMap/Intervals.cs
index 0bf82cf4..98bf9007 100644
--- a/Source/AIFramework/VariableMap/Intervals.cs
+++ b/Source/AIFramework/VariableMap/Intervals.cs
@@ -1,871 +1,871 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-//using System.Compiler.Analysis;
-using Microsoft.AbstractInterpretationFramework.Collections;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-
-/////////////////////////////////////////////////////////////////////////////////
-// An implementation of the interval abstract domain
-/////////////////////////////////////////////////////////////////////////////////
-
-namespace Microsoft.AbstractInterpretationFramework {
-  public class IntervalLattice : MicroLattice {
-    readonly ILinearExprFactory/*!*/ factory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(factory != null);
-    }
-
-
-    public IntervalLattice(ILinearExprFactory/*!*/ factory) {
-      Contract.Requires(factory != null);
-      this.factory = factory;
-      // base();
-    }
-
-    public override bool UnderstandsBasicArithmetics {
-      get {
-        return true;
-      }
-    }
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-
-        return IntervalElement.Top;
-      }
-    }
-
-    public override Element/*!*/ Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-
-        return IntervalElement.Bottom;
-      }
-    }
-
-    /// <summary>
-    /// The paramter is the top?
-    /// </summary>
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      IntervalElement interval = (IntervalElement)element;
-
-      return interval.IsTop();
-    }
-
-    /// <summary>
-    /// The parameter is the bottom?
-    /// </summary>
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      IntervalElement interval = (IntervalElement)element;
-
-      return interval.IsBottom();
-    }
-
-    /// <summary>
-    /// The classic, pointwise, join of intervals
-    /// </summary>
-    public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
-      //Contract.Requires(right != null);
-      //Contract.Requires(left != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
-      IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
-      ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf);
-      ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup);
-
-      IntervalElement/*!*/ join = IntervalElement.Factory(inf, sup);
-
-      return join;
-    }
-
-    /// <summary>
-    /// The classic, pointwise, meet of intervals
-    /// </summary>
-    public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
-      //Contract.Requires(right != null);
-      //Contract.Requires(left != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
-      IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
-      ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf);
-      ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup);
-
-      return IntervalElement.Factory(inf, sup);
-    }
-
-
-    /// <summary>
-    /// The very simple widening of intervals, to be improved with thresholds
-    /// left is the PREVIOUS value in the iterations and right is the NEW one
-    /// </summary>
-    public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
-      //Contract.Requires(right != null);
-      //Contract.Requires(left != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left);
-      IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
-      ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf;
-      ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup;
-
-      IntervalElement widening = IntervalElement.Factory(inf, sup);
-
-      return widening;
-    }
-
-
-    /// <summary>
-    /// Return true iff the interval left is containted in right
-    /// </summary>
-    protected override bool AtMost(Element/*!*/ left, Element/*!*/ right) {
-      //Contract.Requires(right != null);
-      //Contract.Requires(left != null);
-      IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
-      IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
-      if (leftInterval.IsBottom() || rightInterval.IsTop())
-        return true;
-
-      return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup;
-    }
-
-    /// <summary>
-    /// Return just null
-    /// </summary>
-    public override IExpr GetFoldExpr(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      return null;
-    }
-
-    /// <summary>
-    /// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
-    /// </summary>
-    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      //Contract.Requires(var != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element);
-      IExpr lowerBound = null;
-      IExpr upperBound = null;
-
-      if (!(interval.Inf is InfinitaryInt)) {
-        IExpr constant = this.factory.Const(interval.Inf.Value);
-        lowerBound = this.factory.AtMost(constant, var);        // inf <= var 
-      }
-      if (!(interval.Sup is InfinitaryInt)) {
-        IExpr constant = this.factory.Const(interval.Sup.Value);
-        upperBound = this.factory.AtMost(var, constant);       // var <= inf
-      }
-
-      if (lowerBound != null && upperBound != null)
-        return this.factory.And(lowerBound, upperBound);        // inf <= var && var <= sup         
-      else
-        if (lowerBound != null)
-          return lowerBound;
-        else
-          if (upperBound != null)
-            return upperBound;
-          else      // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
-            return this.factory.True;
-    }
-
-    /// <summary>
-    /// For the moment consider just equalities. Other case must be considered
-    /// </summary>
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList /*<IExpr*//*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
-    }
-
-
-    /// <summary>
-    /// Evaluate the predicate passed as input according the semantics of intervals
-    /// </summary>
-    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
-      //Contract.Requires(pred != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      return this.EvaluatePredicateWithState(pred, null);
-    }
-
-    /// <summary>
-    /// Evaluate the predicate passed as input according the semantics of intervals and the given state.
-    /// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates 
-    /// </summary>
-    public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state) {
-      //Contract.Requires(pred != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      if (pred is IFunApp) {
-        IFunApp fun = (IFunApp)pred;
-        if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
-        {
-          IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
-          IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-          if (leftArg is IVariable) {
-            return Eval(rightArg, state);
-          } else if (rightArg is IVariable) {
-            return Eval(leftArg, state);
-          }
-        }
-      }
-      // otherwise we simply return Top
-      return IntervalElement.Top;
-    }
-
-    /// <summary>
-    /// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter
-    /// </summary>
-    private IntervalElement/*!*/ Eval(IExpr/*!*/ exp, IFunctionalMap/* Var -> Element */ state) {
-      Contract.Requires((exp != null));
-      Contract.Ensures(Contract.Result<IntervalElement>() != null);
-
-      IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
-
-      // Eval the expression by structural induction
-
-
-      if (exp is IVariable && state != null) // A variable
-      {
-        object lookup = state[exp];
-        if (lookup is IntervalElement)
-          retVal = (IntervalElement)lookup;
-        else {
-          retVal = (IntervalElement)Top;
-        }
-      } else if (exp is IFunApp) {
-        IFunApp fun = (IFunApp)exp;
-
-        if (fun.FunctionSymbol is IntSymbol)   // An integer
-        {
-          IntSymbol intSymb = (IntSymbol)fun.FunctionSymbol;
-          BigNum val = intSymb.Value;
-
-          retVal = IntervalElement.Factory(val);
-        } else if (fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
-        {
-          IExpr/*!*/ arg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
-          IntervalElement/*!*/ argEval = Eval(arg, state);
-          Contract.Assert(argEval != null);
-          IntervalElement/*!*/ zero = IntervalElement.Factory(BigNum.ZERO);
-          Contract.Assert(zero != null);
-
-          retVal = zero - argEval;
-        } else if (fun.Arguments.Count == 2) {
-          IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
-          IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-
-          IntervalElement/*!*/ leftVal = Eval(left, state);
-          Contract.Assert(leftVal != null);
-          IntervalElement/*!*/ rightVal = Eval(right, state);
-          Contract.Assert(rightVal != null);
-
-          if (fun.FunctionSymbol.Equals(Int.Add))
-            retVal = leftVal + rightVal;
-          else if (fun.FunctionSymbol.Equals(Int.Sub))
-            retVal = leftVal - rightVal;
-          else if (fun.FunctionSymbol.Equals(Int.Mul))
-            retVal = leftVal * rightVal;
-          else if (fun.FunctionSymbol.Equals(Int.Div))
-            retVal = leftVal / rightVal;
-          else if (fun.FunctionSymbol.Equals(Int.Mod))
-            retVal = leftVal % rightVal;
-        }
-      }
-
-      return retVal;
-    }
-
-    /// <summary> 
-    /// Inner class standing for an interval on integers, possibly unbounded
-    /// </summary>
-    private class IntervalElement : Element {
-      protected static readonly IntervalElement/*!*/ TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity());    // Top    = [-oo , +oo]
-      protected static readonly IntervalElement/*!*/ BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo] 
-
-      private readonly ExtendedInt/*!*/ inf;
-      private readonly ExtendedInt/*!*/ sup;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-        Contract.Invariant(inf != null);
-        Contract.Invariant(sup != null);
-      }
-
-      public ExtendedInt/*!*/ Inf {
-        get {
-          Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
-          return inf;
-        }
-      }
-
-      public ExtendedInt/*!*/ Sup {
-        get {
-          Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
-          return sup;
-        }
-      }
-
-      // Construct the inteval [val, val]
-      protected IntervalElement(BigNum val) {
-        this.inf = this.sup = ExtendedInt.Factory(val);
-        // base();
-      }
-
-      // Construct the interval [inf, sup]
-      protected IntervalElement(BigNum infInt, BigNum supInt) {
-        this.inf = ExtendedInt.Factory(infInt);
-        this.sup = ExtendedInt.Factory(supInt);
-        // base();   // to please the compiler...
-      }
-
-      protected IntervalElement(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-        Contract.Requires(sup != null);
-        Contract.Requires(inf != null);
-        this.inf = inf;
-        this.sup = sup;
-        // base();
-      }
-
-      // Construct an Interval
-      public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-        Contract.Requires((sup != null));
-        Contract.Requires((inf != null));
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        if (inf is MinusInfinity && sup is PlusInfinity)
-          return Top;
-        if (inf > sup)
-          return Bottom;
-        // otherwise...
-        return new IntervalElement(inf, sup);
-      }
-
-      public static IntervalElement/*!*/ Factory(BigNum i) {
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        return new IntervalElement(i);
-      }
-
-      public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
-        ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
-
-        return Factory(i, s);
-      }
-
-      static public IntervalElement/*!*/ Top {
-        get {
-          Contract.Ensures(Contract.Result<IntervalElement>() != null);
-
-          return TopInterval;
-        }
-      }
-
-      static public IntervalElement/*!*/ Bottom {
-        get {
-          Contract.Ensures(Contract.Result<IntervalElement>() != null);
-
-          return BottomInterval;
-        }
-      }
-
-      public bool IsTop() {
-        return this.inf is MinusInfinity && this.sup is PlusInfinity;
-      }
-
-      public bool IsBottom() {
-        return this.inf > this.sup;
-      }
-
-      #region Below are the arithmetic operations lifted to intervals
-
-      // Addition
-      public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
-        Contract.Requires(b != null);
-        Contract.Requires(a != null);
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        ExtendedInt/*!*/ inf = a.inf + b.inf;
-        Contract.Assert(inf != null);
-        ExtendedInt/*!*/ sup = a.sup + b.sup;
-        Contract.Assert(sup != null);
-
-        return Factory(inf, sup);
-      }
-
-      // Subtraction
-      public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
-        Contract.Requires(b != null);
-        Contract.Requires(a != null);
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        ExtendedInt/*!*/ inf = a.inf - b.sup;
-        Contract.Assert(inf != null);
-
-        ExtendedInt/*!*/ sup = a.sup - b.inf;
-        Contract.Assert(sup != null);
-        IntervalElement/*!*/ sub = Factory(inf, sup);
-        Contract.Assert(sub != null);
-
-        return sub;
-      }
-
-      // Multiplication
-      public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
-        Contract.Requires(b != null);
-        Contract.Requires(a != null);
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        ExtendedInt/*!*/ infinf = a.inf * b.inf;
-        Contract.Assert(infinf != null);
-        ExtendedInt/*!*/ infsup = a.inf * b.sup;
-        Contract.Assert(infsup != null);
-        ExtendedInt/*!*/ supinf = a.sup * b.inf;
-        Contract.Assert(supinf != null);
-        ExtendedInt/*!*/ supsup = a.sup * b.sup;
-        Contract.Assert(supsup != null);
-
-        ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
-        Contract.Assert(inf != null);
-        ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
-        Contract.Assert(sup != null);
-
-        return Factory(inf, sup);
-      }
-
-      // Division
-      public static IntervalElement/*!*/ operator /(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
-        Contract.Requires(b != null);
-        Contract.Requires(a != null);
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        if (b.inf.IsZero && b.sup.IsZero)   //  Check division by zero
-          return IntervalElement.Top;
-
-        ExtendedInt/*!*/ infinf = a.inf / b.inf;
-        Contract.Assert(infinf != null);
-        ExtendedInt/*!*/ infsup = a.inf / b.sup;
-        Contract.Assert(infsup != null);
-        ExtendedInt/*!*/ supinf = a.sup / b.inf;
-        Contract.Assert(supinf != null);
-        ExtendedInt/*!*/ supsup = a.sup / b.sup;
-        Contract.Assert(supsup != null);
-
-        ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
-        Contract.Assert(inf != null);
-        ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
-        Contract.Assert(sup != null);
-
-        return Factory(inf, sup);
-      }
-
-      // Division
-      public static IntervalElement/*!*/ operator %(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
-        Contract.Requires(b != null);
-        Contract.Requires(a != null);
-        Contract.Ensures(Contract.Result<IntervalElement>() != null);
-        if (b.inf.IsZero && b.sup.IsZero)   //  Check division by zero
-          return IntervalElement.Top;
-
-        ExtendedInt/*!*/ infinf = a.inf % b.inf;
-        Contract.Assert(infinf != null);
-        ExtendedInt/*!*/ infsup = a.inf % b.sup;
-        Contract.Assert(infsup != null);
-        ExtendedInt/*!*/ supinf = a.sup % b.inf;
-        Contract.Assert(supinf != null);
-        ExtendedInt/*!*/ supsup = a.sup % b.sup;
-        Contract.Assert(supsup != null);
-
-        ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
-        ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
-
-        return Factory(inf, sup);
-      }
-
-      #endregion
-
-      #region Overriden methods
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        // Real copying should not be needed because intervals are immutable?
-        return this;
-        /*
-            int valInf = this.inf.Value;
-            int valSup = this.sup.Value;
-
-            ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
-            ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
-
-            return Factory(clonedInf, clonedSup);
-            */
-      }
-
-      [Pure]
-      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
-      }
-
-      [Pure]
-      public override string/*!*/ ToString() {
-        Contract.Ensures(Contract.Result<string>() != null);
-        return "[" + this.inf + ", " + this.sup + "]";
-      }
-
-      #endregion
-    }
-  }
-
-
-  /// The interface for an extended integer
-  /// 
-  [ContractClass(typeof(ExtendedIntContracts))]
-  abstract class ExtendedInt {
-    private static readonly PlusInfinity/*!*/ cachedPlusInf = new PlusInfinity();
-    private static readonly MinusInfinity/*!*/ cachedMinusInf = new MinusInfinity();
-
-    static public ExtendedInt/*!*/ PlusInfinity {
-      get {
-        Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
-        return cachedPlusInf;
-      }
-    }
-
-    static public ExtendedInt/*!*/ MinusInfinity {
-      get {
-        Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
-        return cachedMinusInf;
-      }
-    }
-
-    public abstract BigNum Value {
-      get;
-    }
-
-    public abstract int Signum {
-      get;
-    }
-
-    public bool IsZero {
-      get {
-        return Signum == 0;
-      }
-    }
-
-    public bool IsPositive {
-      get {
-        return Signum > 0;
-      }
-    }
-
-    public bool IsNegative {
-      get {
-        return Signum < 0;
-      }
-    }
-
-
-    #region Below are the extensions of arithmetic operations on extended integers
-
-    // Addition
-    public static ExtendedInt/*!*/ operator +(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (a is InfinitaryInt) {
-        return a;
-      } else if (b is InfinitaryInt) {
-        return b;
-      } else {
-        return ExtendedInt.Factory(a.Value + b.Value);
-      }
-    }
-
-    // Subtraction
-    public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (a is InfinitaryInt) {
-        return a;
-      } else if (b is InfinitaryInt) {
-        return UnaryMinus(b);
-      } else {
-        return ExtendedInt.Factory(a.Value - b.Value);
-      }
-    }
-
-    // Unary minus
-    public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a) {
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      // BUGBUG: Some compiler error prevents the unary minus operator from being used
-      return UnaryMinus(a);
-    }
-
-    // Unary minus
-    public static ExtendedInt/*!*/ UnaryMinus(ExtendedInt/*!*/ a) {
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (a is PlusInfinity)
-        return cachedMinusInf;
-      if (a is MinusInfinity)
-        return cachedPlusInf;
-      else // a is a PureInteger
-        return new PureInteger(-a.Value);
-    }
-
-    // Multiplication
-    public static ExtendedInt/*!*/ operator *(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (a.IsZero) {
-        return a;
-      } else if (b.IsZero) {
-        return b;
-      } else if (a is InfinitaryInt) {
-        if (b.IsPositive) {
-          return a;
-        } else {
-          return UnaryMinus(a);
-        }
-      } else if (b is InfinitaryInt) {
-        if (a.IsPositive) {
-          return b;
-        } else {
-          return UnaryMinus(b);
-        }
-      } else {
-        return ExtendedInt.Factory(a.Value * b.Value);
-      }
-    }
-
-    // Division
-    public static ExtendedInt/*!*/ operator /(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (b.IsZero) {
-        return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
-      }
-      if (a is InfinitaryInt) {
-        return a;
-      } else if (b is InfinitaryInt) {
-        return b;
-      } else {
-        return ExtendedInt.Factory(a.Value / b.Value);
-      }
-    }
-
-    // Modulo
-    public static ExtendedInt/*!*/ operator %(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (b.IsZero) {
-        return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
-      }
-      if (a is InfinitaryInt) {
-        return a;
-      } else if (b is InfinitaryInt) {
-        return b;
-      } else {
-        return ExtendedInt.Factory(a.Value % b.Value);
-      }
-    }
-
-    #endregion
-
-    #region Inf and Sup operations
-
-    public abstract int CompareTo(ExtendedInt/*!*/ that);
-
-    public static bool operator <(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-      Contract.Requires(sup != null);
-      Contract.Requires(inf != null);
-      return inf.CompareTo(sup) < 0;
-    }
-
-    public static bool operator >(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-      Contract.Requires(sup != null);
-      Contract.Requires(inf != null);
-      return inf.CompareTo(sup) > 0;
-    }
-
-    public static bool operator <=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-      Contract.Requires(sup != null);
-      Contract.Requires(inf != null);
-      return inf.CompareTo(sup) <= 0;
-    }
-
-    public static bool operator >=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-      Contract.Requires(sup != null);
-      Contract.Requires(inf != null);
-      Contract.Requires(inf != null && sup != null);
-      return inf.CompareTo(sup) >= 0;
-    }
-
-    public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-      Contract.Requires(sup != null);
-      Contract.Requires(inf != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (inf < sup)
-        return inf;
-      else
-        return sup;
-    }
-
-    public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
-      Contract.Requires(d != null);
-      Contract.Requires(c != null);
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      ExtendedInt/*!*/ infab = Inf(a, b);
-      Contract.Assert(infab != null);
-      ExtendedInt/*!*/ infcd = Inf(c, d);
-      Contract.Assert(infcd != null);
-
-      return Inf(infab, infcd);
-    }
-
-    public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
-      Contract.Requires(sup != null);
-      Contract.Requires(inf != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      if (inf > sup)
-        return inf;
-      else
-        return sup;
-    }
-
-    public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
-      Contract.Requires(d != null);
-      Contract.Requires(c != null);
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      ExtendedInt/*!*/ supab = Sup(a, b);
-      Contract.Assert(supab != null);
-      ExtendedInt/*!*/ supcd = Sup(c, d);
-      Contract.Assert(supcd != null);
-
-      return Sup(supab, supcd);
-    }
-
-    #endregion
-
-    // Return the ExtendedInt corresponding to the value
-    public static ExtendedInt/*!*/ Factory(BigNum val) {
-      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-      return new PureInteger(val);
-    }
-  }
-  [ContractClassFor(typeof(ExtendedInt))]
-  abstract class ExtendedIntContracts : ExtendedInt {
-    public override int CompareTo(ExtendedInt that) {
-      Contract.Requires(that != null);
-      throw new NotImplementedException();
-    }
-  }
-
-  // Stands for a normal (finite) integer x
-  class PureInteger : ExtendedInt {
-    public PureInteger(BigNum i) {
-      this.val = i;
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return this.Value.ToString();
-    }
-
-    private BigNum val;
-    public override BigNum Value {
-      get {
-        return this.val;
-      }
-    }
-
-    public override int Signum {
-      get {
-        return val.Signum;
-      }
-    }
-
-    public override int CompareTo(ExtendedInt/*!*/ that) {
-      //Contract.Requires(that != null);
-      if (that is PlusInfinity)
-        return -1;
-      else if (that is PureInteger)
-        return this.Value.CompareTo(that.Value);
-      else // then that is a MinusInfinity
-        return 1;
-    }
-  }
-
-  abstract class InfinitaryInt : ExtendedInt {
-    public override BigNum Value {
-      get {
-        throw new InvalidOperationException();
-      }
-    }
-  }
-
-  class PlusInfinity : InfinitaryInt {
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return "+oo";
-    }
-
-    public override int Signum {
-      get {
-        return 1;
-      }
-    }
-
-    public override int CompareTo(ExtendedInt/*!*/ that) {
-      //Contract.Requires(that != null);
-      if (that is PlusInfinity)
-        return 0;
-      else
-        return 1;
-    }
-  }
-
-  class MinusInfinity : InfinitaryInt {
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return "-oo";
-    }
-
-    public override int Signum {
-      get {
-        return -1;
-      }
-    }
-
-    public override int CompareTo(ExtendedInt/*!*/ that) {
-      //Contract.Requires(that != null);
-      if (that is MinusInfinity)
-        return 0;
-      else
-        return -1;
-    }
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+//using System.Compiler.Analysis;
+using Microsoft.AbstractInterpretationFramework.Collections;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+
+/////////////////////////////////////////////////////////////////////////////////
+// An implementation of the interval abstract domain
+/////////////////////////////////////////////////////////////////////////////////
+
+namespace Microsoft.AbstractInterpretationFramework {
+  public class IntervalLattice : MicroLattice {
+    readonly ILinearExprFactory/*!*/ factory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(factory != null);
+    }
+
+
+    public IntervalLattice(ILinearExprFactory/*!*/ factory) {
+      Contract.Requires(factory != null);
+      this.factory = factory;
+      // base();
+    }
+
+    public override bool UnderstandsBasicArithmetics {
+      get {
+        return true;
+      }
+    }
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+
+        return IntervalElement.Top;
+      }
+    }
+
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+
+        return IntervalElement.Bottom;
+      }
+    }
+
+    /// <summary>
+    /// The paramter is the top?
+    /// </summary>
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      IntervalElement interval = (IntervalElement)element;
+
+      return interval.IsTop();
+    }
+
+    /// <summary>
+    /// The parameter is the bottom?
+    /// </summary>
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      IntervalElement interval = (IntervalElement)element;
+
+      return interval.IsBottom();
+    }
+
+    /// <summary>
+    /// The classic, pointwise, join of intervals
+    /// </summary>
+    public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
+      //Contract.Requires(right != null);
+      //Contract.Requires(left != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+      IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
+      ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf);
+      ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup);
+
+      IntervalElement/*!*/ join = IntervalElement.Factory(inf, sup);
+
+      return join;
+    }
+
+    /// <summary>
+    /// The classic, pointwise, meet of intervals
+    /// </summary>
+    public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
+      //Contract.Requires(right != null);
+      //Contract.Requires(left != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+      IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
+      ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf);
+      ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup);
+
+      return IntervalElement.Factory(inf, sup);
+    }
+
+
+    /// <summary>
+    /// The very simple widening of intervals, to be improved with thresholds
+    /// left is the PREVIOUS value in the iterations and right is the NEW one
+    /// </summary>
+    public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
+      //Contract.Requires(right != null);
+      //Contract.Requires(left != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left);
+      IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
+      ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf;
+      ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup;
+
+      IntervalElement widening = IntervalElement.Factory(inf, sup);
+
+      return widening;
+    }
+
+
+    /// <summary>
+    /// Return true iff the interval left is containted in right
+    /// </summary>
+    protected override bool AtMost(Element/*!*/ left, Element/*!*/ right) {
+      //Contract.Requires(right != null);
+      //Contract.Requires(left != null);
+      IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+      IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
+      if (leftInterval.IsBottom() || rightInterval.IsTop())
+        return true;
+
+      return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup;
+    }
+
+    /// <summary>
+    /// Return just null
+    /// </summary>
+    public override IExpr GetFoldExpr(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      return null;
+    }
+
+    /// <summary>
+    /// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
+    /// </summary>
+    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      //Contract.Requires(var != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element);
+      IExpr lowerBound = null;
+      IExpr upperBound = null;
+
+      if (!(interval.Inf is InfinitaryInt)) {
+        IExpr constant = this.factory.Const(interval.Inf.Value);
+        lowerBound = this.factory.AtMost(constant, var);        // inf <= var 
+      }
+      if (!(interval.Sup is InfinitaryInt)) {
+        IExpr constant = this.factory.Const(interval.Sup.Value);
+        upperBound = this.factory.AtMost(var, constant);       // var <= inf
+      }
+
+      if (lowerBound != null && upperBound != null)
+        return this.factory.And(lowerBound, upperBound);        // inf <= var && var <= sup         
+      else
+        if (lowerBound != null)
+          return lowerBound;
+        else
+          if (upperBound != null)
+            return upperBound;
+          else      // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
+            return this.factory.True;
+    }
+
+    /// <summary>
+    /// For the moment consider just equalities. Other case must be considered
+    /// </summary>
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList /*<IExpr*//*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+    }
+
+
+    /// <summary>
+    /// Evaluate the predicate passed as input according the semantics of intervals
+    /// </summary>
+    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
+      //Contract.Requires(pred != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return this.EvaluatePredicateWithState(pred, null);
+    }
+
+    /// <summary>
+    /// Evaluate the predicate passed as input according the semantics of intervals and the given state.
+    /// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates 
+    /// </summary>
+    public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state) {
+      //Contract.Requires(pred != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      if (pred is IFunApp) {
+        IFunApp fun = (IFunApp)pred;
+        if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
+        {
+          IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+          IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+          if (leftArg is IVariable) {
+            return Eval(rightArg, state);
+          } else if (rightArg is IVariable) {
+            return Eval(leftArg, state);
+          }
+        }
+      }
+      // otherwise we simply return Top
+      return IntervalElement.Top;
+    }
+
+    /// <summary>
+    /// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter
+    /// </summary>
+    private IntervalElement/*!*/ Eval(IExpr/*!*/ exp, IFunctionalMap/* Var -> Element */ state) {
+      Contract.Requires((exp != null));
+      Contract.Ensures(Contract.Result<IntervalElement>() != null);
+
+      IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
+
+      // Eval the expression by structural induction
+
+
+      if (exp is IVariable && state != null) // A variable
+      {
+        object lookup = state[exp];
+        if (lookup is IntervalElement)
+          retVal = (IntervalElement)lookup;
+        else {
+          retVal = (IntervalElement)Top;
+        }
+      } else if (exp is IFunApp) {
+        IFunApp fun = (IFunApp)exp;
+
+        if (fun.FunctionSymbol is IntSymbol)   // An integer
+        {
+          IntSymbol intSymb = (IntSymbol)fun.FunctionSymbol;
+          BigNum val = intSymb.Value;
+
+          retVal = IntervalElement.Factory(val);
+        } else if (fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
+        {
+          IExpr/*!*/ arg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+          IntervalElement/*!*/ argEval = Eval(arg, state);
+          Contract.Assert(argEval != null);
+          IntervalElement/*!*/ zero = IntervalElement.Factory(BigNum.ZERO);
+          Contract.Assert(zero != null);
+
+          retVal = zero - argEval;
+        } else if (fun.Arguments.Count == 2) {
+          IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+          IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+
+          IntervalElement/*!*/ leftVal = Eval(left, state);
+          Contract.Assert(leftVal != null);
+          IntervalElement/*!*/ rightVal = Eval(right, state);
+          Contract.Assert(rightVal != null);
+
+          if (fun.FunctionSymbol.Equals(Int.Add))
+            retVal = leftVal + rightVal;
+          else if (fun.FunctionSymbol.Equals(Int.Sub))
+            retVal = leftVal - rightVal;
+          else if (fun.FunctionSymbol.Equals(Int.Mul))
+            retVal = leftVal * rightVal;
+          else if (fun.FunctionSymbol.Equals(Int.Div))
+            retVal = leftVal / rightVal;
+          else if (fun.FunctionSymbol.Equals(Int.Mod))
+            retVal = leftVal % rightVal;
+        }
+      }
+
+      return retVal;
+    }
+
+    /// <summary> 
+    /// Inner class standing for an interval on integers, possibly unbounded
+    /// </summary>
+    private class IntervalElement : Element {
+      protected static readonly IntervalElement/*!*/ TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity());    // Top    = [-oo , +oo]
+      protected static readonly IntervalElement/*!*/ BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo] 
+
+      private readonly ExtendedInt/*!*/ inf;
+      private readonly ExtendedInt/*!*/ sup;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(inf != null);
+        Contract.Invariant(sup != null);
+      }
+
+      public ExtendedInt/*!*/ Inf {
+        get {
+          Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
+          return inf;
+        }
+      }
+
+      public ExtendedInt/*!*/ Sup {
+        get {
+          Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
+          return sup;
+        }
+      }
+
+      // Construct the inteval [val, val]
+      protected IntervalElement(BigNum val) {
+        this.inf = this.sup = ExtendedInt.Factory(val);
+        // base();
+      }
+
+      // Construct the interval [inf, sup]
+      protected IntervalElement(BigNum infInt, BigNum supInt) {
+        this.inf = ExtendedInt.Factory(infInt);
+        this.sup = ExtendedInt.Factory(supInt);
+        // base();   // to please the compiler...
+      }
+
+      protected IntervalElement(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+        Contract.Requires(sup != null);
+        Contract.Requires(inf != null);
+        this.inf = inf;
+        this.sup = sup;
+        // base();
+      }
+
+      // Construct an Interval
+      public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+        Contract.Requires((sup != null));
+        Contract.Requires((inf != null));
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        if (inf is MinusInfinity && sup is PlusInfinity)
+          return Top;
+        if (inf > sup)
+          return Bottom;
+        // otherwise...
+        return new IntervalElement(inf, sup);
+      }
+
+      public static IntervalElement/*!*/ Factory(BigNum i) {
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        return new IntervalElement(i);
+      }
+
+      public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
+        ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
+
+        return Factory(i, s);
+      }
+
+      static public IntervalElement/*!*/ Top {
+        get {
+          Contract.Ensures(Contract.Result<IntervalElement>() != null);
+
+          return TopInterval;
+        }
+      }
+
+      static public IntervalElement/*!*/ Bottom {
+        get {
+          Contract.Ensures(Contract.Result<IntervalElement>() != null);
+
+          return BottomInterval;
+        }
+      }
+
+      public bool IsTop() {
+        return this.inf is MinusInfinity && this.sup is PlusInfinity;
+      }
+
+      public bool IsBottom() {
+        return this.inf > this.sup;
+      }
+
+      #region Below are the arithmetic operations lifted to intervals
+
+      // Addition
+      public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+        Contract.Requires(b != null);
+        Contract.Requires(a != null);
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        ExtendedInt/*!*/ inf = a.inf + b.inf;
+        Contract.Assert(inf != null);
+        ExtendedInt/*!*/ sup = a.sup + b.sup;
+        Contract.Assert(sup != null);
+
+        return Factory(inf, sup);
+      }
+
+      // Subtraction
+      public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+        Contract.Requires(b != null);
+        Contract.Requires(a != null);
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        ExtendedInt/*!*/ inf = a.inf - b.sup;
+        Contract.Assert(inf != null);
+
+        ExtendedInt/*!*/ sup = a.sup - b.inf;
+        Contract.Assert(sup != null);
+        IntervalElement/*!*/ sub = Factory(inf, sup);
+        Contract.Assert(sub != null);
+
+        return sub;
+      }
+
+      // Multiplication
+      public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+        Contract.Requires(b != null);
+        Contract.Requires(a != null);
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        ExtendedInt/*!*/ infinf = a.inf * b.inf;
+        Contract.Assert(infinf != null);
+        ExtendedInt/*!*/ infsup = a.inf * b.sup;
+        Contract.Assert(infsup != null);
+        ExtendedInt/*!*/ supinf = a.sup * b.inf;
+        Contract.Assert(supinf != null);
+        ExtendedInt/*!*/ supsup = a.sup * b.sup;
+        Contract.Assert(supsup != null);
+
+        ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+        Contract.Assert(inf != null);
+        ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+        Contract.Assert(sup != null);
+
+        return Factory(inf, sup);
+      }
+
+      // Division
+      public static IntervalElement/*!*/ operator /(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+        Contract.Requires(b != null);
+        Contract.Requires(a != null);
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        if (b.inf.IsZero && b.sup.IsZero)   //  Check division by zero
+          return IntervalElement.Top;
+
+        ExtendedInt/*!*/ infinf = a.inf / b.inf;
+        Contract.Assert(infinf != null);
+        ExtendedInt/*!*/ infsup = a.inf / b.sup;
+        Contract.Assert(infsup != null);
+        ExtendedInt/*!*/ supinf = a.sup / b.inf;
+        Contract.Assert(supinf != null);
+        ExtendedInt/*!*/ supsup = a.sup / b.sup;
+        Contract.Assert(supsup != null);
+
+        ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+        Contract.Assert(inf != null);
+        ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+        Contract.Assert(sup != null);
+
+        return Factory(inf, sup);
+      }
+
+      // Division
+      public static IntervalElement/*!*/ operator %(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+        Contract.Requires(b != null);
+        Contract.Requires(a != null);
+        Contract.Ensures(Contract.Result<IntervalElement>() != null);
+        if (b.inf.IsZero && b.sup.IsZero)   //  Check division by zero
+          return IntervalElement.Top;
+
+        ExtendedInt/*!*/ infinf = a.inf % b.inf;
+        Contract.Assert(infinf != null);
+        ExtendedInt/*!*/ infsup = a.inf % b.sup;
+        Contract.Assert(infsup != null);
+        ExtendedInt/*!*/ supinf = a.sup % b.inf;
+        Contract.Assert(supinf != null);
+        ExtendedInt/*!*/ supsup = a.sup % b.sup;
+        Contract.Assert(supsup != null);
+
+        ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+        ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+
+        return Factory(inf, sup);
+      }
+
+      #endregion
+
+      #region Overriden methods
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        // Real copying should not be needed because intervals are immutable?
+        return this;
+        /*
+            int valInf = this.inf.Value;
+            int valSup = this.sup.Value;
+
+            ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
+            ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
+
+            return Factory(clonedInf, clonedSup);
+            */
+      }
+
+      [Pure]
+      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+      }
+
+      [Pure]
+      public override string/*!*/ ToString() {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return "[" + this.inf + ", " + this.sup + "]";
+      }
+
+      #endregion
+    }
+  }
+
+
+  /// The interface for an extended integer
+  /// 
+  [ContractClass(typeof(ExtendedIntContracts))]
+  abstract class ExtendedInt {
+    private static readonly PlusInfinity/*!*/ cachedPlusInf = new PlusInfinity();
+    private static readonly MinusInfinity/*!*/ cachedMinusInf = new MinusInfinity();
+
+    static public ExtendedInt/*!*/ PlusInfinity {
+      get {
+        Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
+        return cachedPlusInf;
+      }
+    }
+
+    static public ExtendedInt/*!*/ MinusInfinity {
+      get {
+        Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
+        return cachedMinusInf;
+      }
+    }
+
+    public abstract BigNum Value {
+      get;
+    }
+
+    public abstract int Signum {
+      get;
+    }
+
+    public bool IsZero {
+      get {
+        return Signum == 0;
+      }
+    }
+
+    public bool IsPositive {
+      get {
+        return Signum > 0;
+      }
+    }
+
+    public bool IsNegative {
+      get {
+        return Signum < 0;
+      }
+    }
+
+
+    #region Below are the extensions of arithmetic operations on extended integers
+
+    // Addition
+    public static ExtendedInt/*!*/ operator +(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (a is InfinitaryInt) {
+        return a;
+      } else if (b is InfinitaryInt) {
+        return b;
+      } else {
+        return ExtendedInt.Factory(a.Value + b.Value);
+      }
+    }
+
+    // Subtraction
+    public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (a is InfinitaryInt) {
+        return a;
+      } else if (b is InfinitaryInt) {
+        return UnaryMinus(b);
+      } else {
+        return ExtendedInt.Factory(a.Value - b.Value);
+      }
+    }
+
+    // Unary minus
+    public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a) {
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      // BUGBUG: Some compiler error prevents the unary minus operator from being used
+      return UnaryMinus(a);
+    }
+
+    // Unary minus
+    public static ExtendedInt/*!*/ UnaryMinus(ExtendedInt/*!*/ a) {
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (a is PlusInfinity)
+        return cachedMinusInf;
+      if (a is MinusInfinity)
+        return cachedPlusInf;
+      else // a is a PureInteger
+        return new PureInteger(-a.Value);
+    }
+
+    // Multiplication
+    public static ExtendedInt/*!*/ operator *(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (a.IsZero) {
+        return a;
+      } else if (b.IsZero) {
+        return b;
+      } else if (a is InfinitaryInt) {
+        if (b.IsPositive) {
+          return a;
+        } else {
+          return UnaryMinus(a);
+        }
+      } else if (b is InfinitaryInt) {
+        if (a.IsPositive) {
+          return b;
+        } else {
+          return UnaryMinus(b);
+        }
+      } else {
+        return ExtendedInt.Factory(a.Value * b.Value);
+      }
+    }
+
+    // Division
+    public static ExtendedInt/*!*/ operator /(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (b.IsZero) {
+        return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
+      }
+      if (a is InfinitaryInt) {
+        return a;
+      } else if (b is InfinitaryInt) {
+        return b;
+      } else {
+        return ExtendedInt.Factory(a.Value / b.Value);
+      }
+    }
+
+    // Modulo
+    public static ExtendedInt/*!*/ operator %(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (b.IsZero) {
+        return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
+      }
+      if (a is InfinitaryInt) {
+        return a;
+      } else if (b is InfinitaryInt) {
+        return b;
+      } else {
+        return ExtendedInt.Factory(a.Value % b.Value);
+      }
+    }
+
+    #endregion
+
+    #region Inf and Sup operations
+
+    public abstract int CompareTo(ExtendedInt/*!*/ that);
+
+    public static bool operator <(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+      Contract.Requires(sup != null);
+      Contract.Requires(inf != null);
+      return inf.CompareTo(sup) < 0;
+    }
+
+    public static bool operator >(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+      Contract.Requires(sup != null);
+      Contract.Requires(inf != null);
+      return inf.CompareTo(sup) > 0;
+    }
+
+    public static bool operator <=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+      Contract.Requires(sup != null);
+      Contract.Requires(inf != null);
+      return inf.CompareTo(sup) <= 0;
+    }
+
+    public static bool operator >=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+      Contract.Requires(sup != null);
+      Contract.Requires(inf != null);
+      Contract.Requires(inf != null && sup != null);
+      return inf.CompareTo(sup) >= 0;
+    }
+
+    public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+      Contract.Requires(sup != null);
+      Contract.Requires(inf != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (inf < sup)
+        return inf;
+      else
+        return sup;
+    }
+
+    public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
+      Contract.Requires(d != null);
+      Contract.Requires(c != null);
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      ExtendedInt/*!*/ infab = Inf(a, b);
+      Contract.Assert(infab != null);
+      ExtendedInt/*!*/ infcd = Inf(c, d);
+      Contract.Assert(infcd != null);
+
+      return Inf(infab, infcd);
+    }
+
+    public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+      Contract.Requires(sup != null);
+      Contract.Requires(inf != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      if (inf > sup)
+        return inf;
+      else
+        return sup;
+    }
+
+    public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
+      Contract.Requires(d != null);
+      Contract.Requires(c != null);
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      ExtendedInt/*!*/ supab = Sup(a, b);
+      Contract.Assert(supab != null);
+      ExtendedInt/*!*/ supcd = Sup(c, d);
+      Contract.Assert(supcd != null);
+
+      return Sup(supab, supcd);
+    }
+
+    #endregion
+
+    // Return the ExtendedInt corresponding to the value
+    public static ExtendedInt/*!*/ Factory(BigNum val) {
+      Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+      return new PureInteger(val);
+    }
+  }
+  [ContractClassFor(typeof(ExtendedInt))]
+  abstract class ExtendedIntContracts : ExtendedInt {
+    public override int CompareTo(ExtendedInt that) {
+      Contract.Requires(that != null);
+      throw new NotImplementedException();
+    }
+  }
+
+  // Stands for a normal (finite) integer x
+  class PureInteger : ExtendedInt {
+    public PureInteger(BigNum i) {
+      this.val = i;
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return this.Value.ToString();
+    }
+
+    private BigNum val;
+    public override BigNum Value {
+      get {
+        return this.val;
+      }
+    }
+
+    public override int Signum {
+      get {
+        return val.Signum;
+      }
+    }
+
+    public override int CompareTo(ExtendedInt/*!*/ that) {
+      //Contract.Requires(that != null);
+      if (that is PlusInfinity)
+        return -1;
+      else if (that is PureInteger)
+        return this.Value.CompareTo(that.Value);
+      else // then that is a MinusInfinity
+        return 1;
+    }
+  }
+
+  abstract class InfinitaryInt : ExtendedInt {
+    public override BigNum Value {
+      get {
+        throw new InvalidOperationException();
+      }
+    }
+  }
+
+  class PlusInfinity : InfinitaryInt {
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return "+oo";
+    }
+
+    public override int Signum {
+      get {
+        return 1;
+      }
+    }
+
+    public override int CompareTo(ExtendedInt/*!*/ that) {
+      //Contract.Requires(that != null);
+      if (that is PlusInfinity)
+        return 0;
+      else
+        return 1;
+    }
+  }
+
+  class MinusInfinity : InfinitaryInt {
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return "-oo";
+    }
+
+    public override int Signum {
+      get {
+        return -1;
+      }
+    }
+
+    public override int CompareTo(ExtendedInt/*!*/ that) {
+      //Contract.Requires(that != null);
+      if (that is MinusInfinity)
+        return 0;
+      else
+        return -1;
+    }
+  }
+}
diff --git a/Source/AIFramework/VariableMap/MicroLattice.cs b/Source/AIFramework/VariableMap/MicroLattice.cs
index ef98f8f7..f46349b7 100644
--- a/Source/AIFramework/VariableMap/MicroLattice.cs
+++ b/Source/AIFramework/VariableMap/MicroLattice.cs
@@ -1,105 +1,105 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework
-{
-    using System.Diagnostics.Contracts;
-    using System.Collections;
-    using System.Diagnostics;
-    //using System.Compiler;
-    using Microsoft.AbstractInterpretationFramework.Collections;
-
-    /// <summary>
-    ///  Interface for a lattice that works on a per-variable basis.
-    /// </summary>
-    /// 
-  [ContractClass(typeof(MicroLatticeContracts))]
-    public abstract class MicroLattice : MathematicalLattice
-    {
-        /// <summary>
-        ///  Returns the predicate on the given variable for the given
-        ///  lattice element.
-        /// </summary>
-        public abstract IExpr/*!*/ ToPredicate(IVariable/*!*/ v, Element/*!*/ e);
-          /* requires !e.IsBottom && !e.IsTop; */
-
-        /// <summary>
-        ///  Allows the lattice to specify whether it understands a particular function symbol.
-        /// 
-        ///  The lattice is always allowed to "true" even when it really can't do anything with
-        ///  such functions; however, it is advantageous to say "false" when possible to avoid
-        ///  being called to do certain things.
-        /// 
-        ///  The arguments to a function are provided for context so that the lattice can say
-        ///  true or false for the same function symbol in different situations.  For example,
-        ///  a lattice may understand the multiplication of a variable and a constant but not
-        ///  of two variables.  The implementation of a lattice should not hold on to the
-        ///  arguments.
-        /// </summary>
-        /// <param name="f">The function symbol.</param>
-        /// <param name="args">The argument context.</param>
-        /// <returns>True if it may understand f, false if it does not understand f.</returns>
-        public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);
-
-        /// <summary>
-        /// Set this property to true if the implemented MicroLattice can handle basic arithmetic.
-        /// Stated otherwise this property is set to true if the MicroLattice provides a transfer function for a predicate in a given state
-        /// </summary>
-        public  virtual bool UnderstandsBasicArithmetics
-        {
-          get { return false; }
-        }
-
-        /// <summary>
-        ///  Evaluate the predicate e and a yield the lattice element
-        ///  that is implied by it.
-        /// </summary>
-        /// <param name="e">The predicate that is assumed to contain 1 variable.</param>
-        /// <returns>The most precise lattice element that is implied by the predicate.</returns>
-        public abstract Element/*!*/ EvaluatePredicate(IExpr/*!*/ e);
-
-        /// <summary>
-        /// Evaluate the predicate e and yield an overapproximation of the predicate under the state that is passed as a parameter
-        /// Note that unless the subclass implement it, the default behavior is to evaluate the predicate stateless, that implies that it
-        /// is evaluated in any possible context, i.e. it is an upper approximation
-        /// </summary>
-        public virtual Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ e, IFunctionalMap state){
-Contract.Requires(e != null);
-Contract.Ensures(Contract.Result<Element>() != null);
-          return EvaluatePredicate(e);
-        }
-
-        /// <summary>
-        ///  Give an expression (often a value) that can be used to substitute for
-        ///  the variable.
-        /// </summary>
-        /// <param name="e">A lattice element.</param>
-        /// <returns>The null value if no such expression can be given.</returns>
-        public abstract IExpr GetFoldExpr(Element/*!*/ e);
-    }
-    [ContractClassFor(typeof(MicroLattice))]
-    public abstract class MicroLatticeContracts : MicroLattice {
-      public override IExpr ToPredicate(IVariable v, MathematicalLattice.Element e) {
-        Contract.Requires(v != null);
-        Contract.Requires(e != null);
-        Contract.Ensures(Contract.Result<IExpr>() != null);
-        throw new System.NotImplementedException();
-      }
-      public override bool Understands(IFunctionSymbol f, IList args) {
-        Contract.Requires(f != null);
-        Contract.Requires(args != null);
-        throw new System.NotImplementedException();
-      }
-      public override Element EvaluatePredicate(IExpr e) {
-        Contract.Requires(e != null);
-        Contract.Ensures(Contract.Result<Element>() != null);
-        throw new System.NotImplementedException();
-      }
-      public override IExpr GetFoldExpr(MathematicalLattice.Element e) {
-        Contract.Requires(e != null);
-        throw new System.NotImplementedException();
-      }
-    }
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework
+{
+    using System.Diagnostics.Contracts;
+    using System.Collections;
+    using System.Diagnostics;
+    //using System.Compiler;
+    using Microsoft.AbstractInterpretationFramework.Collections;
+
+    /// <summary>
+    ///  Interface for a lattice that works on a per-variable basis.
+    /// </summary>
+    /// 
+  [ContractClass(typeof(MicroLatticeContracts))]
+    public abstract class MicroLattice : MathematicalLattice
+    {
+        /// <summary>
+        ///  Returns the predicate on the given variable for the given
+        ///  lattice element.
+        /// </summary>
+        public abstract IExpr/*!*/ ToPredicate(IVariable/*!*/ v, Element/*!*/ e);
+          /* requires !e.IsBottom && !e.IsTop; */
+
+        /// <summary>
+        ///  Allows the lattice to specify whether it understands a particular function symbol.
+        /// 
+        ///  The lattice is always allowed to "true" even when it really can't do anything with
+        ///  such functions; however, it is advantageous to say "false" when possible to avoid
+        ///  being called to do certain things.
+        /// 
+        ///  The arguments to a function are provided for context so that the lattice can say
+        ///  true or false for the same function symbol in different situations.  For example,
+        ///  a lattice may understand the multiplication of a variable and a constant but not
+        ///  of two variables.  The implementation of a lattice should not hold on to the
+        ///  arguments.
+        /// </summary>
+        /// <param name="f">The function symbol.</param>
+        /// <param name="args">The argument context.</param>
+        /// <returns>True if it may understand f, false if it does not understand f.</returns>
+        public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);
+
+        /// <summary>
+        /// Set this property to true if the implemented MicroLattice can handle basic arithmetic.
+        /// Stated otherwise this property is set to true if the MicroLattice provides a transfer function for a predicate in a given state
+        /// </summary>
+        public  virtual bool UnderstandsBasicArithmetics
+        {
+          get { return false; }
+        }
+
+        /// <summary>
+        ///  Evaluate the predicate e and a yield the lattice element
+        ///  that is implied by it.
+        /// </summary>
+        /// <param name="e">The predicate that is assumed to contain 1 variable.</param>
+        /// <returns>The most precise lattice element that is implied by the predicate.</returns>
+        public abstract Element/*!*/ EvaluatePredicate(IExpr/*!*/ e);
+
+        /// <summary>
+        /// Evaluate the predicate e and yield an overapproximation of the predicate under the state that is passed as a parameter
+        /// Note that unless the subclass implement it, the default behavior is to evaluate the predicate stateless, that implies that it
+        /// is evaluated in any possible context, i.e. it is an upper approximation
+        /// </summary>
+        public virtual Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ e, IFunctionalMap state){
+Contract.Requires(e != null);
+Contract.Ensures(Contract.Result<Element>() != null);
+          return EvaluatePredicate(e);
+        }
+
+        /// <summary>
+        ///  Give an expression (often a value) that can be used to substitute for
+        ///  the variable.
+        /// </summary>
+        /// <param name="e">A lattice element.</param>
+        /// <returns>The null value if no such expression can be given.</returns>
+        public abstract IExpr GetFoldExpr(Element/*!*/ e);
+    }
+    [ContractClassFor(typeof(MicroLattice))]
+    public abstract class MicroLatticeContracts : MicroLattice {
+      public override IExpr ToPredicate(IVariable v, MathematicalLattice.Element e) {
+        Contract.Requires(v != null);
+        Contract.Requires(e != null);
+        Contract.Ensures(Contract.Result<IExpr>() != null);
+        throw new System.NotImplementedException();
+      }
+      public override bool Understands(IFunctionSymbol f, IList args) {
+        Contract.Requires(f != null);
+        Contract.Requires(args != null);
+        throw new System.NotImplementedException();
+      }
+      public override Element EvaluatePredicate(IExpr e) {
+        Contract.Requires(e != null);
+        Contract.Ensures(Contract.Result<Element>() != null);
+        throw new System.NotImplementedException();
+      }
+      public override IExpr GetFoldExpr(MathematicalLattice.Element e) {
+        Contract.Requires(e != null);
+        throw new System.NotImplementedException();
+      }
+    }
 }
 \ No newline at end of file
diff --git a/Source/AIFramework/VariableMap/Nullness.cs b/Source/AIFramework/VariableMap/Nullness.cs
index 613f55e0..474792e0 100644
--- a/Source/AIFramework/VariableMap/Nullness.cs
+++ b/Source/AIFramework/VariableMap/Nullness.cs
@@ -1,260 +1,260 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Collections;
-  using System.Diagnostics;
-  //using System.Compiler.Analysis;
-
-  public class NullnessLattice : MicroLattice {
-    readonly INullnessFactory/*!*/ factory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(factory != null);
-    }
-
-
-    public NullnessLattice(INullnessFactory/*!*/ factory) {
-      Contract.Requires(factory != null);
-      this.factory = factory;
-      // base();
-    }
-
-    enum Value {
-      Bottom,
-      NotNull,
-      Null,
-      MayBeNull
-    }
-
-    private class Elt : Element {
-      public Value value;
-
-      public Elt(Value v) {
-        this.value = v;
-      }
-
-      [Pure]
-      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
-      }
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(this.value);
-      }
-    }
-
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.MayBeNull);
-      }
-    }
-
-    public override Element/*!*/ Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.Bottom);
-      }
-    }
-
-    public static Element/*!*/ Null {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.Null);
-      }
-    }
-
-    public static Element/*!*/ NotNull {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.NotNull);
-      }
-    }
-
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.value == Value.MayBeNull;
-    }
-
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.value == Value.Bottom;
-    }
-
-    public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return (a.value == b.value) ? a : (Elt)Top;
-    }
-
-    public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return (a.value == b.value) ? a : (Elt)Bottom;
-    }
-
-    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      return Join(first, second);
-    }
-
-    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
-    {
-      //Contract.Requires(first != null);
-      //Contract.Requires(second != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return a.value == b.value;
-    }
-
-    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      //Contract.Requires(var != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      Elt e = (Elt)element;
-
-      if (e.value == Value.NotNull) {
-        return factory.Neq(var, factory.Null);
-      }
-      if (e.value == Value.Null) {
-        return factory.Eq(var, factory.Null);
-      }
-      {
-        Contract.Assert(false);
-        throw new cce.UnreachableException();
-      }
-      throw new System.Exception();
-    }
-
-    public override IExpr GetFoldExpr(Element/*!*/ e) {
-      //Contract.Requires(e != null);
-      Elt elt = (Elt)e;
-      if (elt.value == Value.Null) {
-        return factory.Null;
-      } else {
-        // can't fold into an expression
-        return null;
-      }
-    }
-
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
-          f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
-
-        Contract.Assert(args.Count == 2);
-        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-        // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
-        if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
-          return true;
-        } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
-          return true;
-        }
-      }
-      return false;
-    }
-
-    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      IFunApp nary = e as IFunApp;
-      if (nary != null) {
-        bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
-        if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
-          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
-          Contract.Assert(args != null);
-          Contract.Assert(args.Count == 2);
-          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-          // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
-          IVariable var = null;
-          if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
-            var = (IVariable)arg0;
-          } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
-            var = (IVariable)arg1;
-          }
-
-          if (var != null) // found the pattern
-                    {
-            return isEq ? Null : NotNull;
-          }
-        }
-      }
-      return Top;
-    }
-  }
-
-#if false
-
-    public class NullnessMicroLattice : MicroLattice 
-    {
-        public override MicroLatticeElement Top { get { return NullnessLatticeElement.Top; } }
-        public override MicroLatticeElement Bottom { get { return NullnessLatticeElement.Bottom; } }
-
-
-        public override MicroLatticeElement EvaluateExpression (Expr e, LookupValue lookup)
-        {
-            if (e is LiteralExpr && ((LiteralExpr)e).Val == null)
-            {
-                return NullnessLatticeElement.Null;
-            }
-            return Top;
-        }
-
-
-        public override MicroLatticeElement EvaluatePredicate (Expr e, LookupValue lookup)
-        {
-            NAryExpr nary = e as NAryExpr;
-            if (nary != null && 
-                    (nary.Fun.FunctionName.Equals("==") || nary.Fun.FunctionName.Equals("!=")))
-            {
-                Debug.Assert(nary.Args.Length == 2);
-
-                Expr arg0 = nary.Args[0], arg1 = nary.Args[1];
-                Variable var = null;
-
-                // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
-                if (arg0 is IdentifierExpr && arg1 is LiteralExpr && ((LiteralExpr)arg1).Val == null)
-                {
-                    var = ((IdentifierExpr)arg0).Decl;
-                }
-                else if (arg1 is IdentifierExpr && arg0 is LiteralExpr && ((LiteralExpr)arg0).Val == null)
-                {
-                    var = ((IdentifierExpr)arg1).Decl;
-                }
-
-                if (var != null) // found the pattern
-                {
-                    return nary.Fun.FunctionName.Equals("==") ? 
-                        NullnessLatticeElement.Null : 
-                        NullnessLatticeElement.NotNull;
-                }
-            }
-            return Top;
-        }
-    }
-
-#endif
-
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Diagnostics.Contracts;
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Collections;
+  using System.Diagnostics;
+  //using System.Compiler.Analysis;
+
+  public class NullnessLattice : MicroLattice {
+    readonly INullnessFactory/*!*/ factory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(factory != null);
+    }
+
+
+    public NullnessLattice(INullnessFactory/*!*/ factory) {
+      Contract.Requires(factory != null);
+      this.factory = factory;
+      // base();
+    }
+
+    enum Value {
+      Bottom,
+      NotNull,
+      Null,
+      MayBeNull
+    }
+
+    private class Elt : Element {
+      public Value value;
+
+      public Elt(Value v) {
+        this.value = v;
+      }
+
+      [Pure]
+      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+      }
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(this.value);
+      }
+    }
+
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.MayBeNull);
+      }
+    }
+
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.Bottom);
+      }
+    }
+
+    public static Element/*!*/ Null {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.Null);
+      }
+    }
+
+    public static Element/*!*/ NotNull {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.NotNull);
+      }
+    }
+
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.value == Value.MayBeNull;
+    }
+
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.value == Value.Bottom;
+    }
+
+    public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return (a.value == b.value) ? a : (Elt)Top;
+    }
+
+    public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return (a.value == b.value) ? a : (Elt)Bottom;
+    }
+
+    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return Join(first, second);
+    }
+
+    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+    {
+      //Contract.Requires(first != null);
+      //Contract.Requires(second != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return a.value == b.value;
+    }
+
+    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      //Contract.Requires(var != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      Elt e = (Elt)element;
+
+      if (e.value == Value.NotNull) {
+        return factory.Neq(var, factory.Null);
+      }
+      if (e.value == Value.Null) {
+        return factory.Eq(var, factory.Null);
+      }
+      {
+        Contract.Assert(false);
+        throw new cce.UnreachableException();
+      }
+      throw new System.Exception();
+    }
+
+    public override IExpr GetFoldExpr(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      Elt elt = (Elt)e;
+      if (elt.value == Value.Null) {
+        return factory.Null;
+      } else {
+        // can't fold into an expression
+        return null;
+      }
+    }
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
+          f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+
+        Contract.Assert(args.Count == 2);
+        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+        // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+        if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
+          return true;
+        } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+          return true;
+        }
+      }
+      return false;
+    }
+
+    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      IFunApp nary = e as IFunApp;
+      if (nary != null) {
+        bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+        if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+          Contract.Assert(args != null);
+          Contract.Assert(args.Count == 2);
+          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+          // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+          IVariable var = null;
+          if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
+            var = (IVariable)arg0;
+          } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+            var = (IVariable)arg1;
+          }
+
+          if (var != null) // found the pattern
+                    {
+            return isEq ? Null : NotNull;
+          }
+        }
+      }
+      return Top;
+    }
+  }
+
+#if false
+
+    public class NullnessMicroLattice : MicroLattice 
+    {
+        public override MicroLatticeElement Top { get { return NullnessLatticeElement.Top; } }
+        public override MicroLatticeElement Bottom { get { return NullnessLatticeElement.Bottom; } }
+
+
+        public override MicroLatticeElement EvaluateExpression (Expr e, LookupValue lookup)
+        {
+            if (e is LiteralExpr && ((LiteralExpr)e).Val == null)
+            {
+                return NullnessLatticeElement.Null;
+            }
+            return Top;
+        }
+
+
+        public override MicroLatticeElement EvaluatePredicate (Expr e, LookupValue lookup)
+        {
+            NAryExpr nary = e as NAryExpr;
+            if (nary != null && 
+                    (nary.Fun.FunctionName.Equals("==") || nary.Fun.FunctionName.Equals("!=")))
+            {
+                Debug.Assert(nary.Args.Length == 2);
+
+                Expr arg0 = nary.Args[0], arg1 = nary.Args[1];
+                Variable var = null;
+
+                // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+                if (arg0 is IdentifierExpr && arg1 is LiteralExpr && ((LiteralExpr)arg1).Val == null)
+                {
+                    var = ((IdentifierExpr)arg0).Decl;
+                }
+                else if (arg1 is IdentifierExpr && arg0 is LiteralExpr && ((LiteralExpr)arg0).Val == null)
+                {
+                    var = ((IdentifierExpr)arg1).Decl;
+                }
+
+                if (var != null) // found the pattern
+                {
+                    return nary.Fun.FunctionName.Equals("==") ? 
+                        NullnessLatticeElement.Null : 
+                        NullnessLatticeElement.NotNull;
+                }
+            }
+            return Top;
+        }
+    }
+
+#endif
+
+}
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs
index 172cef01..752d3f01 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.cs
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs
@@ -1,854 +1,854 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Diagnostics.Contracts;
-  using System.Collections;
-  using System.Collections.Generic;
-  using System.Diagnostics;
-
-  using Microsoft.AbstractInterpretationFramework;
-  using Microsoft.AbstractInterpretationFramework.Collections;
-
-  using Microsoft.Boogie;
-
-  using IMutableSet = Microsoft.Boogie.GSet<object>;
-  using ISet = Microsoft.Boogie.GSet<object>;
-  using Set = Microsoft.Boogie.GSet<object>;
-  using HashSet = Microsoft.Boogie.GSet<object>;
-
-  /// <summary>
-  ///  Creates a lattice that works for several variables given a MicroLattice.  Assumes
-  ///  if one variable is bottom, then all variables are bottom.
-  /// </summary>
-  public class VariableMapLattice : Lattice {
-    private class Elt : Element {
-      /// <summary>
-      /// IsBottom(e)  iff  e.constraints == null
-      /// </summary>
-      /*MayBeNull*/
-      private IFunctionalMap constraints;  // of type IVariable -> LATTICE_ELEMENT
-      public IFunctionalMap Constraints {
-        get {
-          return this.constraints;
-        }
-      }
-
-      private Elt(bool top) {
-        if (top) {
-          this.constraints = FunctionalHashtable.Empty;
-        } else {
-          this.constraints = null;
-        }
-      }
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(this.constraints);
-      }
-
-      [Pure]
-      public override string/*!*/ ToString() {
-        Contract.Ensures(Contract.Result<string>() != null);
-        if (constraints == null) {
-          return "<bottom>";
-        }
-        string s = "[";
-        string sep = "";
-        foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) {
-          Contract.Assert(v != null);
-          Element m = (Element)constraints[v];
-          s += sep + v.Name + " -> " + m;
-          sep = ", ";
-        }
-        return s + "]";
-      }
-
-      public static readonly Elt/*!*/ Top = new Elt(true);
-      public static readonly Elt/*!*/ Bottom = new Elt(false);
-
-
-      public Elt(IFunctionalMap constraints) {
-        this.constraints = constraints;
-      }
-
-      public bool IsBottom {
-        get {
-          return this.constraints == null;
-        }
-      }
-
-      public int Count {
-        get {
-          return this.constraints == null ? 0 : this.constraints.Count;
-        }
-      }
-
-      public IEnumerable/*<IVariable>*//*!*/ Variables {
-        get {
-          Contract.Requires(!this.IsBottom);
-          Contract.Ensures(Contract.Result<IEnumerable>() != null);
-          Contract.Assume(this.constraints != null);
-          return cce.NonNull(this.constraints.Keys);
-        }
-      }
-
-      public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
-        Contract.Ensures(Contract.Result<IEnumerable>() != null);
-        if (variableComparer == null) {
-          return Variables;
-        } else {
-          ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
-          foreach (IVariable variable in Variables) {
-            vars.Add(variable);
-          }
-          vars.Sort(variableComparer);
-          return vars;
-        }
-      }
-
-      public Element Lookup(IVariable v) {
-        if ((v == null) || (this.constraints == null)) {
-          return null;
-        }
-        return (Element)this.constraints[v];
-      }
-
-      public Element this[IVariable/*!*/ key] {
-        get {
-          Contract.Requires(!this.IsBottom);
-          Contract.Requires(key != null);
-          Contract.Assume(this.constraints != null);
-          return (Element)constraints[key];
-        }
-      }
-
-      /// <summary>
-      /// Add a new entry in the functional map: var --> value.
-      /// If the variable is already there, throws an exception
-      /// </summary>
-      public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
-        Contract.Requires(microLattice != null);
-        Contract.Requires(value != null);
-        Contract.Requires(var != null);
-        Contract.Requires((!this.IsBottom));
-        Contract.Ensures(Contract.Result<Elt>() != null);
-        Contract.Assume(this.constraints != null);
-        Contract.Assert(!this.constraints.Contains(var));
-
-        if (microLattice.IsBottom(value)) {
-          return Bottom;
-        }
-        if (microLattice.IsTop(value)) {
-          return this.Remove(var, microLattice);
-        }
-
-        return new Elt(this.constraints.Add(var, value));
-      }
-
-      /// <summary>
-      /// Set the value of the variable in the functional map
-      /// If the variable is not already there, throws an exception
-      /// </summary>
-      public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
-        Contract.Requires(microLattice != null);
-        Contract.Requires(value != null);
-        Contract.Requires(var != null);
-        Contract.Ensures(Contract.Result<Elt>() != null);
-        if (microLattice.IsBottom(value)) {
-          return Bottom;
-        }
-        if (microLattice.IsTop(value)) {
-          return this.Remove(var, microLattice);
-        }
-
-        Contract.Assume(this.constraints != null);
-        Contract.Assert(this.constraints.Contains(var));
-
-        // this.constraints[var] = value;
-        IFunctionalMap newMap = this.constraints.Set(var, value);
-
-        return new Elt(newMap);
-      }
-
-      public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice) {
-        Contract.Requires(var != null);
-        Contract.Ensures(Contract.Result<Elt>() != null);
-        if (this.IsBottom) {
-          return this;
-        }
-        Contract.Assume(this.constraints != null);
-        return new Elt(this.constraints.Remove(var));
-      }
-
-      public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) {
-        Contract.Requires(microLattice != null);
-        Contract.Requires(newName != null);
-        Contract.Requires(oldName != null);
-        Contract.Requires((!this.IsBottom));
-        Contract.Ensures(Contract.Result<Elt>() != null);
-        Element value = this[oldName];
-        if (value == null) {
-          return this;
-        } // 'oldName' isn't in the map, so neither will be 'newName'
-        Contract.Assume(this.constraints != null);
-        IFunctionalMap newMap = this.constraints.Remove(oldName);
-        newMap = newMap.Add(newName, value);
-        return new Elt(newMap);
-      }
-
-      [Pure]
-      public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
-        throw new System.NotImplementedException();
-      }
-
-    } // class
-
-    private readonly MicroLattice/*!*/ microLattice;
-
-    private readonly IPropExprFactory/*!*/ propExprFactory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(microLattice != null);
-      Contract.Invariant(propExprFactory != null);
-    }
-
-
-    private readonly /*maybe null*/IComparer variableComparer;
-
-    public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
-      : base(valueExprFactory) {
-      Contract.Requires(microLattice != null);
-      Contract.Requires(valueExprFactory != null);
-      Contract.Requires(propExprFactory != null);
-      this.propExprFactory = propExprFactory;
-      this.microLattice = microLattice;
-      this.variableComparer = variableComparer;
-      // base(valueExprFactory);
-    }
-
-    protected override object/*!*/ UniqueId {
-      get {
-        Contract.Ensures(Contract.Result<object>() != null);
-        return this.microLattice.GetType();
-      }
-    }
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return Elt.Top;
-      }
-    }
-
-    public override Element Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return Elt.Bottom;
-      }
-    }
-
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return !e.IsBottom && e.Count == 0;
-    }
-
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      return ((Elt)element).IsBottom;
-    }
-
-    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-
-      // return true iff every constraint in "this" is no weaker than the corresponding
-      // constraint in "that" and there are no additional constraints in "that"
-      foreach (IVariable/*!*/ var in a.Variables) {
-        Contract.Assert(var != null);
-        Element thisValue = cce.NonNull(a[var]);
-
-        Element thatValue = b[var];
-        if (thatValue == null) {
-          continue;
-        } // it's okay for "a" to know something "b" doesn't
-
-        if (this.microLattice.LowerThan(thisValue, thatValue)) {
-          continue;
-        } // constraint for "var" satisfies AtMost relation
-
-        return false;
-      }
-      foreach (IVariable/*!*/ var in b.Variables) {
-        Contract.Assert(var != null);
-        if (a.Lookup(var) != null) {
-          continue;
-        } // we checked this case in the loop above
-
-        Element thatValue = cce.NonNull(b[var]);
-        if (this.microLattice.IsTop(thatValue)) {
-          continue;
-        } // this is a trivial constraint
-
-        return false;
-      }
-      return true;
-    }
-
-    private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
-      Contract.Requires((newValue != null));
-      Contract.Requires((var != null));
-      Contract.Requires((element != null));
-      Contract.Ensures(Contract.Result<Elt>() != null);
-      Elt e = (Elt)element;
-
-      if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
-            {
-        /*MicroLattice*/
-        Element currentValue = e[var];
-
-        if (currentValue == null) {
-          // No information currently, so we just add the new info.
-          return e.Add(var, newValue, this.microLattice);
-        } else {
-          // Otherwise, take the meet of the new and current info.
-          //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
-          return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
-        }
-      }
-      return e;
-    }
-
-    public override string/*!*/ ToString(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Contract.Ensures(Contract.Result<string>() != null);
-      Elt e = (Elt)element;
-
-      if (IsTop(e)) {
-        return "<top>";
-      }
-      if (IsBottom(e)) {
-        return "<bottom>";
-      }
-
-      int k = 0;
-      System.Text.StringBuilder buffer = new System.Text.StringBuilder();
-      foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) {
-        Contract.Assert(key != null);
-        if (k++ > 0) {
-          buffer.Append("; ");
-        }
-        buffer.AppendFormat("{0} = {1}", key, e[key]);
-      }
-      return buffer.ToString();
-    }
-
-    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-
-      IFunctionalMap newMap = FunctionalHashtable.Empty;
-      foreach (IVariable/*!*/ key in a.Variables) {
-        Contract.Assert(key != null);
-        Element aValue = a[key];
-        Element bValue = b[key];
-
-        if (aValue != null && bValue != null) {
-          // Keep only the variables known to both elements.
-          Element newValue = this.microLattice.Join(aValue, bValue);
-          newMap = newMap.Add(key, newValue);
-        }
-      }
-      Elt/*!*/ join = new Elt(newMap);
-      Contract.Assert(join != null);
-
-      // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
-
-      return join;
-    }
-
-    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-
-      IFunctionalMap newMap = FunctionalHashtable.Empty;
-      foreach (IVariable/*!*/ key in a.Variables) {
-        Contract.Assert(key != null);
-        Element/*!*/ aValue = cce.NonNull(a[key]);
-        Element bValue = b[key];
-
-        Element newValue =
-          bValue == null ? aValue :
-          this.microLattice.Meet(aValue, bValue);
-
-        newMap = newMap.Add(key, newValue);
-      }
-      foreach (IVariable/*!*/ key in b.Variables) {
-        Contract.Assert(key != null);
-        Element aValue = a[key];
-        Element bValue = b[key];
-        Debug.Assert(bValue != null);
-
-        if (aValue == null) {
-          // It's a variable we didn't cover in the last loop.
-          newMap = newMap.Add(key, bValue);
-        }
-      }
-      return new Elt(newMap);
-    }
-
-    /// <summary>
-    /// Perform the pointwise widening of the elements in the map
-    /// </summary>
-    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires((second != null));
-      //Contract.Requires((first != null));
-      Contract.Ensures(Contract.Result<Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-
-      // Note we have to add those cases as we do not have a "NonTrivialWiden" method
-      if (a.IsBottom)
-        return new Elt(b.Constraints);
-      if (b.IsBottom)
-        return new Elt(a.Constraints);
-
-      IFunctionalMap newMap = FunctionalHashtable.Empty;
-      foreach (IVariable/*!*/ key in a.Variables) {
-        Contract.Assert(key != null);
-        Element aValue = a[key];
-        Element bValue = b[key];
-
-        if (aValue != null && bValue != null) {
-          // Keep only the variables known to both elements.
-          Element newValue = this.microLattice.Widen(aValue, bValue);
-          newMap = newMap.Add(key, newValue);
-        }
-      }
-      Element/*!*/ widen = new Elt(newMap);
-      Contract.Assert(widen != null);
-      // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
-
-      return widen;
-    }
-
-    internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars) {
-      Contract.Requires(ignoreVars != null);
-      Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<ISet>() != null);
-      HashSet s = new HashSet();
-
-      IFunApp f = e as IFunApp;
-      IFunction lambda = e as IFunction;
-
-      if (e is IVariable) {
-        if (!ignoreVars.Contains(e))
-          s.Add(e);
-      } else if (f != null) // e is IFunApp
-            {
-        foreach (IExpr/*!*/ arg in f.Arguments) {
-          Contract.Assert(arg != null);
-          s.AddAll(VariablesInExpression(arg, ignoreVars));
-        }
-      } else if (lambda != null) {
-        IMutableSet x = new HashSet(1);
-        x.Add(lambda.Param);
-
-        // Ignore the bound variable
-        s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
-      } else if (e is IUnknown) {
-        // skip (actually, it would be appropriate to return the universal set of all variables)
-      } else {
-        Debug.Assert(false, "case not handled: " + e);
-      }
-      return s;
-    }
-
-
-    private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e) {
-      Contract.Ensures(Contract.Result<ArrayList>() != null);
-      ArrayList result = new ArrayList();
-
-      IFunApp f = e as IFunApp;
-      if (f != null) {
-        if (f.FunctionSymbol.Equals(Prop.And)) {
-          foreach (IExpr arg in f.Arguments) {
-            result.AddRange(FindConjuncts(arg));
-          }
-        } else if (f.FunctionSymbol.Equals(Prop.Or)
-                 || f.FunctionSymbol.Equals(Prop.Implies)) {
-          // Do nothing.
-        } else {
-          result.Add(e);
-        }
-      } else {
-        result.Add(e);
-      }
-
-      return result;
-    }
-
-    private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right) {
-      Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
-      left = null;
-      right = null;
-
-      // See if we have an equality
-      IFunApp nary = expr as IFunApp;
-      if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) {
-        return false;
-      }
-
-      // See if it is an equality of two variables
-      IVariable idLeft = nary.Arguments[0] as IVariable;
-      IVariable idRight = nary.Arguments[1] as IVariable;
-      if (idLeft == null || idRight == null) {
-        return false;
-      }
-
-      left = idLeft;
-      right = idRight;
-      return true;
-    }
-
-    /// <summary>
-    /// Returns true iff the expression is in the form var == arithmeticExpr
-    /// </summary>
-    private static bool IsArithmeticExpr(IExpr/*!*/ expr) {
-      Contract.Requires(expr != null);
-      // System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
-
-      if (expr is IVariable)   // expr is a variable
-        return true;
-      else if (expr is IFunApp)     // may be ==, +, -, /, % or an integer
-        {
-        IFunApp fun = (IFunApp)expr;
-
-        if (fun.FunctionSymbol is IntSymbol)     // it is an integer
-          return true;
-        else if (fun.FunctionSymbol.Equals(Int.Negate))  // it is an unary minus
-          return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
-        else if (fun.Arguments.Count != 2)       // A function of two or more operands is not arithmetic
-          return false;
-        else {
-          IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
-          IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-
-          if (!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable
-            return false;
-
-          if (fun.FunctionSymbol.Equals(Value.Eq)
-              || fun.FunctionSymbol.Equals(Int.Add)
-              || fun.FunctionSymbol.Equals(Int.Sub)
-              || fun.FunctionSymbol.Equals(Int.Mul)
-              || fun.FunctionSymbol.Equals(Int.Div)
-              || fun.FunctionSymbol.Equals(Int.Mod))
-            return IsArithmeticExpr(left) && IsArithmeticExpr(right);
-          else
-            return false;
-        }
-      } else {
-        return false;
-      }
-    }
-
-    public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      if (IsTop(element)) {
-        return propExprFactory.True;
-      }
-      if (IsBottom(element)) {
-        return propExprFactory.False;
-      }
-
-      Elt e = (Elt)element;
-      IExpr truth = propExprFactory.True;
-      IExpr result = truth;
-
-      foreach (IVariable/*!*/ variable in e.SortedVariables(variableComparer)) {
-        Contract.Assert(variable != null);
-        Element value = (Element)e[variable];
-
-        if (value == null || this.microLattice.IsTop(value)) {
-          continue;
-        } // Skip variables about which we know nothing.
-        if (this.microLattice.IsBottom(value)) {
-          return propExprFactory.False;
-        }
-
-        IExpr conjunct = this.microLattice.ToPredicate(variable, value);
-
-        result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
-      }
-      return result;
-    }
-
-
-    public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
-      //Contract.Requires(variable != null);
-      //Contract.Requires(element != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
-    }
-
-    private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
-    private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) {
-      //Contract.Requires(var != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      return var;
-    }
-
-    /// <summary>
-    /// Return a new expression in which each variable has been 
-    /// replaced by an expression representing what is known about
-    /// that variable.
-    /// </summary>
-    private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
-        OnUnableToInline/*!*/ unableToInline) {
-      Contract.Requires(unableToInline != null);
-      Contract.Requires(notInlineable != null);
-      Contract.Requires(expr != null);
-      Contract.Requires(element != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      IVariable var = expr as IVariable;
-      if (var != null) {
-        /*MicroLattice*/
-        Element value = element[var];
-        if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value)) {
-          return unableToInline(var); // We don't know anything about this variable.
-        } else {
-          // GetFoldExpr returns null when it can yield an expression that
-          // can be substituted for the variable.
-          IExpr valueExpr = this.microLattice.GetFoldExpr(value);
-          return (valueExpr == null) ? var : valueExpr;
-        }
-      }
-
-      // else
-
-      IFunApp fun = expr as IFunApp;
-      if (fun != null) {
-        IList newargs = new ArrayList();
-        foreach (IExpr/*!*/ arg in fun.Arguments) {
-          Contract.Assert(arg != null);
-          newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
-        }
-        return fun.CloneWithArguments(newargs);
-      }
-
-      // else
-
-      IFunction lambda = expr as IFunction;
-      if (lambda != null) {
-        IMutableSet x = new HashSet(1);
-        x.Add(lambda.Param);
-
-        // Don't inline the bound variable
-        return lambda.CloneWithBody(
-                   InlineVariables(element, lambda.Body,
-                                    cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
-               );
-      }
-
-      // else
-
-      if (expr is IUnknown) {
-        return expr;
-      } else {
-        throw
-          new System.NotImplementedException("cannot inline identifies in expression " + expr);
-      }
-    }
-
-
-    public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
-      //Contract.Requires(expr != null);
-      //Contract.Requires(element != null);
-      //Contract.Ensures(Contract.Result<Element>() != null);
-      Elt/*!*/ result = (Elt)element;
-      Contract.Assert(result != null);
-
-      if (IsBottom(element)) {
-        return result; // == element 
-      }
-
-      expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
-
-      foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) {
-        Contract.Assert(conjunct != null);
-        IVariable left, right;
-
-        if (IsSimpleEquality(conjunct, out left, out right)) {
-          #region The conjunct is a simple equality
-
-
-          Contract.Assert(left != null && right != null);
-
-          Element leftValue = result[left], rightValue = result[right];
-          if (leftValue == null) {
-            leftValue = this.microLattice.Top;
-          }
-          if (rightValue == null) {
-            rightValue = this.microLattice.Top;
-          }
-          Element newValue = this.microLattice.Meet(leftValue, rightValue);
-          result = AddConstraint(result, left, newValue);
-          result = AddConstraint(result, right, newValue);
-
-          #endregion
-        } else {
-          ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
-
-          if (variablesInvolved.Count == 1) {
-            #region We have just one variable
-
-            IVariable var = null;
-            foreach (IVariable/*!*/ v in variablesInvolved) {
-              Contract.Assert(v != null);
-              var = v;
-            } // why is there no better way to get the elements?
-            Contract.Assert(var != null);
-            Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
-            result = AddConstraint(result, var, value);
-
-            #endregion
-          } else if (IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics) {
-            #region We evalaute an arithmetic expression
-
-            IFunApp fun = (IFunApp)conjunct;
-            if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
-                       {
-              // get the variable to be assigned
-              IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
-              IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-              IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
-
-              Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
-              Contract.Assert(value != null);
-              result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
-            }
-            #endregion
-          }
-        }
-      }
-      return result;
-    }
-
-
-    public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
-      //Contract.Requires(newName != null);
-      //Contract.Requires(oldName != null);
-      //Contract.Requires(element != null);
-      //Contract.Ensures(Contract.Result<Element>() != null);
-      if (IsBottom(element)) {
-        return element;
-      } else {
-        return ((Elt)element).Rename(oldName, newName, this.microLattice);
-      }
-    }
-
-
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      return f.Equals(Prop.And) ||
-             f.Equals(Value.Eq) ||
-             microLattice.Understands(f, args);
-    }
-
-    private sealed class EquivalentExprException : CheckedException {
-    }
-    private sealed class EquivalentExprInlineCallback {
-      private readonly IVariable/*!*/ var;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-        Contract.Invariant(var != null);
-      }
-
-      public EquivalentExprInlineCallback(IVariable/*!*/ var) {
-        Contract.Requires(var != null);
-        this.var = var;
-        // base();
-      }
-
-      public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
-        //throws EquivalentExprException;
-      {
-        Contract.Requires(othervar != null);
-        Contract.Ensures(Contract.Result<IExpr>() != null);
-        Contract.EnsuresOnThrow<EquivalentExprException>(true);
-        if (othervar.Equals(var))
-          throw new EquivalentExprException();
-        else
-          return othervar;
-      }
-    }
-
-    public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
-      //Contract.Requires(prohibitedVars != null);
-      //Contract.Requires(var != null);
-      //Contract.Requires(expr != null);
-      //Contract.Requires(q != null);
-      //Contract.Requires(e != null);
-      try {
-        EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
-        return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
-                               new OnUnableToInline(closure.ThrowOnUnableToInline));
-      } catch (EquivalentExprException) {
-        return null;
-      }
-    }
-
-
-    /// <summary>
-    /// Check to see if the given predicate holds in the given lattice element.
-    /// 
-    /// TODO:  We leave this unimplemented for now and just return maybe.
-    /// </summary>
-    /// <param name="e">The lattice element.</param>
-    /// <param name="pred">The predicate.</param>
-    /// <returns>Yes, No, or Maybe</returns>
-    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
-      //Contract.Requires(pred != null);
-      //Contract.Requires(e != null);
-      return Answer.Maybe;
-    }
-
-    /// <summary>
-    ///  Answers a disequality about two variables.  The same information could be obtained
-    ///  by asking CheckPredicate, but a different implementation may be simpler and more
-    ///  efficient.
-    /// 
-    ///  TODO: We leave this unimplemented for now and just return maybe.
-    /// </summary>
-    /// <param name="e">The lattice element.</param>
-    /// <param name="var1">The first variable.</param>
-    /// <param name="var2">The second variable.</param>
-    /// <returns>Yes, No, or Maybe.</returns>
-    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
-      //Contract.Requires(var2 != null);
-      //Contract.Requires(var1 != null);
-      //Contract.Requires(e != null);
-      return Answer.Maybe;
-    }
-
-    public override void Validate() {
-      base.Validate();
-      microLattice.Validate();
-    }
-
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Diagnostics.Contracts;
+  using System.Collections;
+  using System.Collections.Generic;
+  using System.Diagnostics;
+
+  using Microsoft.AbstractInterpretationFramework;
+  using Microsoft.AbstractInterpretationFramework.Collections;
+
+  using Microsoft.Boogie;
+
+  using IMutableSet = Microsoft.Boogie.GSet<object>;
+  using ISet = Microsoft.Boogie.GSet<object>;
+  using Set = Microsoft.Boogie.GSet<object>;
+  using HashSet = Microsoft.Boogie.GSet<object>;
+
+  /// <summary>
+  ///  Creates a lattice that works for several variables given a MicroLattice.  Assumes
+  ///  if one variable is bottom, then all variables are bottom.
+  /// </summary>
+  public class VariableMapLattice : Lattice {
+    private class Elt : Element {
+      /// <summary>
+      /// IsBottom(e)  iff  e.constraints == null
+      /// </summary>
+      /*MayBeNull*/
+      private IFunctionalMap constraints;  // of type IVariable -> LATTICE_ELEMENT
+      public IFunctionalMap Constraints {
+        get {
+          return this.constraints;
+        }
+      }
+
+      private Elt(bool top) {
+        if (top) {
+          this.constraints = FunctionalHashtable.Empty;
+        } else {
+          this.constraints = null;
+        }
+      }
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(this.constraints);
+      }
+
+      [Pure]
+      public override string/*!*/ ToString() {
+        Contract.Ensures(Contract.Result<string>() != null);
+        if (constraints == null) {
+          return "<bottom>";
+        }
+        string s = "[";
+        string sep = "";
+        foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) {
+          Contract.Assert(v != null);
+          Element m = (Element)constraints[v];
+          s += sep + v.Name + " -> " + m;
+          sep = ", ";
+        }
+        return s + "]";
+      }
+
+      public static readonly Elt/*!*/ Top = new Elt(true);
+      public static readonly Elt/*!*/ Bottom = new Elt(false);
+
+
+      public Elt(IFunctionalMap constraints) {
+        this.constraints = constraints;
+      }
+
+      public bool IsBottom {
+        get {
+          return this.constraints == null;
+        }
+      }
+
+      public int Count {
+        get {
+          return this.constraints == null ? 0 : this.constraints.Count;
+        }
+      }
+
+      public IEnumerable/*<IVariable>*//*!*/ Variables {
+        get {
+          Contract.Requires(!this.IsBottom);
+          Contract.Ensures(Contract.Result<IEnumerable>() != null);
+          Contract.Assume(this.constraints != null);
+          return cce.NonNull(this.constraints.Keys);
+        }
+      }
+
+      public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
+        Contract.Ensures(Contract.Result<IEnumerable>() != null);
+        if (variableComparer == null) {
+          return Variables;
+        } else {
+          ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
+          foreach (IVariable variable in Variables) {
+            vars.Add(variable);
+          }
+          vars.Sort(variableComparer);
+          return vars;
+        }
+      }
+
+      public Element Lookup(IVariable v) {
+        if ((v == null) || (this.constraints == null)) {
+          return null;
+        }
+        return (Element)this.constraints[v];
+      }
+
+      public Element this[IVariable/*!*/ key] {
+        get {
+          Contract.Requires(!this.IsBottom);
+          Contract.Requires(key != null);
+          Contract.Assume(this.constraints != null);
+          return (Element)constraints[key];
+        }
+      }
+
+      /// <summary>
+      /// Add a new entry in the functional map: var --> value.
+      /// If the variable is already there, throws an exception
+      /// </summary>
+      public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
+        Contract.Requires(microLattice != null);
+        Contract.Requires(value != null);
+        Contract.Requires(var != null);
+        Contract.Requires((!this.IsBottom));
+        Contract.Ensures(Contract.Result<Elt>() != null);
+        Contract.Assume(this.constraints != null);
+        Contract.Assert(!this.constraints.Contains(var));
+
+        if (microLattice.IsBottom(value)) {
+          return Bottom;
+        }
+        if (microLattice.IsTop(value)) {
+          return this.Remove(var, microLattice);
+        }
+
+        return new Elt(this.constraints.Add(var, value));
+      }
+
+      /// <summary>
+      /// Set the value of the variable in the functional map
+      /// If the variable is not already there, throws an exception
+      /// </summary>
+      public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
+        Contract.Requires(microLattice != null);
+        Contract.Requires(value != null);
+        Contract.Requires(var != null);
+        Contract.Ensures(Contract.Result<Elt>() != null);
+        if (microLattice.IsBottom(value)) {
+          return Bottom;
+        }
+        if (microLattice.IsTop(value)) {
+          return this.Remove(var, microLattice);
+        }
+
+        Contract.Assume(this.constraints != null);
+        Contract.Assert(this.constraints.Contains(var));
+
+        // this.constraints[var] = value;
+        IFunctionalMap newMap = this.constraints.Set(var, value);
+
+        return new Elt(newMap);
+      }
+
+      public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice) {
+        Contract.Requires(var != null);
+        Contract.Ensures(Contract.Result<Elt>() != null);
+        if (this.IsBottom) {
+          return this;
+        }
+        Contract.Assume(this.constraints != null);
+        return new Elt(this.constraints.Remove(var));
+      }
+
+      public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) {
+        Contract.Requires(microLattice != null);
+        Contract.Requires(newName != null);
+        Contract.Requires(oldName != null);
+        Contract.Requires((!this.IsBottom));
+        Contract.Ensures(Contract.Result<Elt>() != null);
+        Element value = this[oldName];
+        if (value == null) {
+          return this;
+        } // 'oldName' isn't in the map, so neither will be 'newName'
+        Contract.Assume(this.constraints != null);
+        IFunctionalMap newMap = this.constraints.Remove(oldName);
+        newMap = newMap.Add(newName, value);
+        return new Elt(newMap);
+      }
+
+      [Pure]
+      public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+        throw new System.NotImplementedException();
+      }
+
+    } // class
+
+    private readonly MicroLattice/*!*/ microLattice;
+
+    private readonly IPropExprFactory/*!*/ propExprFactory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(microLattice != null);
+      Contract.Invariant(propExprFactory != null);
+    }
+
+
+    private readonly /*maybe null*/IComparer variableComparer;
+
+    public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
+      : base(valueExprFactory) {
+      Contract.Requires(microLattice != null);
+      Contract.Requires(valueExprFactory != null);
+      Contract.Requires(propExprFactory != null);
+      this.propExprFactory = propExprFactory;
+      this.microLattice = microLattice;
+      this.variableComparer = variableComparer;
+      // base(valueExprFactory);
+    }
+
+    protected override object/*!*/ UniqueId {
+      get {
+        Contract.Ensures(Contract.Result<object>() != null);
+        return this.microLattice.GetType();
+      }
+    }
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return Elt.Top;
+      }
+    }
+
+    public override Element Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return Elt.Bottom;
+      }
+    }
+
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return !e.IsBottom && e.Count == 0;
+    }
+
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      return ((Elt)element).IsBottom;
+    }
+
+    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+
+      // return true iff every constraint in "this" is no weaker than the corresponding
+      // constraint in "that" and there are no additional constraints in "that"
+      foreach (IVariable/*!*/ var in a.Variables) {
+        Contract.Assert(var != null);
+        Element thisValue = cce.NonNull(a[var]);
+
+        Element thatValue = b[var];
+        if (thatValue == null) {
+          continue;
+        } // it's okay for "a" to know something "b" doesn't
+
+        if (this.microLattice.LowerThan(thisValue, thatValue)) {
+          continue;
+        } // constraint for "var" satisfies AtMost relation
+
+        return false;
+      }
+      foreach (IVariable/*!*/ var in b.Variables) {
+        Contract.Assert(var != null);
+        if (a.Lookup(var) != null) {
+          continue;
+        } // we checked this case in the loop above
+
+        Element thatValue = cce.NonNull(b[var]);
+        if (this.microLattice.IsTop(thatValue)) {
+          continue;
+        } // this is a trivial constraint
+
+        return false;
+      }
+      return true;
+    }
+
+    private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
+      Contract.Requires((newValue != null));
+      Contract.Requires((var != null));
+      Contract.Requires((element != null));
+      Contract.Ensures(Contract.Result<Elt>() != null);
+      Elt e = (Elt)element;
+
+      if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
+            {
+        /*MicroLattice*/
+        Element currentValue = e[var];
+
+        if (currentValue == null) {
+          // No information currently, so we just add the new info.
+          return e.Add(var, newValue, this.microLattice);
+        } else {
+          // Otherwise, take the meet of the new and current info.
+          //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
+          return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
+        }
+      }
+      return e;
+    }
+
+    public override string/*!*/ ToString(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      Elt e = (Elt)element;
+
+      if (IsTop(e)) {
+        return "<top>";
+      }
+      if (IsBottom(e)) {
+        return "<bottom>";
+      }
+
+      int k = 0;
+      System.Text.StringBuilder buffer = new System.Text.StringBuilder();
+      foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) {
+        Contract.Assert(key != null);
+        if (k++ > 0) {
+          buffer.Append("; ");
+        }
+        buffer.AppendFormat("{0} = {1}", key, e[key]);
+      }
+      return buffer.ToString();
+    }
+
+    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+
+      IFunctionalMap newMap = FunctionalHashtable.Empty;
+      foreach (IVariable/*!*/ key in a.Variables) {
+        Contract.Assert(key != null);
+        Element aValue = a[key];
+        Element bValue = b[key];
+
+        if (aValue != null && bValue != null) {
+          // Keep only the variables known to both elements.
+          Element newValue = this.microLattice.Join(aValue, bValue);
+          newMap = newMap.Add(key, newValue);
+        }
+      }
+      Elt/*!*/ join = new Elt(newMap);
+      Contract.Assert(join != null);
+
+      // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
+
+      return join;
+    }
+
+    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+
+      IFunctionalMap newMap = FunctionalHashtable.Empty;
+      foreach (IVariable/*!*/ key in a.Variables) {
+        Contract.Assert(key != null);
+        Element/*!*/ aValue = cce.NonNull(a[key]);
+        Element bValue = b[key];
+
+        Element newValue =
+          bValue == null ? aValue :
+          this.microLattice.Meet(aValue, bValue);
+
+        newMap = newMap.Add(key, newValue);
+      }
+      foreach (IVariable/*!*/ key in b.Variables) {
+        Contract.Assert(key != null);
+        Element aValue = a[key];
+        Element bValue = b[key];
+        Debug.Assert(bValue != null);
+
+        if (aValue == null) {
+          // It's a variable we didn't cover in the last loop.
+          newMap = newMap.Add(key, bValue);
+        }
+      }
+      return new Elt(newMap);
+    }
+
+    /// <summary>
+    /// Perform the pointwise widening of the elements in the map
+    /// </summary>
+    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires((second != null));
+      //Contract.Requires((first != null));
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+
+      // Note we have to add those cases as we do not have a "NonTrivialWiden" method
+      if (a.IsBottom)
+        return new Elt(b.Constraints);
+      if (b.IsBottom)
+        return new Elt(a.Constraints);
+
+      IFunctionalMap newMap = FunctionalHashtable.Empty;
+      foreach (IVariable/*!*/ key in a.Variables) {
+        Contract.Assert(key != null);
+        Element aValue = a[key];
+        Element bValue = b[key];
+
+        if (aValue != null && bValue != null) {
+          // Keep only the variables known to both elements.
+          Element newValue = this.microLattice.Widen(aValue, bValue);
+          newMap = newMap.Add(key, newValue);
+        }
+      }
+      Element/*!*/ widen = new Elt(newMap);
+      Contract.Assert(widen != null);
+      // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+
+      return widen;
+    }
+
+    internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars) {
+      Contract.Requires(ignoreVars != null);
+      Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<ISet>() != null);
+      HashSet s = new HashSet();
+
+      IFunApp f = e as IFunApp;
+      IFunction lambda = e as IFunction;
+
+      if (e is IVariable) {
+        if (!ignoreVars.Contains(e))
+          s.Add(e);
+      } else if (f != null) // e is IFunApp
+            {
+        foreach (IExpr/*!*/ arg in f.Arguments) {
+          Contract.Assert(arg != null);
+          s.AddAll(VariablesInExpression(arg, ignoreVars));
+        }
+      } else if (lambda != null) {
+        IMutableSet x = new HashSet(1);
+        x.Add(lambda.Param);
+
+        // Ignore the bound variable
+        s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
+      } else if (e is IUnknown) {
+        // skip (actually, it would be appropriate to return the universal set of all variables)
+      } else {
+        Debug.Assert(false, "case not handled: " + e);
+      }
+      return s;
+    }
+
+
+    private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e) {
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
+      ArrayList result = new ArrayList();
+
+      IFunApp f = e as IFunApp;
+      if (f != null) {
+        if (f.FunctionSymbol.Equals(Prop.And)) {
+          foreach (IExpr arg in f.Arguments) {
+            result.AddRange(FindConjuncts(arg));
+          }
+        } else if (f.FunctionSymbol.Equals(Prop.Or)
+                 || f.FunctionSymbol.Equals(Prop.Implies)) {
+          // Do nothing.
+        } else {
+          result.Add(e);
+        }
+      } else {
+        result.Add(e);
+      }
+
+      return result;
+    }
+
+    private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right) {
+      Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
+      left = null;
+      right = null;
+
+      // See if we have an equality
+      IFunApp nary = expr as IFunApp;
+      if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) {
+        return false;
+      }
+
+      // See if it is an equality of two variables
+      IVariable idLeft = nary.Arguments[0] as IVariable;
+      IVariable idRight = nary.Arguments[1] as IVariable;
+      if (idLeft == null || idRight == null) {
+        return false;
+      }
+
+      left = idLeft;
+      right = idRight;
+      return true;
+    }
+
+    /// <summary>
+    /// Returns true iff the expression is in the form var == arithmeticExpr
+    /// </summary>
+    private static bool IsArithmeticExpr(IExpr/*!*/ expr) {
+      Contract.Requires(expr != null);
+      // System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
+
+      if (expr is IVariable)   // expr is a variable
+        return true;
+      else if (expr is IFunApp)     // may be ==, +, -, /, % or an integer
+        {
+        IFunApp fun = (IFunApp)expr;
+
+        if (fun.FunctionSymbol is IntSymbol)     // it is an integer
+          return true;
+        else if (fun.FunctionSymbol.Equals(Int.Negate))  // it is an unary minus
+          return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
+        else if (fun.Arguments.Count != 2)       // A function of two or more operands is not arithmetic
+          return false;
+        else {
+          IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+          IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+
+          if (!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable
+            return false;
+
+          if (fun.FunctionSymbol.Equals(Value.Eq)
+              || fun.FunctionSymbol.Equals(Int.Add)
+              || fun.FunctionSymbol.Equals(Int.Sub)
+              || fun.FunctionSymbol.Equals(Int.Mul)
+              || fun.FunctionSymbol.Equals(Int.Div)
+              || fun.FunctionSymbol.Equals(Int.Mod))
+            return IsArithmeticExpr(left) && IsArithmeticExpr(right);
+          else
+            return false;
+        }
+      } else {
+        return false;
+      }
+    }
+
+    public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      if (IsTop(element)) {
+        return propExprFactory.True;
+      }
+      if (IsBottom(element)) {
+        return propExprFactory.False;
+      }
+
+      Elt e = (Elt)element;
+      IExpr truth = propExprFactory.True;
+      IExpr result = truth;
+
+      foreach (IVariable/*!*/ variable in e.SortedVariables(variableComparer)) {
+        Contract.Assert(variable != null);
+        Element value = (Element)e[variable];
+
+        if (value == null || this.microLattice.IsTop(value)) {
+          continue;
+        } // Skip variables about which we know nothing.
+        if (this.microLattice.IsBottom(value)) {
+          return propExprFactory.False;
+        }
+
+        IExpr conjunct = this.microLattice.ToPredicate(variable, value);
+
+        result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
+      }
+      return result;
+    }
+
+
+    public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
+      //Contract.Requires(variable != null);
+      //Contract.Requires(element != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
+    }
+
+    private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
+    private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) {
+      //Contract.Requires(var != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      return var;
+    }
+
+    /// <summary>
+    /// Return a new expression in which each variable has been 
+    /// replaced by an expression representing what is known about
+    /// that variable.
+    /// </summary>
+    private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
+        OnUnableToInline/*!*/ unableToInline) {
+      Contract.Requires(unableToInline != null);
+      Contract.Requires(notInlineable != null);
+      Contract.Requires(expr != null);
+      Contract.Requires(element != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      IVariable var = expr as IVariable;
+      if (var != null) {
+        /*MicroLattice*/
+        Element value = element[var];
+        if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value)) {
+          return unableToInline(var); // We don't know anything about this variable.
+        } else {
+          // GetFoldExpr returns null when it can yield an expression that
+          // can be substituted for the variable.
+          IExpr valueExpr = this.microLattice.GetFoldExpr(value);
+          return (valueExpr == null) ? var : valueExpr;
+        }
+      }
+
+      // else
+
+      IFunApp fun = expr as IFunApp;
+      if (fun != null) {
+        IList newargs = new ArrayList();
+        foreach (IExpr/*!*/ arg in fun.Arguments) {
+          Contract.Assert(arg != null);
+          newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
+        }
+        return fun.CloneWithArguments(newargs);
+      }
+
+      // else
+
+      IFunction lambda = expr as IFunction;
+      if (lambda != null) {
+        IMutableSet x = new HashSet(1);
+        x.Add(lambda.Param);
+
+        // Don't inline the bound variable
+        return lambda.CloneWithBody(
+                   InlineVariables(element, lambda.Body,
+                                    cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
+               );
+      }
+
+      // else
+
+      if (expr is IUnknown) {
+        return expr;
+      } else {
+        throw
+          new System.NotImplementedException("cannot inline identifies in expression " + expr);
+      }
+    }
+
+
+    public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
+      //Contract.Requires(expr != null);
+      //Contract.Requires(element != null);
+      //Contract.Ensures(Contract.Result<Element>() != null);
+      Elt/*!*/ result = (Elt)element;
+      Contract.Assert(result != null);
+
+      if (IsBottom(element)) {
+        return result; // == element 
+      }
+
+      expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
+
+      foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) {
+        Contract.Assert(conjunct != null);
+        IVariable left, right;
+
+        if (IsSimpleEquality(conjunct, out left, out right)) {
+          #region The conjunct is a simple equality
+
+
+          Contract.Assert(left != null && right != null);
+
+          Element leftValue = result[left], rightValue = result[right];
+          if (leftValue == null) {
+            leftValue = this.microLattice.Top;
+          }
+          if (rightValue == null) {
+            rightValue = this.microLattice.Top;
+          }
+          Element newValue = this.microLattice.Meet(leftValue, rightValue);
+          result = AddConstraint(result, left, newValue);
+          result = AddConstraint(result, right, newValue);
+
+          #endregion
+        } else {
+          ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
+
+          if (variablesInvolved.Count == 1) {
+            #region We have just one variable
+
+            IVariable var = null;
+            foreach (IVariable/*!*/ v in variablesInvolved) {
+              Contract.Assert(v != null);
+              var = v;
+            } // why is there no better way to get the elements?
+            Contract.Assert(var != null);
+            Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
+            result = AddConstraint(result, var, value);
+
+            #endregion
+          } else if (IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics) {
+            #region We evalaute an arithmetic expression
+
+            IFunApp fun = (IFunApp)conjunct;
+            if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
+                       {
+              // get the variable to be assigned
+              IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+              IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+              IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
+
+              Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
+              Contract.Assert(value != null);
+              result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
+            }
+            #endregion
+          }
+        }
+      }
+      return result;
+    }
+
+
+    public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+      //Contract.Requires(newName != null);
+      //Contract.Requires(oldName != null);
+      //Contract.Requires(element != null);
+      //Contract.Ensures(Contract.Result<Element>() != null);
+      if (IsBottom(element)) {
+        return element;
+      } else {
+        return ((Elt)element).Rename(oldName, newName, this.microLattice);
+      }
+    }
+
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      return f.Equals(Prop.And) ||
+             f.Equals(Value.Eq) ||
+             microLattice.Understands(f, args);
+    }
+
+    private sealed class EquivalentExprException : CheckedException {
+    }
+    private sealed class EquivalentExprInlineCallback {
+      private readonly IVariable/*!*/ var;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(var != null);
+      }
+
+      public EquivalentExprInlineCallback(IVariable/*!*/ var) {
+        Contract.Requires(var != null);
+        this.var = var;
+        // base();
+      }
+
+      public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
+        //throws EquivalentExprException;
+      {
+        Contract.Requires(othervar != null);
+        Contract.Ensures(Contract.Result<IExpr>() != null);
+        Contract.EnsuresOnThrow<EquivalentExprException>(true);
+        if (othervar.Equals(var))
+          throw new EquivalentExprException();
+        else
+          return othervar;
+      }
+    }
+
+    public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
+      //Contract.Requires(prohibitedVars != null);
+      //Contract.Requires(var != null);
+      //Contract.Requires(expr != null);
+      //Contract.Requires(q != null);
+      //Contract.Requires(e != null);
+      try {
+        EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
+        return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
+                               new OnUnableToInline(closure.ThrowOnUnableToInline));
+      } catch (EquivalentExprException) {
+        return null;
+      }
+    }
+
+
+    /// <summary>
+    /// Check to see if the given predicate holds in the given lattice element.
+    /// 
+    /// TODO:  We leave this unimplemented for now and just return maybe.
+    /// </summary>
+    /// <param name="e">The lattice element.</param>
+    /// <param name="pred">The predicate.</param>
+    /// <returns>Yes, No, or Maybe</returns>
+    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
+      //Contract.Requires(pred != null);
+      //Contract.Requires(e != null);
+      return Answer.Maybe;
+    }
+
+    /// <summary>
+    ///  Answers a disequality about two variables.  The same information could be obtained
+    ///  by asking CheckPredicate, but a different implementation may be simpler and more
+    ///  efficient.
+    /// 
+    ///  TODO: We leave this unimplemented for now and just return maybe.
+    /// </summary>
+    /// <param name="e">The lattice element.</param>
+    /// <param name="var1">The first variable.</param>
+    /// <param name="var2">The second variable.</param>
+    /// <returns>Yes, No, or Maybe.</returns>
+    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
+      //Contract.Requires(var2 != null);
+      //Contract.Requires(var1 != null);
+      //Contract.Requires(e != null);
+      return Answer.Maybe;
+    }
+
+    public override void Validate() {
+      base.Validate();
+      microLattice.Validate();
+    }
+
+  }
+}