bug fixes in z3api

7 files changed, 110 insertions, 74 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 64533c02..631597b2 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -83,7 +83,7 @@ namespace Microsoft.Boogie.Z3
     {

         void CreateBacktrackPoint();

         void Backtrack();

-        void AddAxiom(VCExpr vc, LineariserOptions linOptions);

+        void AddAxiom(VCExpr axiom, LineariserOptions linOptions);

         void AddConjecture(VCExpr vc, LineariserOptions linOptions);

         void AddSmtlibString(string smtlibString);

         string GetDeclName(Z3ConstDeclAst constDeclAst);

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 7c41f25c..8d0c8aeb 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -10,6 +10,7 @@ using Microsoft.Boogie;
 using Microsoft.Boogie.Z3;

 using Microsoft.Z3;

 using Microsoft.Boogie.VCExprAST;

+using Microsoft.Boogie.Simplify;

 

 using TypeAst = System.IntPtr;

 using TermAst = System.IntPtr;

@@ -20,49 +21,62 @@ using PatternAst = System.IntPtr;
 

 namespace Microsoft.Boogie.Z3

 {

-    public class Z3apiProcessTheoremProver : Z3ProcessTheoremProver

+    public class Z3apiProcessTheoremProver : ProverInterface

     {

-        public Z3apiProcessTheoremProver(VCExpressionGenerator gen,

-                                         DeclFreeProverContext ctx,

-                                         Z3InstanceOptions opts)

-            : base(gen, ctx, opts)

+        public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)

         {

+            this.options = opts;

+            this.context = (Z3apiProverContext) ctxt;

             this.z3ContextIsUsed = false;

         }

 

+        private Z3InstanceOptions options;

+

+        private Z3apiProverContext context;

+        public override ProverContext Context

+        {

+            get { return context; }

+        }

+

+        public override VCExpressionGenerator VCExprGen

+        {

+            get { return context.ExprGen; }

+        }

+

         public override void Close()

         {

             base.Close();

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

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

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

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

         }

         private bool z3ContextIsUsed;

 

         public void PushAxiom(VCExpr axiom)

         {

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

+            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

             cm.CreateBacktrackPoint();

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

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

+            cm.AddAxiom(axiom, linOptions);

+            

         }

 

         private void PushConjecture(VCExpr conjecture)

         {

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

+            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

             cm.CreateBacktrackPoint();

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

-            cm.AddConjecture((VCExpr)conjecture, linOptions);

+            cm.AddConjecture(conjecture, linOptions);

         }

 

         public void PrepareCheck(string descriptiveName, VCExpr vc)

         {

-            PushAxiom(ctx.Axioms);

+            PushAxiom(context.Axioms);

             PushConjecture(vc);

         }

 

         public void BeginPreparedCheck()

         {

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

+            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

             outcome = Outcome.Undetermined;

             outcome = cm.Check(out z3LabelModels);

         }

@@ -75,19 +89,19 @@ namespace Microsoft.Boogie.Z3
         public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

         {

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

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

+            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

             if (z3ContextIsUsed)

             {

                 cm.Backtrack();

             }

             else

             {

-                cm.AddAxiom((VCExpr)ctx.Axioms, linOptions);

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

                 z3ContextIsUsed = true;

             }

 

             cm.CreateBacktrackPoint();

-            cm.AddConjecture((VCExpr)vc, linOptions);

+            cm.AddConjecture(vc, linOptions);

 

             BeginPreparedCheck();

         }

@@ -111,12 +125,13 @@ namespace Microsoft.Boogie.Z3
 

         public void CreateBacktrackPoint()

         {

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

+            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

             cm.CreateBacktrackPoint();

         }

+

         override public void Pop()

         {

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

+            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

             cm.Backtrack();

         }

 

@@ -148,13 +163,11 @@ namespace Microsoft.Boogie.Z3
     {

         public Z3SafeContext cm;

         

-        public Z3apiProverContext(VCExpressionGenerator gen, 

-                                  VCGenerationOptions genOptions, 

-                                  Z3InstanceOptions opts)

-            : base(gen, genOptions)

+        public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)

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

         {

             Z3Config config = BuildConfig(opts.Timeout, true);

-            this.cm = new Z3SafeContext(config, gen);

+            this.cm = new Z3SafeContext(this, config, gen);

         }

         private static Z3Config BuildConfig(int timeout, bool nativeBv)

         {

@@ -208,25 +221,37 @@ namespace Microsoft.Boogie.Z3
             base.DeclareGlobalVariable(v, attributes);

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

         }

+

+        public override string Lookup(VCExprVar var)

+        {

+            return cm.Namer.Lookup(var);

+        }

     }

 }

 

 namespace Microsoft.Boogie.Z3api

 {

-    public class Factory : Microsoft.Boogie.Z3.Factory

+    public class Factory : ProverFactory

     {

-        protected override Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,

-                                                              DeclFreeProverContext ctx,

-                                                              Z3InstanceOptions opts)

+        public override object SpawnProver(ProverOptions options, object ctxt)

+        {

+            return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt);

+        }

+

+        public override object NewProverContext(ProverOptions opts)

         {

-            return new Z3apiProcessTheoremProver(gen, ctx, opts);

+            if (CommandLineOptions.Clo.BracketIdsInVC < 0)

+            {

+                CommandLineOptions.Clo.BracketIdsInVC = 0;

+            }

+

+            VCExpressionGenerator gen = new VCExpressionGenerator();

+            return new Z3apiProverContext((Z3InstanceOptions)opts, gen);

         }

 

-        protected override DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,

-                                                                  VCGenerationOptions genOptions,

-                                                                  Z3InstanceOptions opts)

+        public override ProverOptions BlankProverOptions()

         {

-            return new Z3apiProverContext(gen, genOptions, opts);

+            return new Z3InstanceOptions();

         }

     }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 9ce303f4..c6907639 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -87,8 +87,29 @@ namespace Microsoft.Boogie.Z3
 

         public Context z3;

         public Z3Config config;

+        public Z3apiProverContext ctxt;

         private VCExpressionGenerator gen;

         private Z3TypeCachedBuilder tm;

+        private UniqueNamer namer;

+        public UniqueNamer Namer

+        {

+            get { return namer; }

+        }

+

+        public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen)

+        {

+            Context z3 = new Context(config.Config);

+            if (config.LogFilename != null)

+                z3.OpenLog(config.LogFilename);

+            foreach (string tag in config.DebugTraces)

+                z3.EnableDebugTrace(tag);

+            this.ctxt = ctxt;

+            this.z3 = z3;

+            this.config = config;

+            this.tm = new Z3TypeCachedBuilder(this);

+            this.gen = gen;

+            this.namer = new UniqueNamer();

+        }

 

         public void CreateBacktrackPoint()

         {

@@ -108,10 +129,10 @@ namespace Microsoft.Boogie.Z3
             symbols.Backtrack();

         }

 

-        public void AddAxiom(VCExpr vc, LineariserOptions linOptions)

+        public void AddAxiom(VCExpr axiom, LineariserOptions linOptions)

         {

-            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);

-            Z3TermAst z3ast = (Z3TermAst)vc.Accept(visitor, linOptions);

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

+            Z3TermAst z3ast = (Z3TermAst)axiom.Accept(visitor, linOptions);

             Term term = Unwrap(z3ast);

             z3.AssertCnstr(term);

         }

@@ -119,7 +140,7 @@ namespace Microsoft.Boogie.Z3
         public void AddConjecture(VCExpr vc, LineariserOptions linOptions)

         {

             VCExpr not_vc = (VCExpr)this.gen.Not(vc);

-            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);

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

             Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);

             Term term = Unwrap(z3ast);

             z3.AssertCnstr(term);

@@ -346,7 +367,7 @@ namespace Microsoft.Boogie.Z3
                 //System.Console.WriteLine("Check Begin");

                 outcome = z3.CheckAndGetModel(out z3Model);

                 //System.Console.WriteLine("Check End");

-                if (outcome == LBool.True)

+                if (outcome != LBool.False)

                 {

                     Debug.Assert(z3Model != null);

 

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

         }

 

-        public Z3SafeContext(Z3Config config, VCExpressionGenerator gen)

-        {

-            Context z3 = new Context(config.Config);

-            // TBD: z3.EnableArithmetic();

-            if (config.LogFilename != null)

-                z3.OpenLog(config.LogFilename);

-            foreach (string tag in config.DebugTraces)

-                z3.EnableDebugTrace(tag);

-            this.z3 = z3;

-            this.config = config;

-            this.tm = new Z3TypeCachedBuilder(this);

-            this.gen = gen;

-        }

-

         public void DeclareType(string typeName)

         {

         }

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index 0284d219..ade8cad0 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -12,14 +12,14 @@ using Microsoft.Z3;
 using Microsoft.Boogie.VCExprAST;

 

 namespace Microsoft.Boogie.Z3 {

-  public class Z3StubContext:Z3Context {

+  public class Z3StubContext : Z3Context {

     class Z3StubPatternAst: Z3PatternAst {}

     class Z3StubTermAst: Z3TermAst {}

     class Z3StubLabeledLiterals: Z3LabeledLiterals {}

   

     public void CreateBacktrackPoint(){}

     public void Backtrack(){}

-    public void AddAxiom(VCExpr vc, LineariserOptions linOptions) {}

+    public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) { }

     public void AddConjecture(VCExpr vc, LineariserOptions linOptions){}

     public void AddSmtlibString(string smtlibString) {}

     public string GetDeclName(Z3ConstDeclAst constDeclAst) {

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index b2a84c8f..35bdb61a 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -32,10 +32,10 @@ namespace Microsoft.Boogie.Z3
         internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;

         protected Z3Context cm;

 

-        public Z3apiExprLineariser(Z3Context cm)

+        public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)

         {

             this.cm = cm;

-            this.namer = new UniqueNamer();

+            this.namer = namer;

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

         }

 

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 66f1e9a1..40e454fb 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -29,6 +29,7 @@ namespace Microsoft.Boogie
     public virtual void AddAxiom(Axiom a, string attributes) {Contract.Requires(a != null); ProcessDeclaration(a); }

     public virtual void DeclareGlobalVariable(GlobalVariable v, string attributes) {Contract.Requires(v != null); ProcessDeclaration(v); }

     public abstract void AddAxiom(VCExpr vc);

+    public abstract string Lookup(VCExprVar var);

     public abstract VCExpressionGenerator ExprGen { get; }

     public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }

     public abstract VCGenerationOptions VCGenOptions { get; }

@@ -232,6 +233,11 @@ void ObjectInvariant()
       return res;

     }

 

+    public override string Lookup(VCExprVar var)

+    {

+        return exprTranslator.Lookup(var);

+    }

+

     public override VCExpressionGenerator ExprGen { get {Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);

 

      return gen;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 7d994160..9ca934b2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1585,9 +1585,9 @@ namespace VC {
         Contract.Assert(vc != null);

 

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-          reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, cce.NonNull((DeclFreeProverContext)this.Checker.TheoremProver.Context), parent.program);

+          reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

         } else {

-          reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, (DeclFreeProverContext)this.Checker.TheoremProver.Context, parent.program);

+          reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, this.Checker.TheoremProver.Context, parent.program);

         }

 

         if (CommandLineOptions.Clo.TraceVerify && no >= 0) {

@@ -2454,15 +2454,15 @@ namespace VC {
       /*

       ErrorReporter errReporter;

       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-        errReporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, (DeclFreeProverContext!) checker.TheoremProver.Context, program);

+        errReporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, checker.TheoremProver.Context, program);

       } else {

-        errReporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, (DeclFreeProverContext!) checker.TheoremProver.Context, program);

+        errReporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, checker.TheoremProver.Context, program);

       }

       */

 

       reporter = new StratifiedInliningErrorReporter(

          cce.NonNull(implName2StratifiedInliningInfo), checker.TheoremProver, callback,

-         (DeclFreeProverContext)checker.TheoremProver.Context, gotoCmdOrigins, program, impl);

+         checker.TheoremProver.Context, gotoCmdOrigins, program, impl);

 

     }

 

@@ -2879,7 +2879,7 @@ namespace VC {
       }

 

       Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo;

-      DeclFreeProverContext/*!*/ context;

+      ProverContext/*!*/ context;

       Program/*!*/ program;

 

       public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,

@@ -2888,7 +2888,7 @@ namespace VC {
           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

           VerifierCallback/*!*/ callback,

           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

-          DeclFreeProverContext/*!*/ context,

+          ProverContext/*!*/ context,

           Program/*!*/ program) {

         Contract.Requires(gotoCmdOrigins != null);

         Contract.Requires(label2absy != null);

@@ -2980,7 +2980,7 @@ namespace VC {
           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

           VerifierCallback/*!*/ callback,

           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

-          DeclFreeProverContext/*!*/ context,

+          ProverContext/*!*/ context,

           Program/*!*/ program)

         : base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, context, program) // here for aesthetic purposes //TODO: Maybe nix?

       {

@@ -3047,7 +3047,7 @@ namespace VC {
       FCallHandler calls;

       Program/*!*/ program;

       Implementation/*!*/ mainImpl;

-      DeclFreeProverContext/*!*/ context;

+      ProverContext/*!*/ context;

       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

 

       public bool underapproximationMode;

@@ -3066,7 +3066,7 @@ namespace VC {
 

 

       public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,

-                                             ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, DeclFreeProverContext/*!*/ context,

+                                             ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ProverContext/*!*/ context,

                                              Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,

                                              Program/*!*/ program, Implementation/*!*/ mainImpl) {

         Contract.Requires(cce.NonNullElements(implName2StratifiedInliningInfo));

@@ -3673,7 +3673,7 @@ namespace VC {
     private static Counterexample LazyCounterexample(

                                        ErrorModel/*!*/ errModel,

                                        Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

-                                       DeclFreeProverContext/*!*/ context,

+                                       ProverContext/*!*/ context,

                                        Program/*!*/ program,

                                        string/*!*/ implName, List<int>/*!*/ values)

     {

@@ -3685,7 +3685,6 @@ namespace VC {
       Contract.Requires(values != null);

       Contract.Ensures(Contract.Result<Counterexample>() != null);

 

-      VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);

       Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;

       Contract.Assert(boogieExprTranslator != null);

       LazyInliningInfo info = implName2LazyInliningInfo[implName];

@@ -3694,7 +3693,7 @@ namespace VC {
       Block b = cce.NonNull( info.impl).Blocks[0];

       trace.Add(b);

       VCExprVar cfcVar = boogieExprTranslator.LookupVariable(info.controlFlowVariable);

-      string cfcName = vcExprTranslator.Lookup(cfcVar);

+      string cfcName = context.Lookup(cfcVar);

       int cfcPartition = errModel.LookupSkolemFunctionAt(cfcName + "!" + info.uniqueId, values);

       int cfcValue = errModel.LookupPartitionValue(cfcPartition);

       

@@ -3741,7 +3740,7 @@ namespace VC {
             if (var is Constant) 

             {

               exprVar = boogieExprTranslator.LookupVariable(var);

-              name = vcExprTranslator.Lookup(exprVar);

+              name = context.Lookup(exprVar);

               args.Add(errModel.identifierToPartition[name]);

               continue;

             }

@@ -3785,7 +3784,7 @@ namespace VC {
             }

             

             exprVar = boogieExprTranslator.LookupVariable(var);

-            name = vcExprTranslator.Lookup(exprVar);

+            name = context.Lookup(exprVar);

             args.Add(errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values));

           }

           calleeCounterexamples[assumeCmd] = 

@@ -3817,7 +3816,7 @@ namespace VC {
                           Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, ErrorModel errModel,

                           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

                           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

-                          DeclFreeProverContext/*!*/ context, Program/*!*/ program,

+                          ProverContext/*!*/ context, Program/*!*/ program,

                           Dictionary<Absy/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

     {

       Contract.Requires(b != null);

@@ -3854,7 +3853,6 @@ namespace VC {
         if (naryExpr == null) continue;

         string calleeName = naryExpr.Fun.FunctionName;

         if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;

-        VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);

         Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;

         Contract.Assert(boogieExprTranslator != null);

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

@@ -3872,7 +3870,7 @@ namespace VC {
           Contract.Assert( idExpr.Decl != null);

           VCExprVar var = boogieExprTranslator.LookupVariable(idExpr.Decl);

           Contract.Assert(var != null);

-          string name = vcExprTranslator.Lookup(var);

+          string name = context.Lookup(var);

           Contract.Assert(name != null);

           args.Add(errModel.identifierToPartition[name]);

         }