From bfa90b9c75e1253924e61960b3afe2b4f4d1d63c Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Fri, 23 Sep 2011 15:31:51 -0700
Subject: Better support for map types

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

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 9f5730ce..a9203e6b 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -618,6 +618,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var fname = tpl.Func.Name;
 
         if (tpl.Args.Length == 2 && tpl.Args[0] == element && fname.StartsWith("$select.$map_t")) {
+          var mt = model.TryGetFunc("MT#" + fname);
+          if (mt != null && mt.Arity == 0)
+            return mt.GetConstant();
           var t1 = GuessType(tpl.Args[1]);
           var t2 = GuessType(tpl.Result);
           var t = f_map_t.TryEval(t1, t2);
-- 
cgit v1.2.3