diff options
| author |  akashlal <unknown> | 2011-03-18 01:21:06 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2011-03-18 01:21:06 +0000 |
| commit | b05011878c6ec3aa713d5f5c4ece5825132ce2ca (patch) | |
| tree | edf0b9711ccad6c4de48d4d81e655ce7586745c5 /Source/VCGeneration | |
| parent | df0fd34ecd8e381083e6c0839dbbb9944803a28c (diff) | |
minor fix with loopy counterexample generation
Diffstat (limited to 'Source/VCGeneration')
| -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)
|