summaryrefslogtreecommitdiff
path: root/Source/ModelViewer
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-09-23 15:31:51 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-09-23 15:31:51 -0700
commitbfa90b9c75e1253924e61960b3afe2b4f4d1d63c (patch)
tree8b17a69e2bc848d7e75b2b73d14c77fbea934a98 /Source/ModelViewer
parent14485cfa01cc2955d7a9cd3a41bead4c2ec4188d (diff)
Better support for map types
Diffstat (limited to 'Source/ModelViewer')
-rw-r--r--Source/ModelViewer/VccProvider.cs3
1 files changed, 3 insertions, 0 deletions
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);