fixed bug

Source/Core/Monomorphization.cs

@@ -1830,6 +1830,13 @@ public static string MkInstanceName(string name, List<Type> actualTypeParams)
     public Type LookupType(Type type)
     {
       type = TypeProxy.FollowProxy(type.Expanded);
+      if (type is MapType mapType && mapType.FreeVariables.Count == 0)
+      {
+        var instantiatedTypeArguments = mapType.Arguments.Select(x => LookupType(x)).ToList();
+        var instantiatedTypeResult = LookupType(mapType.Result);
+        return new MapType(Token.NoToken, new List<TypeVariable>(mapType.TypeParameters), instantiatedTypeArguments,
+          instantiatedTypeResult);
+      }
       if (type is CtorType ctorType && ctorType.FreeVariables.Count == 0 &&
           MonomorphismChecker.DoesTypeCtorDeclNeedMonomorphization(ctorType.Decl))
       {

Test/monomorphize/type-translation-bug.bpl

@@ -0,0 +1,19 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure {:inline 1} Copy<T>(v: T) returns (copy_v: T)
+{
+  copy_v := v;
+}
+
+type Value;
+type Round;
+datatype Option<T> { None(), Some(t: T) }
+
+var decision: [Round]Option Value;
+procedure Foo()
+modifies decision;
+{
+  call decision := Copy((lambda r: Round :: None()));
+  assert decision == (lambda r: Round :: None());
+}

Test/monomorphize/type-translation-bug.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors