1 files changed, 10 insertions, 0 deletions
diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
index 7abe52e2..d02e6f31 100644
--- a/Source/AbsInt/NativeLattice.cs
+++ b/Source/AbsInt/NativeLattice.cs
@@ -46,6 +46,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
     public abstract Element Update(Element element, AssignCmd cmd);  // requiers 'cmd' to be a simple (possibly parallel) assignment command
     public abstract Element Eliminate(Element element, Variable v);
 
+    /// <summary>
+    /// Specialize the lattice to implementation "impl", if non-null.
+    /// If "impl" is null, remove specialization.
+    /// </summary>
+    public virtual void Specialize(Implementation impl) {
+    }
+
     public virtual void Validate() {
       Contract.Assert(IsTop(Top));
       Contract.Assert(IsBottom(Bottom));
@@ -136,7 +143,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
               Expr e = Substituter.Apply(formalProcImplSubst, pre.Condition);
               start = lattice.Constrain(start, e);
             }
+
+            lattice.Specialize(impl);
             Analyze(impl, lattice, start);
+            lattice.Specialize(null);
           }
         }
       }