From cfbfbb0229db8f71c4fb21c0f4c7cfb60debd507 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Wed, 26 Oct 2011 11:14:25 -0700
Subject: VCC: Detect wrong model files

---
 Source/ModelViewer/VccProvider.cs | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Source/ModelViewer')

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index b5ba6c22..ede520cb 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -135,7 +135,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         sn.SetupVars();
         states.Add(sn);
       }
+
       var allStates = states.ToArray();
+      if (allStates.Length == 1 && allStates[0].vars.Count == 0) {
+        throw new Exception("This VCC model doesn't contain any variables. Was it saved with the -bvd option?");
+      }
       states.Clear();
       var i = 0;
       while (i < allStates.Length) {
-- 
cgit v1.2.3