Merge

4 files changed, 75 insertions, 287 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 98a67409..50a8f45c 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -254,6 +254,24 @@ namespace Microsoft.Boogie
       }

 

       /// <summary>

+      /// Look for function application with a subsequence of given arguments and return its value or null if no such application exists.

+      /// </summary>

+      public Element TryPartialEval(params Element[] args)

+      {

+        foreach (var tpl in apps) {

+          int j = 0;

+          for (int i = 0; i < args.Length; ++i) {

+            if (tpl.Args[j] == args[i]) {

+              j++;

+              if (j == tpl.Args.Length)

+                return tpl.Result;

+            }

+          }

+        }

+        return null;

+      }

+

+      /// <summary>

       /// Short for TryEval(args) == (Element)true

       /// </summary>

       public bool IsTrue(params Element[] args)

@@ -515,6 +533,11 @@ namespace Microsoft.Boogie
       return res;

     }

 

+    public Func TryGetSkolemFunc(string name)

+    {

+      return Functions.Where(f => f.Name.StartsWith(name + "!")).FirstOrDefault();

+    }

+

     public Element GetElement(string name)

     {

       Element res;

@@ -524,6 +547,11 @@ namespace Microsoft.Boogie
         throw new KeyNotFoundException("element '" + name + "' undefined in the model");

     }

 

+    public Element MkIntElement(int v)

+    {

+      return MkElement(v.ToString());

+    }

+

     public void Write(System.IO.TextWriter wr)

     {

       wr.WriteLine("*** MODEL");

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 2210d357..8f8f145e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -19,7 +19,7 @@ using Microsoft.Boogie.VCExprAST;
 namespace Microsoft.Boogie {

   public class CalleeCounterexampleInfo {

     public Counterexample counterexample;

-    public List<object>/*!>!*/ args;

+    public List<Model.Element>/*!>!*/ args;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -28,7 +28,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public CalleeCounterexampleInfo(Counterexample cex, List<object/*!>!*/> x) {

+    public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {

       Contract.Requires(cex != null);

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

       counterexample = cex;

@@ -76,7 +76,7 @@ namespace Microsoft.Boogie {
 

     [Peer]

     public BlockSeq Trace;

-    public ErrorModel Model;

+    public Model Model;

     public VC.ModelViewInfo MvInfo;

     public ProverContext Context;

     [Peer]

@@ -84,7 +84,7 @@ namespace Microsoft.Boogie {
 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

-    internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context) {

+    internal Counterexample(BlockSeq trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

       this.Trace = trace;

@@ -211,7 +211,7 @@ namespace Microsoft.Boogie {
     {

       if (Model == null) return null;

 

-      Model m = Model.ToModel();

+      Model m = Model;

 

       var mvstates = m.TryGetFunc("@MV_state");

       if (MvInfo == null || mvstates == null)

@@ -308,7 +308,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(trace != null);

       Contract.Requires(failingAssert != null);

@@ -338,7 +338,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(!failingRequires.Free);

       Contract.Requires(trace != null);

@@ -371,7 +371,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index dad151e5..1bb70879 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2302,7 +2302,7 @@ namespace VC
                 {

                     if (errModel == null)

                         return;

-                    var cex = GenerateTraceMain(labels, errModel, mvInfo);

+                    var cex = GenerateTraceMain(labels, errModel.ToModel(), mvInfo);

                     Debug.Assert(candidatesToExpand.Count == 0);

                     if(cex != null) callback.OnCounterexample(cex, null);

                     return;

@@ -2311,7 +2311,7 @@ namespace VC
                 Contract.Assert(calls != null);

                 Contract.Assert(errModel != null);

 

-                GenerateTraceMain(labels, errModel, mvInfo);

+                GenerateTraceMain(labels, errModel.ToModel(), mvInfo);

 

                 /*

                     foreach (string lab in labels)

@@ -2328,13 +2328,13 @@ namespace VC
             }

 

             // Construct the interprocedural trace

-            private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo)

+            private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo)

             {

                 Contract.Requires(errModel != null);

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

                 if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null)

                 {

-                    errModel.Print(ErrorReporter.ModelWriter);

+                    errModel.Write(ErrorReporter.ModelWriter);

                     ErrorReporter.ModelWriter.Flush();

                 }

 

@@ -2365,7 +2365,7 @@ namespace VC
                 return newCounterexample;

             }

 

-            private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo,

+            private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,

                                                  int candidateId, Implementation procImpl)

             {

                 Contract.Requires(errModel != null);

@@ -2414,7 +2414,7 @@ namespace VC
             }

 

             private Counterexample GenerateTraceRec(

-                                  IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo, int candidateId,

+                                  IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo, int candidateId,

                                   Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,

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

             {

@@ -2456,28 +2456,28 @@ namespace VC
                             var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];

 

                             // Record concrete value of the argument to this procedure

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

+                            var args = new List<Model.Element>();

                             if (expr is VCExprIntLit)

                             {

-                                args.Add(errModel.valueToPartition[(expr as VCExprIntLit).Val]);

+                                args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));

                             }

                             else if (expr is VCExprVar)

                             {

                                 var idExpr = expr as VCExprVar;

                                 string name = context.Lookup(idExpr);

                                 Contract.Assert(name != null);

-                                if (errModel.identifierToPartition.ContainsKey(name))

+                                Model.Func f = errModel.TryGetFunc(name);

+                                if (f != null)

                                 {

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

+                                    args.Add(f.GetConstant());

                                 }

                             }

                             else

                             {

                                 Contract.Assert(false);

                             }

-                            var values = errModel.PartitionsToValues(args);

                             calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

-                                 new CalleeCounterexampleInfo(null, values);

+                                 new CalleeCounterexampleInfo(null, args);

                             continue;

                         }

 

@@ -2496,7 +2496,7 @@ namespace VC
                           calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                               new CalleeCounterexampleInfo(

                                   cce.NonNull(GenerateTrace(labels, errModel, mvInfo, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),

-                                  new List<object>());

+                                  new List<Model.Element>());

                         }

                     }

 

@@ -2609,7 +2609,7 @@ namespace VC
             }

 

             return extractLoopTraceRec(

-                new CalleeCounterexampleInfo(cex, new List<object>()),

+                new CalleeCounterexampleInfo(cex, new List<Model.Element>()),

                 mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

         }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 19418b46..ff106380 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1922,7 +1922,7 @@ namespace VC {
         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

 

-        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, MvInfo, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

+        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel == null ? null : errModel.ToModel(), MvInfo, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

 

         if (newCounterexample == null)

           return;

@@ -2017,7 +2017,7 @@ namespace VC {
             if (b.Cmds.Has(a)) {

               BlockSeq trace = new BlockSeq();

               trace.Add(b);

-              Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, context, incarnationOriginMap);

+              Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel == null ? null : errModel.ToModel(), MvInfo, context, incarnationOriginMap);

               callback.OnCounterexample(newCounterexample, null);

               goto NEXT_ASSERT;

             }

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

 

         return extractLoopTraceRec(

-            new CalleeCounterexampleInfo(cex, new List<object>()),

+            new CalleeCounterexampleInfo(cex, new List<Model.Element>()),

             mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

     }

 

@@ -2623,11 +2623,11 @@ namespace VC {
     }

 

     private static Counterexample LazyCounterexample(

-                                       ErrorModel/*!*/ errModel, ModelViewInfo mvInfo,

+                                       Model/*!*/ errModel, ModelViewInfo mvInfo,

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

                                        ProverContext/*!*/ context,

                                        Program/*!*/ program,

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

+                                       string/*!*/ implName, List<Model.Element>/*!*/ values)

     {

       Contract.Requires(errModel != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));

@@ -2646,9 +2646,10 @@ namespace VC {
       trace.Add(b);

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

       string cfcName = context.Lookup(cfcVar);

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

-      int cfcValue = errModel.LookupPartitionValue(cfcPartition);

-      

+      Model.Func skolemFunction = errModel.TryGetSkolemFunc(cfcName + "!" + info.uniqueId);

+      Model.Element cfcValue = skolemFunction.TryPartialEval(values.ToArray());

+

+      Model.Func controlFlowFunction = errModel.GetFunc("ControlFlow");

       var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

       while (true) {

         CmdSeq cmds = b.Cmds;Contract.Assert(cmds != null);

@@ -2657,7 +2658,7 @@ namespace VC {
         {

           Cmd cmd = cce.NonNull( cmds[i]);

           AssertCmd assertCmd = cmd as AssertCmd;

-          if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId) == assertCmd.UniqueId)

+          if (assertCmd != null && controlFlowFunction.TryEval(cfcValue, errModel.MkIntElement(b.UniqueId)).AsInt() == assertCmd.UniqueId)

           {

             Counterexample newCounterexample;

             newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, context, cce.NonNull(info.incarnationOriginMap));

@@ -2673,15 +2674,16 @@ namespace VC {
           Contract.Assert(calleeName != null);

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

       

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

+          List<Model.Element> args = new List<Model.Element>();

           foreach (Expr expr in naryExpr.Args)

           {Contract.Assert(expr != null);

             VCExprVar exprVar;

             string name;

             LiteralExpr litExpr = expr as LiteralExpr;

+            

             if (litExpr != null) 

             {

-              args.Add(errModel.valueToPartition[litExpr.Val]);

+              args.Add(errModel.MkElement(litExpr.Val.ToString()));

               continue;

             }

           

@@ -2693,7 +2695,7 @@ namespace VC {
             {

               exprVar = boogieExprTranslator.LookupVariable(var);

               name = context.Lookup(exprVar);

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

+              args.Add(errModel.GetFunc(name).GetConstant());

               continue;

             }

             

@@ -2737,17 +2739,18 @@ namespace VC {
             

             exprVar = boogieExprTranslator.LookupVariable(var);

             name = context.Lookup(exprVar);

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

+            Model.Func skolemFunction1 = errModel.TryGetSkolemFunc(name + "!" + info.uniqueId);

+            args.Add(skolemFunction1.TryPartialEval(values.ToArray()));

           }

           calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = 

             new CalleeCounterexampleInfo(

               LazyCounterexample(errModel, mvInfo, implName2LazyInliningInfo, context, program, calleeName, args),

-              errModel.PartitionsToValues(args));

+              args);

         }

           

         GotoCmd gotoCmd = transferCmd as GotoCmd;

         if (gotoCmd == null) break;

-        int nextBlockId = errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId);

+        int nextBlockId = controlFlowFunction.TryEval(cfcValue, errModel.MkIntElement(b.UniqueId)).AsInt();

         foreach (Block x in gotoCmd.labelTargets) {

           if (nextBlockId == x.UniqueId) {

             b = x;

@@ -2771,7 +2774,7 @@ namespace VC {
     }

 

     static Counterexample TraceCounterexample(

-                          Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, ErrorModel errModel, ModelViewInfo mvInfo,

+                          Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, Model errModel, ModelViewInfo mvInfo,

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

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

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

@@ -2812,13 +2815,13 @@ namespace VC {
         if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;

         Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;

         Contract.Assert(boogieExprTranslator != null);

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

+        List<Model.Element> args = new List<Model.Element>();

         foreach (Expr expr in naryExpr.Args)

         {Contract.Assert(expr != null);

           LiteralExpr litExpr = expr as LiteralExpr;

           if (litExpr != null) 

           {

-            args.Add(errModel.valueToPartition[litExpr.Val]);

+            args.Add(errModel.MkElement(litExpr.Val.ToString()));

             continue;

           }

           

@@ -2829,12 +2832,12 @@ namespace VC {
           Contract.Assert(var != null);

           string name = context.Lookup(var);

           Contract.Assert(name != null);

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

+          args.Add(errModel.GetFunc(name).GetConstant());

         }

         calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = 

             new CalleeCounterexampleInfo(

                 LazyCounterexample(errModel, mvInfo, implName2LazyInliningInfo, context, program, calleeName, args),

-                errModel.PartitionsToValues(args));

+                args);

         #endregion

       }

       

@@ -3340,231 +3343,7 @@ namespace VC {
       }

     }

 

-    //returned int is zID

-    static int GetValuesFromModel(Bpl.Expr expr, Hashtable /*Variable -> Expr*/ incarnationMap, ErrorModel errModel,

-      Dictionary<Bpl.Expr/*!*/, object>/*!*/ exprToPrintableValue) 

-      //modifies exprToPrintableValue.*;

-    {

-      Contract.Requires(expr != null);

-      Contract.Requires(incarnationMap != null);

-      Contract.Requires(errModel != null);

-      Contract.Requires(exprToPrintableValue != null);

-      // call GetValuesFromModel on all proper subexpressions, returning their value, 

-      // so they only have to be computed once!

-      if (expr is LiteralExpr) {

-        // nothing needs to be added to the exprToPrintableValue map, because e.g. 0 -> 0 is not interesting

-        object o = ((LiteralExpr) expr).Val;

-        if (o == null) {

-          o = "nullObject";

-        } 

-        int idForExprVal;

-        if (errModel.valueToPartition.TryGetValue(o, out idForExprVal)) {

-          return idForExprVal;

-        } else {

-          return -1;

-        }

-      }

-      else if (expr is IdentifierExpr) {

-        // if the expression expr is in the incarnation map, then use its incarnation, 

-        // otherwise just use the actual expression 

-        string s = ((IdentifierExpr) expr).Name;

-        object o = null;

-        Variable v = ((IdentifierExpr) expr).Decl;

-        if (v != null && incarnationMap.ContainsKey(v)) {

-          if (incarnationMap[v] is IdentifierExpr) {

-            s = ((IdentifierExpr) incarnationMap[v]).Name;

-          } else if (incarnationMap[v] is LiteralExpr) {

-            o = ((LiteralExpr) incarnationMap[v]).Val;

-          }

-        }

-        // if o is not null, then we got a LiteralExpression, that needs separate treatment

-        if (o == null) {

-          // if the expression (respectively its incarnation) is mapped to some partition

-          // then return that id, else return the error code -1

-          if (errModel.identifierToPartition.ContainsKey(s)) {

-            int i = errModel.identifierToPartition[s];

-            // if the key is already in the map we can assume that it is the same map we would

-            // get now and thus just ignore it

-            if (!exprToPrintableValue.ContainsKey(expr)) {

-              exprToPrintableValue.Add(expr, ValueFromZID(errModel, i, ((IdentifierExpr) expr).Name));

-            }

-            return i;

-          } else {

-            return -1;

-          }

-        } else if (errModel.valueToPartition.ContainsKey(o)) {

-          int i = errModel.valueToPartition[o];

-          if (!exprToPrintableValue.ContainsKey(expr))

-            exprToPrintableValue.Add(expr, ValueFromZID(errModel, i));

-          return i;

-        } else {

-          return -1;

-        }

-      }

-      else if (expr is Bpl.NAryExpr) {

-        Bpl.NAryExpr e = (Bpl.NAryExpr)expr;

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

-        bool undefined = false;

-        // do the recursion first

-        foreach (Expr argument in ((NAryExpr) expr).Args) {

-          int zid = -1;

-          if (argument != null) {

-            zid = GetValuesFromModel(argument, incarnationMap, errModel, exprToPrintableValue);

-          }

-          // if one of the arguments is 'undefined' then return -1 ('noZid') for this

-          // but make sure the recursion is complete first1

-          if (zid == -1) {

-            undefined = true;

-          }

-          zargs.Add(zid);

-        }

-        IAppliable fun = e.Fun;

-        Contract.Assert(fun != null);

-        string functionName = fun.FunctionName; // PR: convert to select1, select2, etc in case of a map?

-        // same as IndexedExpr:

-        int id = TreatFunction(functionName, zargs, undefined, errModel);

-        if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {

-          exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));

-        }

-        return id;

-      } 

-      else if (expr is Bpl.OldExpr) {

-        //Bpl.OldExpr e = (Bpl.OldExpr)expr;

-        // We do not know which heap is the old heap and what the latest state change was,

-        // therefore we cannot return anything useful here!

-        return -1;

-      } 

-      else if (expr is Bpl.QuantifierExpr) {

-        Bpl.QuantifierExpr q = (Bpl.QuantifierExpr)expr;

-        for (int i = 0; i < q.Dummies.Length; i++) {

-          Bpl.Variable v = q.Dummies[i];

-          if (v != null) {

-            // add to the incarnation map a connection between the bound variable v

-            // of the quantifier and its skolemized incarnation, if available,

-            // i.e., search through the list of identifiers in the model and look for

-            // v.sk.(q.SkolemId), only pick those that are directly associated to a value

-            // DISCLAIMER: of course it is very well possible that one of these incarnations 

-            // could be used without actually having a value, but it seems better to pick those

-            // with a value, that is they are more likely to contribute useful information to 

-            // the output

-            List<Bpl.IdentifierExpr> quantVarIncarnationList = new List<Bpl.IdentifierExpr>();

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

-            int numberOfNonNullValueIncarnations = 0;

-            for (int j = 0; j < errModel.partitionToIdentifiers.Count; j++){

-              List<string> pti = errModel.partitionToIdentifiers[j];

-              Contract.Assert(pti != null);

-              if (pti != null) {

-                for (int k = 0; k < pti.Count; k++) {

-                  // look for v.sk.(q.SkolemId)

-                  // if there is more than one look at if there is exactly one with a non-null value

-                  // associated, see above explanation

-                  if (pti[k].StartsWith(v + ".sk." + q.SkolemId) && 

-                      errModel.partitionToValue[errModel.identifierToPartition[pti[k]]] != null) {

-                    quantVarIncarnationList.Add(new Bpl.IdentifierExpr(Bpl.Token.NoToken, pti[k], new Bpl.UnresolvedTypeIdentifier(Token.NoToken, "TName")));

-                    incarnationZidList.Add(j);

-                    if (errModel.partitionToValue[errModel.identifierToPartition[pti[k]]] != null) {

-                      numberOfNonNullValueIncarnations++;

-                    }

-                  }

-                }

-              }

-            }

-            // only one such variable found, associate it with v

-            if (quantVarIncarnationList.Count == 1) {

-              incarnationMap[v] = quantVarIncarnationList[0];

-            } else if (quantVarIncarnationList.Count > 1 && numberOfNonNullValueIncarnations == 1) {

-              // if there are multiple candidate incarnations and exactly one of them has a value 

-              // we can pick that one; otherwise it is not clear how to pick one out of multiple 

-              // incarnations without a value or out of multiple incarnations with a value associated

-              for (int n = 0; n < incarnationZidList.Count; n++) {

-                if (errModel.partitionToValue[incarnationZidList[n]] != null) {

-                  // quantVarIncarnationList and incarnationZidList are indexed in lockstep, so if

-                  // for the associated zid the partitionToValue map is non-null then that is the one

-                  // thus distinguished incarnation we want to put into the incarnationMap

-                  incarnationMap[v] = quantVarIncarnationList[n];

-                  break;

-                }

-              }

-            }

-          }

-        }

-        // generate the value of the body but do not return that outside

-        GetValuesFromModel(q.Body, incarnationMap, errModel, exprToPrintableValue);

-        // the quantifier cannot contribute any one value to the rest of the 

-        // expression, thus just return -1

-        return -1;

-      } 

-      else if (expr is Bpl.BvExtractExpr) {

-        Bpl.BvExtractExpr ex = (Bpl.BvExtractExpr) expr;

-        Bpl.Expr e0 = ex.Bitvector;

-        Bpl.Expr e1 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.Start));

-        Bpl.Expr e2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.End));

-        string functionName = "$bv_extract";

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

-        bool undefined = false;

-        

-        int zid = -1;

-        zid = GetValuesFromModel(e0, incarnationMap, errModel, exprToPrintableValue);

-        if (zid == -1) {

-          undefined = true;

-        }

-        zargs.Add(zid);

-        

-        zid = -1;

-        zid = GetValuesFromModel(e1, incarnationMap, errModel, exprToPrintableValue);

-        if (zid == -1) {

-          undefined = true;

-        }

-        zargs.Add(zid);

-        

-        zid = -1;

-        zid = GetValuesFromModel(e2, incarnationMap, errModel, exprToPrintableValue);

-        if (zid == -1) {

-          undefined = true;

-        }

-        zargs.Add(zid);

-        

-        //same as NAryExpr:

-        int id = TreatFunction(functionName, zargs, undefined, errModel);

-        if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {

-          exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));

-        }

-        return id;

-      } 

-      else if (expr is Bpl.BvConcatExpr) {

-        // see comment above

-        Bpl.BvConcatExpr bvc = (Bpl.BvConcatExpr) expr;

-        string functionName = "$bv_concat";

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

-        bool undefined = false;

-        

-        int zid = -1;

-        zid = GetValuesFromModel(bvc.E0, incarnationMap, errModel, exprToPrintableValue);

-        if (zid == -1) {

-          undefined = true;

-        }

-        zargs.Add(zid);

-        

-        zid = -1;

-        zid = GetValuesFromModel(bvc.E0, incarnationMap, errModel, exprToPrintableValue);

-        if (zid == -1) {

-          undefined = true;

-        }

-        zargs.Add(zid);

-      

-        //same as NAryExpr:

-        int id = TreatFunction(functionName, zargs, undefined, errModel);

-        if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {

-          exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));

-        }

-        return id;

-      }

-      else {

-        Contract.Assert(false);throw new cce.UnreachableException();  // unexpected Bpl.Expr

-      }

-    }

-

-    protected static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo, ProverContext context,

+    protected static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context,

       Dictionary<Incarnation, Absy> incarnationOriginMap) 

     {

       Contract.Requires(cmd != null);

@@ -3575,16 +3354,7 @@ namespace VC {
       Contract.Ensures(Contract.Result<Counterexample>() != null);

 

       List<string> relatedInformation = new List<string>();

-      if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {

-        if (cmd.OrigExpr != null && cmd.IncarnationMap != null && errModel != null) {

-          

-          // get all possible information first

-          Dictionary<Expr, object> exprToPrintableValue = new Dictionary<Expr, object>();

-          GetValuesFromModel(cmd.OrigExpr, cmd.IncarnationMap, errModel, exprToPrintableValue);

-          // then apply the strategies

-          ApplyEnhancedErrorPrintingStrategy(cmd.OrigExpr, cmd.IncarnationMap, cmd.ErrorDataEnhanced, errModel, exprToPrintableValue, relatedInformation, true, incarnationOriginMap);

-        }

-      }

+      

       

       // See if it is a special assert inserted in translation

       if (cmd is AssertRequiresCmd)

@@ -3611,16 +3381,6 @@ namespace VC {
       }

     }

 

-    //    static void EmitImpl(Implementation! impl, bool printDesugarings) {

-    //      int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

-    //      CommandLineOptions.Clo.PrintUnstructured = 2;  // print only the unstructured program

-    //      bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings;

-    //      CommandLineOptions.Clo.PrintDesugarings = printDesugarings;

-    //      impl.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-    //      CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;

-    //      CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

-    //    }

-

     static VCExpr LetVC(Block startBlock,

                         Variable controlFlowVariable,

                         Hashtable/*<int, Absy!>*/ label2absy,