diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-09-23 15:31:51 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-09-23 15:31:51 -0700 |
| commit | bfa90b9c75e1253924e61960b3afe2b4f4d1d63c (patch) | |
| tree | 8b17a69e2bc848d7e75b2b73d14c77fbea934a98 /Source/ModelViewer/VccProvider.cs | |
| parent | 14485cfa01cc2955d7a9cd3a41bead4c2ec4188d (diff) | |
Better support for map types
Diffstat (limited to 'Source/ModelViewer/VccProvider.cs')
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 3 |
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);
|