minor fix with loopy counterexample generation

1 files changed, 1 insertions, 0 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index f3517d60..f508fb3d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2413,6 +2413,7 @@ namespace VC {
         Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)

     {

         Contract.Requires(currProc != null);

+        if (cexInfo.counterexample == null) return cexInfo;

 

         var cex = cexInfo.counterexample;

         // Go through all blocks in the trace, map them back to blocks in the original program (if there is one)