diff options
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 3311e6b4..454a2f30 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -241,7 +241,7 @@ namespace Microsoft.Boogie { ApplyRedirections(m);
var mvstates = m.TryGetFunc("$mv_state");
- if (MvInfo == null || mvstates == null)
+ if (MvInfo == null || mvstates == null || (mvstates.Arity == 1 && mvstates.Apps.Count() == 0))
return;
Contract.Assert(mvstates.Arity == 2);
|