From fe461a22df4cade95f1ff30f8e19ef8a54ce8b41 Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Wed, 14 Jan 2015 13:51:45 +0000
Subject: Fix related to limitations in CVC4 model parsing

---
 Source/VCGeneration/ConditionGeneration.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/VCGeneration')

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);
-- 
cgit v1.2.3