diff options
| author |  Ally Donaldson <unknown> | 2015-01-14 13:51:45 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2015-01-14 13:51:45 +0000 |
| commit | fe461a22df4cade95f1ff30f8e19ef8a54ce8b41 (patch) | |
| tree | b329aa8fbf678fed98c9e510643ca72d10082a7c | |
| parent | d16fd70f1678b0e3f1683ba0c8b93f21d3d88cc4 (diff) | |
Fix related to limitations in CVC4 model parsing
| -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);
|