From 3d2bdaf737810142e8685296813562e7e29c9952 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 26 Oct 2011 16:52:40 -0700
Subject: BVD: fixed two basic but damning problems with the Dafny provider,
 and elided some temporary variables

---
 Source/ModelViewer/DafnyProvider.cs | 4 ++++
 Source/ModelViewer/Namer.cs         | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'Source/ModelViewer')

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 32912113..328bbb26 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -92,9 +92,13 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     {
       if (name.StartsWith("$")) // this covers $Heap and $_Frame and $nw...
         return null;
+      if (name.Contains("##"))  // a temporary variable of the translation
+        return null;
+#if SOMETIME_AGAIN
       var hash = name.IndexOf('#');
       if (0 < hash)
         return name.Substring(0, hash);
+#endif
       return name;
     }
 
diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index fce9522d..1006c658 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -530,7 +530,7 @@ namespace Microsoft.Boogie.ModelViewer
 
     protected virtual string Format()
     {
-      if (args.Length == 0)
+      if (args == null || args.Length == 0)
         return format;
 
       var res = new StringBuilder(format.Length);
-- 
cgit v1.2.3