Merge.

4 files changed, 490 insertions, 37 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 98bb95d2..e9e6b60e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -480,6 +480,7 @@ namespace Microsoft.Boogie {
     public bool UseSmtOutputFormat = false;

     public bool WeakArrayTheory = false;

     public bool UseLabels = true;

+    public bool SIBoolControlVC = false;

     public bool MonomorphicArrays {

       get {

         return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic;

@@ -1417,6 +1418,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || 

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

+              ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) ||

               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

               ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||

               ps.CheckBooleanFlag("reverseHoudiniWorklist", ref ReverseHoudiniWorklist) ||

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e5cffd93..b85fdec1 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -159,12 +159,12 @@ namespace Microsoft.Boogie.SMTLib
     internal TypeAxiomBuilder AxBuilder { get; private set; }

     internal readonly UniqueNamer Namer;

     readonly TypeDeclCollector DeclCollector;

-    SMTLibProcess Process;

+    protected SMTLibProcess Process;

     readonly List<string> proverErrors = new List<string>();

     readonly List<string> proverWarnings = new List<string>();

     readonly StringBuilder common = new StringBuilder();

     TextWriter currentLogFile;

-    volatile ErrorHandler currentErrorHandler;

+    protected volatile ErrorHandler currentErrorHandler;

 

     private void FeedTypeDeclsToProver()

     {

@@ -187,7 +187,7 @@ namespace Microsoft.Boogie.SMTLib
       Send(s, true);

     }

 

-    private void SendThisVC(string s)

+    protected void SendThisVC(string s)

     {

       Send(s, false);

     }

@@ -560,7 +560,7 @@ namespace Microsoft.Boogie.SMTLib
             return temp;

         }

 		

-		private VCExpr SExprToVCExpr (SExpr e, Dictionary<string,VCExpr> bound)

+		protected VCExpr SExprToVCExpr (SExpr e, Dictionary<string,VCExpr> bound)

 		{

 			if (e.Arguments.Count() == 0) {

 				var name = StripCruft(e.Name);

@@ -1160,7 +1160,7 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

-    private void HandleProverError(string s)

+    protected void HandleProverError(string s)

     {

       s = s.Replace("\r", "");

       lock (proverWarnings) {

@@ -1248,7 +1248,10 @@ namespace Microsoft.Boogie.SMTLib
                 xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

               }

             }

-            else {

+            else if(CommandLineOptions.Clo.SIBoolControlVC) {

+                labels = new string[0];

+                xlabels = labels;

+            } else {

               labels = CalculatePath(handler.StartingProcId());

               xlabels = labels;

             }

@@ -2095,6 +2098,236 @@ namespace Microsoft.Boogie.SMTLib
     }

   }

 

+  public class SMTLibInterpolatingProcessTheoremProver : SMTLibProcessTheoremProver

+  {

+      SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,

+                                        SMTLibProverContext ctx)

+          : base(options, gen, ctx)

+      {

+          // anything else?

+      }

+

+      public override void AssertNamed(VCExpr vc, bool polarity, string name)

+      {

+          string vcString;

+          if (polarity)

+          {

+              vcString = VCExpr2String(vc, 1);

+          }

+          else

+          {

+              vcString = "(not " + VCExpr2String(vc, 1) + ")";

+          }

+          AssertAxioms();

+          SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));

+      }

+

+      public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B)

+      {

+          string A_str = VCExpr2String(A, 1);

+          string B_str = VCExpr2String(B, 1);

+

+          AssertAxioms();

+          SendThisVC("(compute-interpolant " + A_str + " " + B_str + ")");

+

+          SExpr interpolant;

+          Outcome result = GetInterpolantResponse(out interpolant);

+

+          if (result != Outcome.Valid)

+              return null;

+

+          VCExpr interpolantVC = SExprToVCExpr(interpolant, new Dictionary<string, VCExpr>());

+          return interpolantVC;

+      }

+

+      private Outcome GetInterpolantResponse(out SExpr interpolant)

+      {

+          var result = Outcome.Undetermined;

+          var wasUnknown = false;

+          interpolant = null;

+

+          Process.Ping();

+          bool onlyOnce = false;

+

+          while (true)

+          {

+              var resp = Process.GetProverResponse();

+              if (resp == null || Process.IsPong(resp))

+                  break;

+

+              switch (resp.Name)

+              {

+                  case "unsat":

+                      result = Outcome.Valid;

+                      break;

+                  case "sat":

+                      result = Outcome.Invalid;

+                      break;

+                  case "unknown":

+                      result = Outcome.Invalid;

+                      wasUnknown = true;

+                      break;

+                  default:

+                      if (result == Outcome.Valid)

+                      {

+                          interpolant = resp as SExpr;

+

+                          Contract.Assert(onlyOnce == false);

+                          onlyOnce = true;

+                          continue;

+                      }

+                      HandleProverError("Unexpected prover response: " + resp.ToString());

+                      break;

+              }

+          }

+

+          if (wasUnknown)

+          {

+              SendThisVC("(get-info :reason-unknown)");

+              Process.Ping();

+

+              while (true)

+              {

+                  var resp = Process.GetProverResponse();

+                  if (resp == null || Process.IsPong(resp))

+                      break;

+

+                  if (resp.ArgCount == 1 && resp.Name == ":reason-unknown")

+                  {

+                      switch (resp[0].Name)

+                      {

+                          case "memout":

+                              currentErrorHandler.OnResourceExceeded("memory");

+                              result = Outcome.OutOfMemory;

+                              Process.NeedsRestart = true;

+                              break;

+                          case "timeout":

+                          case "canceled":

+                              currentErrorHandler.OnResourceExceeded("timeout");

+                              result = Outcome.TimeOut;

+                              break;

+                          default:

+                              break;

+                      }

+                  }

+                  else

+                  {

+                      HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString());

+                  }

+              }

+          }

+

+          return result;

+      }

+

+      public override List<VCExpr> GetTreeInterpolant(List<string> root, List<string> leaves)

+      {

+          List<VCExpr> result = new List<VCExpr>();

+

+          string vcStr = "true";

+          foreach (string str in root)

+              vcStr = vcStr + " " + str;

+          foreach (string str in leaves)

+              vcStr = vcStr + "\r\n (interp " + str + ")";

+

+          vcStr = "(get-interpolant (and\r\n" + vcStr + "\r\n))";

+          SendThisVC(vcStr);

+

+          List<SExpr> interpolantList;

+          Outcome result2 = GetTreeInterpolantResponse(out interpolantList);

+

+          if (result2 != Outcome.Valid)

+              return null;

+

+          Dictionary<string, VCExpr> bound = new Dictionary<string, VCExpr>();

+          foreach (SExpr sexpr in interpolantList)

+          {

+              VCExpr interpolantVC = SExprToVCExpr(sexpr, bound);

+              result.Add(interpolantVC);

+          }

+

+          return result;

+      }

+

+      private Outcome GetTreeInterpolantResponse(out List<SExpr> interpolantList)

+      {

+          var result = Outcome.Undetermined;

+          var wasUnknown = false;

+          interpolantList = new List<SExpr>();

+

+          Process.Ping();

+

+          while (true)

+          {

+              var resp = Process.GetProverResponse();

+              if (resp == null || Process.IsPong(resp))

+                  break;

+

+              switch (resp.Name)

+              {

+                  case "unsat":

+                      result = Outcome.Valid;

+                      break;

+                  case "sat":

+                      result = Outcome.Invalid;

+                      break;

+                  case "unknown":

+                      result = Outcome.Invalid;

+                      wasUnknown = true;

+                      break;

+                  default:

+                      if (result == Outcome.Valid)

+                      {

+                          SExpr interpolant = resp as SExpr;

+                          interpolantList.Add(interpolant);

+                          continue;

+                          //return result;

+                      }

+                      HandleProverError("Unexpected prover response: " + resp.ToString());

+                      break;

+              }

+          }

+

+          if (wasUnknown)

+          {

+              SendThisVC("(get-info :reason-unknown)");

+              Process.Ping();

+

+              while (true)

+              {

+                  var resp = Process.GetProverResponse();

+                  if (resp == null || Process.IsPong(resp))

+                      break;

+

+                  if (resp.ArgCount == 1 && resp.Name == ":reason-unknown")

+                  {

+                      switch (resp[0].Name)

+                      {

+                          case "memout":

+                              currentErrorHandler.OnResourceExceeded("memory");

+                              result = Outcome.OutOfMemory;

+                              Process.NeedsRestart = true;

+                              break;

+                          case "timeout":

+                          case "canceled":

+                              currentErrorHandler.OnResourceExceeded("timeout");

+                              result = Outcome.TimeOut;

+                              break;

+                          default:

+                              break;

+                      }

+                  }

+                  else

+                  {

+                      HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString());

+                  }

+              }

+          }

+

+          return result;

+      }

+  }

+

   public class SMTLibProverContext : DeclFreeProverContext

   {

     internal SMTLibProcessTheoremProver parent;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index bb34c8f8..8cee2675 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -603,6 +603,32 @@ namespace Microsoft.Boogie {
     {

         throw new NotImplementedException();

     }

+

+    //////////////////////

+    // For interpolation queries

+    //////////////////////

+

+    // Assert vc tagged with a name

+    public virtual void AssertNamed(VCExpr vc, bool polarity, string name)

+    {

+        throw new NotImplementedException();

+    }

+

+    // Returns Interpolant(A,B)

+    public virtual VCExpr ComputeInterpolant(VCExpr A, VCExpr B)

+    {

+        throw new NotImplementedException();

+    }

+

+    // Returns for each l, Interpolant(root + (leaves - l), l)

+    // Preconditions:

+    //    leaves cannot have subformulas with same variable names

+    //    Both root and leaves should have been previously named via AssertNamed

+    public virtual List<VCExpr> GetTreeInterpolant(List<string> root, List<string> leaves)

+    {

+        throw new NotImplementedException();

+    }

+

   }

 

   public class ProverInterfaceContracts : ProverInterface {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index a9745b3c..e8194891 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -195,7 +195,8 @@ namespace VC {
     public Implementation impl;

     public Function function;

     public Variable controlFlowVariable;

-    public AssertCmd exitAssertCmd;

+    public Dictionary<Block, VCExprVar> blockToControlVar;

+    public Cmd exitAssertCmd;

     public VCExpr vcexpr;

     public List<VCExprVar> interfaceExprVars;

     public List<VCExprVar> privateExprVars;

@@ -252,8 +253,148 @@ namespace VC {
       initialized = false;

     }

 

+    public void GenerateVCBoolControl()

+    {

+        Debug.Assert(!initialized);

+        Debug.Assert(CommandLineOptions.Clo.SIBoolControlVC);

+

+        // fix names for exit variables

+        var outputVariables = new List<Variable>();

+        var assertConjuncts = new List<Expr>();

+        foreach (Variable v in impl.OutParams)

+        {

+            Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

+            outputVariables.Add(c);

+            Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

+            assertConjuncts.Add(eqExpr);

+        }

+        foreach (IdentifierExpr e in impl.Proc.Modifies)

+        {

+            if (e.Decl == null) continue;

+            Variable v = e.Decl;

+            Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

+            outputVariables.Add(c);

+            Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

+            assertConjuncts.Add(eqExpr);

+        }

+        exitAssertCmd = new AssumeCmd(Token.NoToken, Expr.BinaryTreeAnd(assertConjuncts));

+        (exitAssertCmd as AssumeCmd).Attributes = new QKeyValue(Token.NoToken, "exitAssert", new List<object>(), null);

+

+        // no need for label2absy

+        label2absy = new Dictionary<int, Absy>();

+

+        // Passify

+        Program program = vcgen.program;

+        ProverInterface proverInterface = vcgen.prover;

+        vcgen.ConvertCFG2DAG(impl);

+        vcgen.PassifyImpl(impl, out mvInfo);

+

+        VCExpressionGenerator gen = proverInterface.VCExprGen;

+        var exprGen = proverInterface.Context.ExprGen;

+        var translator = proverInterface.Context.BoogieExprTranslator;

+

+        // add a boolean variable at each call site

+        vcgen.InstrumentCallSites(impl);

+

+        // typecheck

+        var tc = new TypecheckingContext(null);

+        impl.Typecheck(tc);

+

+        ///////////////////

+        // Generate the VC

+        ///////////////////

+

+        // block -> bool variable

+        blockToControlVar = new Dictionary<Block, VCExprVar>();

+        foreach (var b in impl.Blocks)

+            blockToControlVar.Add(b, gen.Variable(b.Label + "_holds", Bpl.Type.Bool));

+

+        vcexpr = VCExpressionGenerator.True;

+        foreach (var b in impl.Blocks)

+        {

+            // conjoin all assume cmds

+            VCExpr c = VCExpressionGenerator.True;

+            foreach (var cmd in b.Cmds)

+            {

+                var acmd = cmd as AssumeCmd;

+                if (acmd == null)

+                {

+                    Debug.Assert(cmd is AssertCmd && (cmd as AssertCmd).Expr is LiteralExpr &&

+                        ((cmd as AssertCmd).Expr as LiteralExpr).IsTrue);

+                    continue;

+                }

+                var expr = translator.Translate(acmd.Expr);

+                // Label the assume if it is a procedure call

+                NAryExpr naryExpr = acmd.Expr as NAryExpr;

+                if (naryExpr != null && naryExpr.Fun is FunctionCall)

+                {

+                    var id = acmd.UniqueId;

+                    label2absy[id] = acmd;

+                    expr = gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), expr);

+                }

+

+                c = gen.AndSimp(c, expr);

+            }

+            vcexpr = gen.AndSimp(vcexpr, gen.Eq(blockToControlVar[b], c));

+

+            // block implies a disjunction of successors

+            Debug.Assert(!(b.TransferCmd is ReturnExprCmd), "Not supported");

+            var gc = b.TransferCmd as GotoCmd;

+            if (gc != null)

+            {

+                VCExpr succ = VCExpressionGenerator.False;

+                foreach (var sb in gc.labelTargets)

+                    succ = gen.OrSimp(succ, blockToControlVar[sb]);

+                vcexpr = gen.AndSimp(vcexpr, succ);

+            }

+            else

+            {

+                // nothing to do

+            }

+        }

+        // assert start block

+        vcexpr = gen.AndSimp(vcexpr, blockToControlVar[impl.Blocks[0]]);

+

+        //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);

+        // Collect other information

+        callSites = vcgen.CollectCallSites(impl);

+        recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);

+

+        // record interface variables

+        privateExprVars = new List<VCExprVar>();

+        foreach (Variable v in impl.LocVars)

+        {

+            privateExprVars.Add(translator.LookupVariable(v));

+        }

+        foreach (Variable v in impl.OutParams)

+        {

+            privateExprVars.Add(translator.LookupVariable(v));

+        }

+        privateExprVars.AddRange(blockToControlVar.Values);

+

+        interfaceExprVars = new List<VCExprVar>();

+        foreach (Variable v in program.GlobalVariables)

+        {

+            interfaceExprVars.Add(translator.LookupVariable(v));

+        }

+        foreach (Variable v in impl.InParams)

+        {

+            interfaceExprVars.Add(translator.LookupVariable(v));

+        }

+        foreach (Variable v in outputVariables)

+        {

+            interfaceExprVars.Add(translator.LookupVariable(v));

+        }

+    }

+

     public void GenerateVC() {

       if (initialized) return;

+      if (CommandLineOptions.Clo.SIBoolControlVC)

+      {

+          GenerateVCBoolControl();

+          initialized = true;

+          return;

+      }

       List<Variable> outputVariables = new List<Variable>();

       List<Expr> assertConjuncts = new List<Expr>();

       foreach (Variable v in impl.OutParams) {

@@ -464,9 +605,8 @@ namespace VC {
     // Used inside PassifyImpl

     protected override void addExitAssert(string implName, Block exitBlock) {

       if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {

-        AssertCmd exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd;

-        Contract.Assert(exitAssertCmd != null);

-        exitBlock.Cmds.Add(exitAssertCmd);

+        var exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd;

+        if(exitAssertCmd != null) exitBlock.Cmds.Add(exitAssertCmd);

       }

     }

 

@@ -1075,7 +1215,12 @@ namespace VC {
       reporter.SetCandidateHandler(calls);

       calls.id2VC.Add(0, vc);

       calls.extraRecursion = extraRecBound;

-

+      if (CommandLineOptions.Clo.SIBoolControlVC)

+      {

+          calls.candiate2block2controlVar.Add(0, new Dictionary<Block, VCExpr>());

+          implName2StratifiedInliningInfo[impl.Name].blockToControlVar.Iter(tup =>

+              calls.candiate2block2controlVar[0].Add(tup.Key, tup.Value));

+      }

       // Identify summary candidates: Match ensure clauses with the appropriate call site

       if (useSummary) calls.matchSummaries();

 

@@ -1468,6 +1613,16 @@ namespace VC {
           prover.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);

           substExistsDict.Add(v, prover.VCExprGen.Variable(newName, v.Type));

         }

+        if (CommandLineOptions.Clo.SIBoolControlVC)

+        {

+            // record the mapping for control booleans (for tracing the path later)

+            calls.candiate2block2controlVar[id] = new Dictionary<Block, VCExpr>();

+            foreach (var tup in info.blockToControlVar)

+            {

+                calls.candiate2block2controlVar[id].Add(tup.Key,

+                    substExistsDict[tup.Value]);

+            }

+        }

         if (CommandLineOptions.Clo.ModelViewFile != null) {

           SaveSubstitution(vState, id, substForallDict, substExistsDict);

         }

@@ -1550,6 +1705,8 @@ namespace VC {
       public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;

       public Dictionary<int, VCExpr> id2VC;

       public Dictionary<string/*!*/, int>/*!*/ label2Id;

+      // candidate to block to Bool Control variable

+      public Dictionary<int, Dictionary<Block, VCExpr>> candiate2block2controlVar;

       // Stores the candidate from which this one originated

       public Dictionary<int, int> candidateParent;

       // Mapping from candidate Id to the "si_unique_call" id that led to 

@@ -1630,6 +1787,7 @@ namespace VC {
         recentlyAddedCandidates = new HashSet<int>();

         argExprMap = new Dictionary<int, VCExpr>();

         recordExpr2Var = new Dictionary<BoogieCallExpr, VCExpr>();

+        candiate2block2controlVar = new Dictionary<int, Dictionary<Block, VCExpr>>();

 

         forcedCandidates = new HashSet<int>();

         extraRecursion = new Dictionary<string, int>();

@@ -1884,6 +2042,8 @@ namespace VC {
             int candidateId = GetNewId(callExpr);

             boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;

             candidateParent[candidateId] = currInlineCount;

+            candiate2block2controlVar[candidateId] = new Dictionary<Block, VCExpr>();

+

             string label = GetLabel(candidateId);

             var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1);

             if (unique_call_id != -1)

@@ -2049,7 +2209,6 @@ namespace VC {
       FCallHandler calls;

       StratifiedInliningInfo mainInfo;

       StratifiedVC mainVC;

-      Counterexample CexTrace;

 

       public bool underapproximationMode;

       public List<int> candidatesToExpand;

@@ -2079,7 +2238,6 @@ namespace VC {
         this.underapproximationMode = false;

         this.calls = null;

         this.candidatesToExpand = new List<int>();

-        this.CexTrace = null;

       }

 

       public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,

@@ -2095,7 +2253,6 @@ namespace VC {
         this.mainVC = mainVC;

         this.underapproximationMode = false;

         this.candidatesToExpand = new List<int>();

-        this.CexTrace = null;

       }

 

       public void SetCandidateHandler(FCallHandler calls) {

@@ -2256,25 +2413,56 @@ namespace VC {
 

         Hashtable traceNodes = new Hashtable();

 

-        foreach (string s in labels) {

-          Contract.Assert(s != null);

-          var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId);

-

-          if (absylabel == null) continue;

-

-          Absy absy;

-

-          if (candidateId == 0) {

-            absy = Label2Absy(absylabel);

-          }

-          else {

-            absy = Label2Absy(procImpl.Name, absylabel);

-          }

-

-          if (traceNodes.ContainsKey(absy))

-            System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");

-          else

-            traceNodes.Add(absy, null);

+        if (!CommandLineOptions.Clo.SIBoolControlVC)

+        {

+            foreach (string s in labels)

+            {

+                Contract.Assert(s != null);

+                var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId);

+

+                if (absylabel == null) continue;

+

+                Absy absy;

+

+                if (candidateId == 0)

+                {

+                    absy = Label2Absy(absylabel);

+                }

+                else

+                {

+                    absy = Label2Absy(procImpl.Name, absylabel);

+                }

+

+                if (traceNodes.ContainsKey(absy))

+                    System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");

+                else

+                    traceNodes.Add(absy, null);

+            }

+        }

+        else

+        {

+            Debug.Assert(CommandLineOptions.Clo.UseProverEvaluate, "Must use prover evaluate option with boolControlVC");

+            var block = procImpl.Blocks[0];

+            traceNodes.Add(block, null);

+            while (true)

+            {

+                var gc = block.TransferCmd as GotoCmd;

+                if (gc == null) break;

+                Block next = null;

+                foreach (var succ in gc.labelTargets)

+                {

+                    var succtaken = (bool) theoremProver.Evaluate(calls.candiate2block2controlVar[candidateId][succ]);

+                    if (succtaken)

+                    {

+                        next = succ;

+                        traceNodes.Add(succ, null);

+                        break;

+                    }

+                }

+                Debug.Assert(next != null, "Must find a successor");

+                Debug.Assert(traceNodes.ContainsKey(next), "CFG cannot be cyclic");

+                block = next;

+            }

         }

 

         List<Block> trace = new List<Block>();

@@ -2307,10 +2495,14 @@ namespace VC {
             Cmd cmd = cce.NonNull(cmds[i]);

 

             // Skip if 'cmd' not contained in the trace or not an assert

-            if (cmd is AssertCmd && traceNodes.Contains(cmd)) {

-              Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context);

-              newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

-              return newCounterexample;

+            if ((cmd is AssertCmd && traceNodes.Contains(cmd)) ||

+                 (cmd is AssumeCmd && QKeyValue.FindBoolAttribute((cmd as AssumeCmd).Attributes, "exitAssert")))

+            {

+                var acmd = cmd as AssertCmd;

+                if (acmd == null) { acmd = new AssertCmd(Token.NoToken, Expr.True); }

+                Counterexample newCounterexample = AssertCmdToCounterexample(acmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context);

+                newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

+                return newCounterexample;

             }

 

             // Counterexample generation for inlined procedures