diff options
| -rw-r--r-- | Source/VCGeneration/VC.cs | 1 |
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)
|