summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Ally Donaldson <unknown>2015-01-14 13:51:45 +0000
committerGravatar Ally Donaldson <unknown>2015-01-14 13:51:45 +0000
commitfe461a22df4cade95f1ff30f8e19ef8a54ce8b41 (patch)
treeb329aa8fbf678fed98c9e510643ca72d10082a7c
parentd16fd70f1678b0e3f1683ba0c8b93f21d3d88cc4 (diff)
Fix related to limitations in CVC4 model parsing
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs2
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);