diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
index a769a8b3ce0..f379556919a 100644
--- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
@@ -2874,6 +2874,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -2884,6 +2885,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.EqCommon: {
@@ -3015,7 +3017,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -3037,8 +3039,14 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
           ConvertFromChar(e.E, wr, inLetExprBody, wStmts);
           wr.Write(", BigInteger.One)");
         } else if (e.ToType.IsCharType) {
-          wr.Write($"({CharTypeName})");
-          TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+          if (UnicodeCharEnabled) {
+            wr.Write($"new {CharTypeName}((int)");
+            TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+            wr.Write(")");
+          } else {
+            wr.Write($"({CharTypeName})");
+            TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+          }
         } else {
           // (int or bv or char) -> (int or bv or ORDINAL)
           var fromNative = AsNativeType(e.E.Type);
diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
index 3634c831915..d268d997987 100644
--- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
+++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
@@ -2053,6 +2053,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -2063,6 +2064,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:
diff --git a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
index ab4330d07b9..a949d5d4802 100644
--- a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
+++ b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
@@ -529,6 +529,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -539,6 +540,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:
diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
index 564cf40c0f8..238e26fe57e 100644
--- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
+++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
@@ -3114,6 +3114,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -3124,6 +3125,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.BitwiseAnd:
@@ -3368,7 +3370,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -3659,7 +3661,7 @@ protected override void EmitCollectionDisplay(CollectionType ct, IToken tok, Lis
           wr.Write("_dafny.SeqOf");
         }
       }
-      TrExprList(elements, wr, inLetExprBody, wStmts, type: ct.TypeArgs[0]);
+      TrExprList(elements, wr, inLetExprBody, wStmts, typeAt: _ => ct.TypeArgs[0]);
     }
 
     protected override void EmitMapDisplay(MapType mt, IToken tok, List<ExpressionPair> elements,
diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
index 1d110cd315f..23cf4246bdc 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -222,7 +222,7 @@ protected override void EmitSeqSelect(AssignStmt s0, List<Type> tupleTypeArgsLis
       var lhs = (SeqSelectExpr)s0.Lhs;
       ConcreteSyntaxTree wColl, wIndex, wValue;
       EmitIndexCollectionUpdate(lhs.Seq.Type, out wColl, out wIndex, out wValue, wr, nativeIndex: true);
-      var wCoerce = EmitCoercionIfNecessary(from: null, to: lhs.Seq.Type, tok: s0.Tok, wr: wColl);
+      var wCoerce = EmitCoercionIfNecessary(from: NativeObjectType, to: lhs.Seq.Type, tok: s0.Tok, wr: wColl);
       wCoerce.Write($"({TypeName(lhs.Seq.Type.NormalizeExpand(), wCoerce, s0.Tok)})");
       EmitTupleSelect(tup, 0, wCoerce);
       wColl.Write(")");
@@ -961,7 +961,11 @@ private void EmitTypeMethod(TopLevelDecl/*?*/ enclosingTypeDecl, string typeName
             if (targetType.IsBoolType) {
               typeDescriptorExpr = $"{DafnyTypeDescriptor}.booleanWithDefault({w ?? "false"})";
             } else if (targetType.IsCharType) {
-              typeDescriptorExpr = $"{DafnyTypeDescriptor}.charWithDefault({w ?? CharType.DefaultValueAsString})";
+              if (UnicodeCharEnabled) {
+                typeDescriptorExpr = $"{DafnyTypeDescriptor}.unicodeCharWithDefault((int){w ?? CharType.DefaultValueAsString})";
+              } else {
+                typeDescriptorExpr = $"{DafnyTypeDescriptor}.charWithDefault({w ?? CharType.DefaultValueAsString})";
+              }
             } else if (targetType.IsTypeParameter) {
               typeDescriptorExpr = TypeDescriptor(targetType, wr, enclosingTypeDecl.tok);
             } else {
@@ -1160,6 +1164,8 @@ private string GetBoxedNativeTypeName(NativeType nt) {
     // Note the (semantically iffy) distinction between a *primitive type*,
     // being one of the eight Java primitive types, and a NativeType, which can
     // only be one of the integer types.
+    // Note also that in --unicode-char mode, we have our own CodePoint boxing type
+    // that boxes int values that are actually Dafny char values.
     private bool IsJavaPrimitiveType(Type type) {
       return type.IsBoolType || type.IsCharType || AsNativeType(type) != null;
     }
@@ -1328,7 +1334,11 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
         GetSpecialFieldInfo(sf.SpecialId, sf.IdParam, objType, out var compiledName, out _, out _);
         if (compiledName.Length != 0) {
           if (member.EnclosingClass is DatatypeDecl) {
-            return SuffixLvalue(obj, $".{compiledName}()");
+            if (member.EnclosingClass is TupleTypeDecl && sf.Type.Subst(typeMap).IsCharType && UnicodeCharEnabled) {
+              return SuffixLvalue(obj, $".{compiledName}().value()");
+            } else {
+              return SuffixLvalue(obj, $".{compiledName}()");
+            }
           } else {
             return SuffixLvalue(obj, $".{compiledName}");
           }
@@ -1339,11 +1349,15 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
       } else if (member is Function fn) {
         var wr = new ConcreteSyntaxTree();
         EmitNameAndActualTypeArgs(IdName(member), TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, member, false)), member.tok, wr);
-        if (typeArgs.Count == 0 && additionalCustomParameter == null) {
+        var needsEtaConversion = typeArgs.Any()
+               || additionalCustomParameter != null
+               || (UnicodeCharEnabled &&
+                  (fn.ResultType.IsCharType || fn.Formals.Any(f => f.Type.IsCharType)));
+        if (!needsEtaConversion) {
           var nameAndTypeArgs = wr.ToString();
           return SuffixLvalue(obj, $"::{nameAndTypeArgs}");
         } else {
-          // We need an eta conversion to adjust for the difference in arity.
+          // We need an eta conversion to adjust for the difference in arity or coerce inputs/outputs.
           // (T0 a0, T1 a1, ...) -> obj.F(rtd0, rtd1, ..., additionalCustomParameter, a0, a1, ...)
           wr.Write("(");
           var sep = "";
@@ -1360,14 +1374,22 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
               var name = idGenerator.FreshId("_eta");
               var ty = arg.Type.Subst(typeMap);
               prefixWr.Write($"{prefixSep}{BoxedTypeName(ty, prefixWr, arg.tok)} {name}");
-              wr.Write("{0}{1}", sep, name);
+              wr.Write(sep);
+              var coercedWr = EmitCoercionIfNecessary(NativeObjectType, ty, arg.tok, wr);
+              coercedWr.Write(name);
               sep = ", ";
               prefixSep = ", ";
             }
           }
           prefixWr.Write(") -> ");
           wr.Write(")");
-          return EnclosedLvalue(prefixWr.ToString(), obj, $".{wr.ToString()}");
+
+          if (fn.ResultType.IsCharType && UnicodeCharEnabled) {
+            prefixWr.Write("dafny.CodePoint.valueOf(");
+            wr.Write(")");
+          }
+
+          return EnclosedLvalue(prefixWr.ToString(), obj, $".{wr}");
         }
       } else {
         var field = (Field)member;
@@ -1610,7 +1632,8 @@ protected override void EmitIndexCollectionUpdate(Expression source, Expression
         TrExpr(index, wr, inLetExprBody, wStmts);
       }
       wr.Write(", ");
-      TrExpr(value, wr, inLetExprBody, wStmts);
+      var coercedWr = EmitCoercionIfNecessary(value.Type, NativeObjectType, Token.NoToken, wr);
+      TrExpr(value, coercedWr, inLetExprBody, wStmts);
       wr.Write(")");
     }
 
@@ -2497,6 +2520,9 @@ void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type> typeArgs,
 
     protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, IToken tok, List<string> inNames,
         Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, bool untyped = false) {
+      // TODO: there may be an opportunity to share code with CreateIIFE,
+      // which may be worth it given all the necessary coercions.
+
       if (inTypes.Count != 1) {
         functions.Add(inTypes.Count);
       }
@@ -2504,9 +2530,18 @@ protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, IToken to
       if (!untyped) {
         wr.Write("({0}<{1}{2}>)", DafnyFunctionIface(inTypes.Count), Util.Comma("", inTypes, t => BoxedTypeName(t, wr, tok) + ", "), BoxedTypeName(resultType, wr, tok));
       }
-      wr.Write($"({inNames.Comma(nm => nm)}) ->");
+      var boxedInNames = inNames.Select(inName => ProtectedFreshId(inName + "_boxed")).ToList();
+      wr.Write($"({boxedInNames.Comma(nm => nm)}) ->");
       var w = wr.NewExprBlock("");
       wr.Write(")");
+
+      for (var i = 0; i < inNames.Count; i++) {
+        w.Write($"{TypeName(inTypes[i], w, tok)} {inNames[i]} = ");
+        var coercedW = EmitCoercionIfNecessary(NativeObjectType, inTypes[i], tok, w);
+        coercedW.Write(boxedInNames[i]);
+        w.WriteLine(";");
+      }
+
       return w;
     }
 
@@ -2559,7 +2594,7 @@ private string HelperClass(NativeType nt) {
     protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, Expression e0, Expression e1, IToken tok,
       Type resultType, out string opString,
       out string preOpString, out string postOpString, out string callString, out string staticCallString,
-      out bool reverseArguments, out bool truncateResult, out bool convertE1_to_int, ConcreteSyntaxTree errorWr) {
+      out bool reverseArguments, out bool truncateResult, out bool convertE1_to_int, out bool coerceE1, ConcreteSyntaxTree errorWr) {
       opString = null;
       preOpString = "";
       postOpString = "";
@@ -2568,6 +2603,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, Expression e0
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string opS,
         out string postOpS, out string callS) {
@@ -2763,6 +2799,7 @@ void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string
         case BinaryExpr.ResolvedOpcode.InMap:
           callString = $"<{BoxedTypeName(e0.Type, errorWr, tok)}>contains";
           reverseArguments = true;
+          coerceE1 = true;
           break;
 
         case BinaryExpr.ResolvedOpcode.Union:
@@ -2802,10 +2839,11 @@ void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string
         case BinaryExpr.ResolvedOpcode.InSeq:
           callString = "contains";
           reverseArguments = true;
+          coerceE1 = true;
           break;
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -2948,7 +2986,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
       if (xType is BoolType) {
         return "false";
       } else if (xType is CharType) {
-        return UnicodeCharEnabled ? $"dafny.CodePoint.valueOf({CharType.DefaultValueAsString})" : CharType.DefaultValueAsString;
+        return UnicodeCharEnabled ? $"((int){CharType.DefaultValueAsString})" : CharType.DefaultValueAsString;
       } else if (xType is IntType || xType is BigOrdinalType) {
         return "java.math.BigInteger.ZERO";
       } else if (xType is RealType) {
@@ -3051,7 +3089,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
           return $"({s}{typeargs})null";
         }
         var relevantTypeArgs = UsedTypeParameters(dt, udt.TypeArgs);
-        return $"{s}.{typeargs}Default({Util.Comma(relevantTypeArgs, ta => DefaultValue(ta.Actual, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors))})";
+        return $"{s}.{typeargs}Default({Util.Comma(relevantTypeArgs, ta => DefaultValueCoercedIfNecessary(ta.Actual, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors))})";
       } else {
         Contract.Assert(false);
         throw new cce.UnreachableException(); // unexpected type
@@ -3123,6 +3161,7 @@ protected override void EmitDestructor(string source, Formal dtor, int formalNon
       if (ctor.EnclosingDatatype is TupleTypeDecl tupleTypeDecl) {
         Contract.Assert(tupleTypeDecl.NonGhostDims != 1); // such a tuple is an erasable-wrapper type, handled above
         dtorName = $"dtor__{dtor.NameForCompilation}()";
+        wr = EmitCoercionIfNecessary(NativeObjectType, bvType, dtor.tok, wr);
       } else {
         dtorName = FieldName(dtor, formalNonGhostIndex);
       }
@@ -3255,9 +3294,19 @@ protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
     protected override ConcreteSyntaxTree CreateForeachLoop(
       string tmpVarName, Type collectionElementType, IToken tok, out ConcreteSyntaxTree collectionWriter, ConcreteSyntaxTree wr) {
 
-      wr.Write("for ({1} {0} : ", tmpVarName, TypeName(collectionElementType, wr, tok));
+      // We may have to coerce from the boxed type used in collections
+      var needsCoercion = IsCoercionNecessary(NativeObjectType, collectionElementType);
+      var boxedType = BoxedTypeName(collectionElementType, wr, tok);
+      var loopVarName = needsCoercion ? ProtectedFreshId(tmpVarName + "_boxed") : tmpVarName;
+      wr.Write($"for ({boxedType} {loopVarName} : ");
       collectionWriter = wr.Fork();
       var wwr = wr.NewBlock(")");
+      if (needsCoercion) {
+        wwr.Write($"{TypeName(collectionElementType, wr, tok)} {tmpVarName} = ");
+        var coercedWwr = EmitCoercionIfNecessary(NativeObjectType, collectionElementType, tok, wwr);
+        coercedWwr.Write(loopVarName);
+        wwr.WriteLine(";");
+      }
       return wwr;
     }
 
@@ -3464,7 +3513,7 @@ protected override void EmitNewArray(Type elementType, IToken tok, List<string>
         wBareArray = wr.Fork();
         wr.Write(")");
         if (mustInitialize) {
-          wr.Write($".fillThenReturn({DefaultValue(elementType, wr, tok, true)})");
+          wr.Write($".fillThenReturn({DefaultValueCoercedIfNecessary(elementType, wr, tok, true)})");
         }
       } else {
         wr.Write($"({ArrayTypeName(elementType, dimensions.Count, wr, tok, false)}) ");
@@ -3473,7 +3522,7 @@ protected override void EmitNewArray(Type elementType, IToken tok, List<string>
         }
         wBareArray = wr.Fork();
         if (mustInitialize) {
-          wr.Write($", {DefaultValue(elementType, wr, tok, true)})");
+          wr.Write($", {DefaultValueCoercedIfNecessary(elementType, wr, tok, true)})");
         }
       }
 
@@ -3588,9 +3637,10 @@ protected override void EmitTupleSelect(string prefix, int i, ConcreteSyntaxTree
     }
 
     protected override void EmitApplyExpr(Type functionType, IToken tok, Expression function, List<Expression> arguments, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      wr = EmitCoercionIfNecessary(NativeObjectType, functionType.AsArrowType.Result, tok, wr);
       TrParenExpr(function, wr, inLetExprBody, wStmts);
       wr.Write(".apply");
-      TrExprList(arguments, wr, inLetExprBody, wStmts);
+      TrExprList(arguments, wr, inLetExprBody, wStmts, typeAt: _ => NativeObjectType);
     }
 
     protected override bool NeedsCastFromTypeParameter => true;
@@ -3610,7 +3660,7 @@ protected override bool IsCoercionNecessary(Type/*?*/ from, Type/*?*/ to) {
         return true;
       }
 
-      if (UnicodeCharEnabled && ((IsObjectType(from) && to.IsCharType) || (from.IsCharType && IsObjectType(to)))) {
+      if (UnicodeCharEnabled && ((IsNativeObjectType(from) && to.IsCharType) || (from.IsCharType && IsNativeObjectType(to)))) {
         // Need to box from int to CodePoint, or unbox from CodePoint to int
         return true;
       }
@@ -3642,7 +3692,7 @@ protected override Type TypeForCoercion(Type type) {
     // (see for example https://github.com/dafny-lang/dafny/issues/2989).
     private static readonly Type NativeObjectType = null;
 
-    private bool IsObjectType(Type type) {
+    private bool IsNativeObjectType(Type type) {
       return type == NativeObjectType || type.IsTypeParameter;
     }
 
@@ -3653,15 +3703,15 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
       if (UnicodeCharEnabled) {
         // Need to box from int to CodePoint, or unbox from CodePoint to int
 
-        if (IsObjectType(from) && to is { IsCharType: true }) {
-          wr.Write($"((dafny.CodePoint)(");
+        if (IsNativeObjectType(from) && to is { IsCharType: true }) {
+          wr.Write("((dafny.CodePoint)(");
           var w = wr.Fork();
           wr.Write(")).value()");
           return w;
         }
 
-        if (from is { IsCharType: true } && IsObjectType(to)) {
-          wr.Write($"dafny.CodePoint.valueOf(");
+        if (from is { IsCharType: true } && IsNativeObjectType(to)) {
+          wr.Write("dafny.CodePoint.valueOf(");
           var w = wr.Fork();
           wr.Write(")");
           return w;
@@ -3967,11 +4017,24 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
 
     protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok,
       ConcreteSyntaxTree wr, ref ConcreteSyntaxTree wStmts, out ConcreteSyntaxTree wrRhs, out ConcreteSyntaxTree wrBody) {
-      wr.Write("({0})", TypeName(bodyType, wr, bodyTok));
-      wr.Write("{0}.<{1}, {2}>Let(", DafnyHelpersClass, BoxedTypeName(bvType, wr, bvTok), BoxedTypeName(bodyType, wr, bodyTok));
+      wr = EmitCoercionIfNecessary(NativeObjectType, bodyType, bvTok, wr);
+      var boxedBvType = BoxedTypeName(bvType, wr, bvTok);
+      wr.Write("{0}.<{1}, {2}>Let(", DafnyHelpersClass, boxedBvType, BoxedTypeName(bodyType, wr, bodyTok));
       wrRhs = wr.Fork();
-      wr.Write($", {bvName} -> ");
-      wrBody = wr.Fork();
+      wrRhs = EmitCoercionIfNecessary(bvType, NativeObjectType, bvTok, wrRhs);
+
+      var boxedBvName = idGenerator.FreshId("boxed");
+      wr.Write($", {boxedBvName} ->");
+      var wrBodyWithCoercion = wr.NewBlock();
+      wrBodyWithCoercion.Write($"{TypeName(bvType, wr, bvTok)} {bvName} = ");
+      var wrUnboxed = EmitCoercionIfNecessary(NativeObjectType, bvType, bvTok, wrBodyWithCoercion.Fork());
+      wrUnboxed.Write(boxedBvName);
+      wrBodyWithCoercion.WriteLine(";");
+
+      wrBodyWithCoercion.Write("return ");
+      wrBody = wrBodyWithCoercion.Fork();
+      wrBody = EmitCoercionIfNecessary(bodyType, NativeObjectType, bodyTok, wrBody);
+      wrBodyWithCoercion.WriteLine(";");
       wr.Write(")");
     }
 
diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
index bdad2798865..0c71b658b31 100644
--- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
+++ b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
@@ -1977,6 +1977,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -1987,6 +1988,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:
@@ -2246,7 +2248,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs
index 2a2a3ab0795..477c2c237e4 100644
--- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs
+++ b/Source/DafnyCore/Compilers/Python/Compiler-python.cs
@@ -1427,6 +1427,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -1437,6 +1438,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.And:
@@ -1560,7 +1562,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
             out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments,
-            out truncateResult, out convertE1_to_int,
+            out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
index 98fc12f4c0f..5c497aefc1d 100644
--- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs
+++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
@@ -1168,6 +1168,7 @@ protected virtual void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       // This default implementation does not handle all cases. It handles some cases that look the same
@@ -1181,6 +1182,7 @@ protected virtual void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       BinaryExpr.ResolvedOpcode dualOp = BinaryExpr.ResolvedOpcode.Add;  // NOTE! "Add" is used to say "there is no dual op"
       BinaryExpr.ResolvedOpcode negatedOp = BinaryExpr.ResolvedOpcode.Add;  // NOTE! "Add" is used to say "there is no negated op"
@@ -1251,13 +1253,13 @@ protected virtual void CompileBinOp(BinaryExpr.ResolvedOpcode op,
         Contract.Assert(negatedOp == BinaryExpr.ResolvedOpcode.Add);
         CompileBinOp(dualOp,
           e1, e0, tok, resultType,
-          out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+          out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
           errorWr);
         reverseArguments = !reverseArguments;
       } else if (negatedOp != BinaryExpr.ResolvedOpcode.Add) {  // remember from above that Add stands for "there is no negated op"
         CompileBinOp(negatedOp,
           e0, e1, tok, resultType,
-          out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+          out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
           errorWr);
         preOpString = "!" + preOpString;
       }
@@ -2899,6 +2901,15 @@ bool HasGhostGroundingCtor(Type ty) {
       return TypeInitializationValue(simplifiedType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
     }
 
+    protected string DefaultValueCoercedIfNecessary(Type type, ConcreteSyntaxTree wr, IToken tok,
+      bool constructTypeParameterDefaultsFromTypeDescriptors = false) {
+
+      var resultWr = new ConcreteSyntaxTree();
+      var coercedWr = EmitCoercionIfNecessary(type, TypeForCoercion(type), tok, resultWr);
+      coercedWr.Write(DefaultValue(type, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors));
+      return resultWr.ToString();
+    }
+
     // ----- Stmt ---------------------------------------------------------------------------------
 
     public class CheckHasNoAssumes_Visitor : BottomUpVisitor {
@@ -4316,6 +4327,7 @@ void TrRhsArray(TypeRhs typeRhs, string nw, ConcreteSyntaxTree wr, ConcreteSynta
           w = CreateForLoop(indices[d], bound, w);
         }
         var (wArray, wrRhs) = EmitArrayUpdate(indices, typeRhs.EType, w);
+        wrRhs = EmitCoercionIfNecessary(TypeForCoercion(typeRhs.EType), typeRhs.EType, typeRhs.Tok, wrRhs);
         wrRhs.Write("{0}{1}({2})", init, LambdaExecute, indices.Comma(idx => ArrayIndexToInt(idx)));
         wArray.Write(nw);
         EndStmt(w);
@@ -4701,22 +4713,20 @@ protected void TrParenExpr(Expression expr, ConcreteSyntaxTree wr, bool inLetExp
     /// Before calling TrExprList(exprs), the caller must have spilled the let variables declared in expressions in "exprs".
     /// </summary>
     protected void TrExprList(List<Expression> exprs, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts,
-        Type/*?*/ type = null, bool parens = true) {
+        Func<int, Type> typeAt = null, bool parens = true) {
       Contract.Requires(cce.NonNullElements(exprs));
       if (parens) { wr = wr.ForkInParens(); }
-      string sep = "";
-      foreach (Expression e in exprs) {
-        wr.Write(sep);
+
+      wr.Comma(exprs, (e, index) => {
         ConcreteSyntaxTree w;
-        if (type != null) {
+        if (typeAt != null) {
           w = wr.Fork();
-          w = EmitCoercionIfNecessary(e.Type, type, e.tok, w);
+          w = EmitCoercionIfNecessary(e.Type, typeAt(index), e.tok, w);
         } else {
           w = wr;
         }
         TrExpr(e, w, inLetExprBody, wStmts);
-        sep = ", ";
-      }
+      });
     }
 
     protected virtual void WriteCast(string s, ConcreteSyntaxTree wr) { }
@@ -4963,7 +4973,7 @@ void writeObj(ConcreteSyntaxTree w) {
           wr.Write(sign.ToString());
         } else {
           string opString, preOpString, postOpString, callString, staticCallString;
-          bool reverseArguments, truncateResult, convertE1_to_int;
+          bool reverseArguments, truncateResult, convertE1_to_int, coerceE1;
           CompileBinOp(e.ResolvedOp, e.E0, e.E1, e.tok, expr.Type,
             out opString,
             out preOpString,
@@ -4973,6 +4983,7 @@ void writeObj(ConcreteSyntaxTree w) {
             out reverseArguments,
             out truncateResult,
             out convertE1_to_int,
+            out coerceE1,
             wr);
 
           if (truncateResult && e.Type.IsBitVectorType) {
@@ -4997,6 +5008,9 @@ void writeObj(ConcreteSyntaxTree w) {
             inner.Write(" {0} ", opString);
             if (convertE1_to_int) {
               EmitExprAsNativeInt(e1, inLetExprBody, inner, wStmts);
+            } else if (coerceE1) {
+              var coercedInner = EmitCoercionIfNecessary(e1.Type, TypeForCoercion(e1.Type), e1.tok, inner);
+              TrParenExpr(e1, coercedInner, inLetExprBody, wStmts);
             } else {
               TrParenExpr(e1, inner, inLetExprBody, wStmts);
             }
@@ -5007,6 +5021,9 @@ void writeObj(ConcreteSyntaxTree w) {
             wr.Write(".{0}(", callString);
             if (convertE1_to_int) {
               EmitExprAsNativeInt(e1, inLetExprBody, wr, wStmts);
+            } else if (coerceE1) {
+              var coercedWr = EmitCoercionIfNecessary(e1.Type, TypeForCoercion(e1.Type), e1.tok, wr);
+              TrParenExpr(e1, coercedWr, inLetExprBody, wStmts);
             } else {
               TrParenExpr(e1, wr, inLetExprBody, wStmts);
             }
diff --git a/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs b/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs
index 10608e9947a..82c747e06ac 100644
--- a/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs
+++ b/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs
@@ -73,6 +73,31 @@ public ConcreteSyntaxTree WriteLine() {
       return this;
     }
 
+    public ConcreteSyntaxTree Comma<T>(IEnumerable<T> elements, Action<T> a) {
+      return Comma(", ", elements, (element, _) => a(element));
+    }
+
+    public ConcreteSyntaxTree Comma<T>(IEnumerable<T> elements, Action<T, int> a) {
+      return Comma(", ", elements, a);
+    }
+
+    public ConcreteSyntaxTree Comma<T>(string comma, IEnumerable<T> elements, Action<T> a) {
+      return Comma(comma, elements, (element, _) => a(element));
+    }
+
+    public ConcreteSyntaxTree Comma<T>(string comma, IEnumerable<T> elements, Action<T, int> a) {
+      var sep = "";
+      var index = 0;
+      foreach (var element in elements) {
+        Write(sep);
+        a(element, index);
+        sep = comma;
+        index++;
+      }
+
+      return this;
+    }
+
     [StringFormatMethod("format")]
     public ConcreteSyntaxTree Write(string format, params object[] args) {
       Write(string.Format(format, args));
diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntime.go b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntime.go
index 1ef1afe1729..f5288328cda 100644
--- a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntime.go
+++ b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntime.go
@@ -1034,6 +1034,7 @@ func (_this arrayForByte) ArrayGet1CodePoint(index int) CodePoint {
 func (_this arrayForByte) ArraySet1CodePoint(value CodePoint, index int) {
   panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}")
 }
+
 func (_this arrayForByte) anySlice(lo, hi Int) []interface{} {
   if lo.IsNilInt() {
     lo = Zero
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/CodePoint.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/CodePoint.java
index 86fa7a4431b..71f38eef4f5 100644
--- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/CodePoint.java
+++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/CodePoint.java
@@ -48,9 +48,13 @@ public boolean equals(Object obj) {
         return value == ((CodePoint)obj).value;
     }
 
+    public static int hashCode(int value) {
+        return Integer.hashCode(value);
+    }
+
     @Override
     public int hashCode() {
-        return Integer.hashCode(value);
+        return hashCode(value);
     }
 
     public int value() {
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java
index 74cf708d1f5..13127e4bb9d 100644
--- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java
+++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java
@@ -168,12 +168,11 @@ public static Iterable<Character> AllChars() {
         return () -> IntStream.range(0, 0x1_0000).<Character>mapToObj(i -> Character.valueOf((char)i)).iterator();
     }
 
-    // Note we don't use CodePoint here because this is only used in the implementation of quantification,
-    // where we want to enumerate primitive values, and it's challenging to customize that logic
-    // to unbox CodePoints manually.
-    public static Iterable<Integer> AllUnicodeChars() {
+    public static Iterable<CodePoint> AllUnicodeChars() {
         return () -> IntStream.concat(IntStream.range(0, 0xD800), 
-                                      IntStream.range(0xE000, 0x11_0000)).iterator();
+                                      IntStream.range(0xE000, 0x11_0000))
+                              .mapToObj(CodePoint::valueOf)
+                              .iterator();
     }
 
     public static <G> String toString(G g) {
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java
index 56fdece34fc..52a6d299049 100644
--- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java
+++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java
@@ -122,7 +122,7 @@ public static TypeDescriptor<Character> charWithDefault(char d) {
         return new CharType(d);
     }
 
-    public static TypeDescriptor<CodePoint> unicodeCharWithDefault(char d) {
+    public static TypeDescriptor<CodePoint> unicodeCharWithDefault(int d) {
         return new UnicodeCharType(CodePoint.valueOf(d));
     }
 
diff --git a/Source/TestDafny/TestDafny.cs b/Source/TestDafny/TestDafny.cs
index 1460cf28918..9ce6d4b28ec 100644
--- a/Source/TestDafny/TestDafny.cs
+++ b/Source/TestDafny/TestDafny.cs
@@ -86,18 +86,23 @@ private static int ForEachCompiler(ForEachCompilerOptions options) {
     var expectedOutput = "\nDafny program verifier did not attempt verification\n" +
                          File.ReadAllText(expectFile);
 
+    var success = true;
     foreach (var plugin in dafnyOptions.Plugins) {
       foreach (var compiler in plugin.GetCompilers()) {
         var result = RunWithCompiler(options, compiler, expectedOutput);
         if (result != 0) {
-          return result;
+          success = false;
         }
       }
     }
 
-    Console.Out.WriteLine(
-      $"All executions were successful and matched the expected output (or reported errors for known unsupported features)!");
-    return 0;
+    if (success) {
+      Console.Out.WriteLine(
+        $"All executions were successful and matched the expected output (or reported errors for known unsupported features)!");
+      return 0;
+    } else {
+      return -1;
+    }
   }
 
   private static int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend backend, string expectedOutput) {
diff --git a/Test/allocated1/dafny0/Strings.dfy.expect b/Test/allocated1/dafny0/Strings.dfy.expect
index cd5ab16dd75..90fe826a7f3 100644
--- a/Test/allocated1/dafny0/Strings.dfy.expect
+++ b/Test/allocated1/dafny0/Strings.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 9 verified, 0 errors
+Dafny program verifier finished with 11 verified, 0 errors
 ch = D
 The string is: DDD
 Escape X: I say "hello" \ you say 'good bye'
diff --git a/Test/comp/NativeNumbers.dfy b/Test/comp/NativeNumbers.dfy
index d122d681a5d..ebe1d1677e9 100644
--- a/Test/comp/NativeNumbers.dfy
+++ b/Test/comp/NativeNumbers.dfy
@@ -1,10 +1,10 @@
 // Skip JavaScript because JavaScript doesn't have the same native types
 
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:py "%s" >> "%t"
+// RUN: %dafny /compile:0 /unicodeChar:0 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /spillTargetCode:2 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /spillTargetCode:2 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /spillTargetCode:2 /compileTarget:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {
diff --git a/Test/comp/Numbers.dfy b/Test/comp/Numbers.dfy
index 65848ac921f..af76b5f40de 100644
--- a/Test/comp/Numbers.dfy
+++ b/Test/comp/Numbers.dfy
@@ -1,9 +1,9 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
+// RUN: %dafny /compile:0 /unicodeChar:0 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {
diff --git a/Test/comp/UnicodeStrings.dfy b/Test/comp/UnicodeStrings.dfy
index bff5daa1dd1..413a813fc91 100644
--- a/Test/comp/UnicodeStrings.dfy
+++ b/Test/comp/UnicodeStrings.dfy
@@ -242,3 +242,19 @@ method CharQuantification() {
 
 // Dummy identity function just to enable triggers that Dafny and Boogie are happy with
 function method Identity<T>(x: T): T { x }
+
+method CharsAndArrows() {
+  var lambda := (c: char) requires c <= 'Z' => c + 1 as char;
+  var fromLambda := lambda('C');
+  print fromLambda, "\n";
+
+  var funcRef := IncrementChar;
+  var fromFuncRef := funcRef('C');
+  print fromFuncRef, "\n";
+}
+
+function method IncrementChar(c: char): char 
+  requires c <= 'Z'
+{
+  c + 1 as char
+}
diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy
index 82007e31da4..a38d9eb516e 100644
--- a/Test/dafny0/Strings.dfy
+++ b/Test/dafny0/Strings.dfy
@@ -152,3 +152,19 @@ method AllCharsTest() {
 }
 
 function method Identity<T>(x: T): T { x }
+
+method CharsAndArrows() {
+  var lambda := (c: char) requires c <= 'Z' => c + 1 as char;
+  var fromLambda := lambda('C');
+  print fromLambda, "\n";
+
+  var funcRef := IncrementChar;
+  var fromFuncRef := funcRef('C');
+  print fromFuncRef, "\n";
+}
+
+function method IncrementChar(c: char): char 
+  requires c <= 'Z'
+{
+  c + 1 as char
+}
diff --git a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
index beff6508b61..66653bb0c86 100644
--- a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
+++ b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
@@ -11,3 +11,39 @@ Diff (changing expected into actual):
 +      }
  
 
+Executing on Go...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+ 
+ Dafny program verifier did not attempt verification
+-System.Func`2[System.Numerics.BigInteger,System.Numerics.BigInteger]
++func(dafny.Int) dafny.Int
+ 
+
+Executing on Java...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+ 
+ Dafny program verifier did not attempt verification
+-System.Func`2[System.Numerics.BigInteger,System.Numerics.BigInteger]
++Function
+ 
+
+Executing on Python...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+ 
+ Dafny program verifier did not attempt verification
+-System.Func`2[System.Numerics.BigInteger,System.Numerics.BigInteger]
++Function
+ 
+
+Executing on C++...
+Execution failed, for reasons other than known unsupported features. Output:
+
+Dafny program verifier did not attempt verification
+(0,-1): Error: UserDefinedTypeName _#Func1
+
+Error:
+
+Executing on Dafny...
diff --git a/Test/unicodechars/comp/Arrays.dfy b/Test/unicodechars/comp/Arrays.dfy
index fd09042100d..d206b7dc373 100644
--- a/Test/unicodechars/comp/Arrays.dfy
+++ b/Test/unicodechars/comp/Arrays.dfy
@@ -1,7 +1,2 @@
-// RUN: %baredafny run --no-verify --target=cs --unicode-char %args "%s" > "%t"
-// RUN: %baredafny run --no-verify --target=js --unicode-char %args "%s" >> "%t"
-// RUN: %baredafny run --no-verify --target=go --unicode-char %args "%s" >> "%t"
-// this is not yet working: %baredafny run --no-verify --target=java --unicode-char %args "%s" >> "%t"
-// RUN: %baredafny run --no-verify --target=py --unicode-char %args "%s" >> "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:1
 include "../../comp/Arrays.dfy"
diff --git a/Test/unicodechars/comp/Arrays.dfy.expect b/Test/unicodechars/comp/Arrays.dfy.expect
index 36fa3933c6a..4511b0842c8 100644
--- a/Test/unicodechars/comp/Arrays.dfy.expect
+++ b/Test/unicodechars/comp/Arrays.dfy.expect
@@ -1,299 +1,3 @@
-
-Dafny program verifier did not attempt verification
-0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 
-17
-[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22]
-[2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
-[20, 21, 22]
-[0, 1, 2, 3, 4, 5, 6, 7]
-[0, 1, 2, 3, 4, 5, 6, 7]
-'d' 'd' 'd' 
-'h' 'e' 'l' 'l' 'o' 
-0 0 0 0 0 0 0 0 
-0 0 0 0 0 0 0 0 
-1 0 0 0 0 
-0 1 0 0 0 
-0 0 1 0 0 
-cube dims: 3 0 4
-[] [0] [0, 0] [0, 0, 0] [0, 0, 0, 0] 
-It's null
-hi hello tjena hej hola
-hi hello tjena hej hola
-hi hello tjena hej hola
-'d' 'd' 'd' 
-'h' 'e' 'l' 'l' 'o' 
-8 8 8 8 
-true true true 
-1 1 1 1 1 
-2 2 2 2 2 
-3 3 3 3 3 
-4 4 4 4 4 
-('d', 8, true, 1, 2, 3, 4)
-'D' 'D' 'D' 
-0 0 0 0 
-false false false 
-0 0 0 0 0 
-0 0 0 0 0 
-0 0 0 0 0 
-0 0 0 0 0 
-('D', 0, false, 0, 0, 0, 0)
-8 0
-false 0 null null
-8 8
-8 8
-8 8
-8 8
-'D' 'D' 'D' 
-'D' 'D' 'D' 
-'D' 'D' 'D' 
-'D' 'D' 'r' ('D', 'D', 'r')
-'D' 'D' 'r'
-[19, 18, 9, 8]
- true
- false
- true
- false
- false
- false
- true
- true
- false
- true
- false
- true
- true
- false
-hello there
-false false
-true true
-false false
-false false
-uninitialized bytes: array[0, 0, 0]
-bytes from display: array[7, 8, 9]
-bytes from lambda: array[20, 21, 22]
-uninitialized 1bytes: array[1, 1, 1]
-1bytes from display: array[7, 8, 9]
-1bytes from lambda: array[20, 21, 22]
-17 19 18 20
-100 200 300 120 38
-hello [0, 1, 2, 3, 4] [2, 2, 2, 2, 2]
-[77, 77, 77, 77, 77, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 78, 78, 78, 78, 78]
-[77, 77, 77, 77, 77, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 78, 78, 78, 78, 78]
-[99, 99, 99, 99, 99, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 82, 82, 82, 82, 82]
-[0, 0, 0, 0, 0, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 60, 60, 60, 60, 60]
-[0, 0, 0, 0, 0, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 60, 60, 60, 60, 60]
-DDDDDabcdeabcdeggggg
-['D', 'D', 'D', 'D', 'D', 'a', 'b', 'c', 'd', 'e', 'a', 'b', 'c', 'd', 'e', 'g', 'g', 'g', 'g', 'g']
-[77, 77, 77, 77, 77, 77, 77, 77, 77, 77, 50, 78, 78, 78, 78, 78, 50, 78, 78, 78]
-[77, 77, 77, 77, 77, 77, 77, 77, 77, 77, 50, 78, 78, 78, 78, 78, 50, 78, 78, 78]
-[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 50, 60, 60, 60, 60, 60, 50, 60, 60, 60]
-['D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'a', 'g', 'g', 'g', 'g', 'g', 'a', 'g', 'g', 'g']
-0 69 50
-0 69 50
-'D' 'k' 'n'
-false false
-true true
-false false
-false false
-true true
-
-Dafny program verifier did not attempt verification
-0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 
-17
-[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22]
-[2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
-[20, 21, 22]
-[0, 1, 2, 3, 4, 5, 6, 7]
-[0, 1, 2, 3, 4, 5, 6, 7]
-'d' 'd' 'd' 
-'h' 'e' 'l' 'l' 'o' 
-0 0 0 0 0 0 0 0 
-0 0 0 0 0 0 0 0 
-1 0 0 0 0 
-0 1 0 0 0 
-0 0 1 0 0 
-cube dims: 3 0 4
-[] [0] [0, 0] [0, 0, 0] [0, 0, 0, 0] 
-It's null
-hi hello tjena hej hola
-hi hello tjena hej hola
-hi hello tjena hej hola
-'d' 'd' 'd' 
-'h' 'e' 'l' 'l' 'o' 
-8 8 8 8 
-true true true 
-1 1 1 1 1 
-2 2 2 2 2 
-3 3 3 3 3 
-4 4 4 4 4 
-('d', 8, true, 1, 2, 3, 4)
-'D' 'D' 'D' 
-0 0 0 0 
-false false false 
-0 0 0 0 0 
-0 0 0 0 0 
-0 0 0 0 0 
-0 0 0 0 0 
-('D', 0, false, 0, 0, 0, 0)
-8 0
-false 0 null null
-8 8
-8 8
-8 8
-8 8
-'D' 'D' 'D' 
-'D' 'D' 'D' 
-'D' 'D' 'D' 
-'D' 'D' 'r' ('D', 'D', 'r')
-'D' 'D' 'r'
-[19, 18, 9, 8]
- true
- false
- true
- false
- false
- false
- true
- true
- false
- true
- false
- true
- true
- false
-hello there
-false false
-true true
-false false
-false false
-uninitialized bytes: array[0, 0, 0]
-bytes from display: array[7, 8, 9]
-bytes from lambda: array[20, 21, 22]
-uninitialized 1bytes: array[1, 1, 1]
-1bytes from display: array[7, 8, 9]
-1bytes from lambda: array[20, 21, 22]
-17 19 18 20
-100 200 300 120 38
-hello [0, 1, 2, 3, 4] [2, 2, 2, 2, 2]
-[77, 77, 77, 77, 77, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 78, 78, 78, 78, 78]
-[77, 77, 77, 77, 77, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 78, 78, 78, 78, 78]
-[99, 99, 99, 99, 99, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 82, 82, 82, 82, 82]
-[0, 0, 0, 0, 0, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 60, 60, 60, 60, 60]
-[0, 0, 0, 0, 0, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 60, 60, 60, 60, 60]
-DDDDDabcdeabcdeggggg
-['D', 'D', 'D', 'D', 'D', 'a', 'b', 'c', 'd', 'e', 'a', 'b', 'c', 'd', 'e', 'g', 'g', 'g', 'g', 'g']
-[77, 77, 77, 77, 77, 77, 77, 77, 77, 77, 50, 78, 78, 78, 78, 78, 50, 78, 78, 78]
-[77, 77, 77, 77, 77, 77, 77, 77, 77, 77, 50, 78, 78, 78, 78, 78, 50, 78, 78, 78]
-[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 50, 60, 60, 60, 60, 60, 50, 60, 60, 60]
-['D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'a', 'g', 'g', 'g', 'g', 'g', 'a', 'g', 'g', 'g']
-0 69 50
-0 69 50
-'D' 'k' 'n'
-false false
-true true
-false false
-false false
-true true
-
-Dafny program verifier did not attempt verification
-0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 
-17
-[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22]
-[2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
-[20, 21, 22]
-[0, 1, 2, 3, 4, 5, 6, 7]
-[0, 1, 2, 3, 4, 5, 6, 7]
-'d' 'd' 'd' 
-'h' 'e' 'l' 'l' 'o' 
-0 0 0 0 0 0 0 0 
-0 0 0 0 0 0 0 0 
-1 0 0 0 0 
-0 1 0 0 0 
-0 0 1 0 0 
-cube dims: 3 0 4
-[] [0] [0, 0] [0, 0, 0] [0, 0, 0, 0] 
-It's null
-hi hello tjena hej hola
-hi hello tjena hej hola
-hi hello tjena hej hola
-'d' 'd' 'd' 
-'h' 'e' 'l' 'l' 'o' 
-8 8 8 8 
-true true true 
-1 1 1 1 1 
-2 2 2 2 2 
-3 3 3 3 3 
-4 4 4 4 4 
-('d', 8, true, 1, 2, 3, 4)
-'D' 'D' 'D' 
-0 0 0 0 
-false false false 
-0 0 0 0 0 
-0 0 0 0 0 
-0 0 0 0 0 
-0 0 0 0 0 
-('D', 0, false, 0, 0, 0, 0)
-8 0
-false 0 null null
-8 8
-8 8
-8 8
-8 8
-'D' 'D' 'D' 
-'D' 'D' 'D' 
-'D' 'D' 'D' 
-'D' 'D' 'r' ('D', 'D', 'r')
-'D' 'D' 'r'
-[19, 18, 9, 8]
- true
- false
- true
- false
- false
- false
- true
- true
- false
- true
- false
- true
- true
- false
-hello there
-false false
-true true
-false false
-false false
-uninitialized bytes: array[0, 0, 0]
-bytes from display: array[7, 8, 9]
-bytes from lambda: array[20, 21, 22]
-uninitialized 1bytes: array[1, 1, 1]
-1bytes from display: array[7, 8, 9]
-1bytes from lambda: array[20, 21, 22]
-17 19 18 20
-100 200 300 120 38
-hello [0, 1, 2, 3, 4] [2, 2, 2, 2, 2]
-[77, 77, 77, 77, 77, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 78, 78, 78, 78, 78]
-[77, 77, 77, 77, 77, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 78, 78, 78, 78, 78]
-[99, 99, 99, 99, 99, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 82, 82, 82, 82, 82]
-[0, 0, 0, 0, 0, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 60, 60, 60, 60, 60]
-[0, 0, 0, 0, 0, 20, 21, 22, 23, 24, 20, 21, 22, 23, 24, 60, 60, 60, 60, 60]
-DDDDDabcdeabcdeggggg
-['D', 'D', 'D', 'D', 'D', 'a', 'b', 'c', 'd', 'e', 'a', 'b', 'c', 'd', 'e', 'g', 'g', 'g', 'g', 'g']
-[77, 77, 77, 77, 77, 77, 77, 77, 77, 77, 50, 78, 78, 78, 78, 78, 50, 78, 78, 78]
-[77, 77, 77, 77, 77, 77, 77, 77, 77, 77, 50, 78, 78, 78, 78, 78, 50, 78, 78, 78]
-[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 50, 60, 60, 60, 60, 60, 50, 60, 60, 60]
-['D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'D', 'a', 'g', 'g', 'g', 'g', 'g', 'a', 'g', 'g', 'g']
-0 69 50
-0 69 50
-'D' 'k' 'n'
-false false
-true true
-false false
-false false
-true true
-
-Dafny program verifier did not attempt verification
 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 
 17
 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22]
diff --git a/Test/unicodechars/comp/Collections.dfy b/Test/unicodechars/comp/Collections.dfy
new file mode 100644
index 00000000000..fb3e451eb83
--- /dev/null
+++ b/Test/unicodechars/comp/Collections.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:0 /verifyAllModules /unicodeChar:1 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+include "../../comp/Collections.dfy"
diff --git a/Test/unicodechars/comp/Collections.dfy.expect b/Test/unicodechars/comp/Collections.dfy.expect
new file mode 100644
index 00000000000..70586502b0d
--- /dev/null
+++ b/Test/unicodechars/comp/Collections.dfy.expect
@@ -0,0 +1,637 @@
+
+Dafny program verifier finished with 40 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+Sets: {} {17, 82} {12, 17}
+  cardinality: 0 2 2
+  union: {17, 82} {12, 17, 82}
+  intersection: {} {17}
+  difference: {} {82}
+  disjoint: true false
+  subset: true false true
+  proper subset: true false false
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  eq covariance: 1 true true
+false true
+|s|=4 |S|=16
+{{}, {'a'}, {'b'}, {'c'}, {'d'}, {'a', 'b'}, {'a', 'c'}, {'b', 'c'}, {'a', 'd'}, {'b', 'd'}, {'c', 'd'}, {'a', 'b', 'c'}, {'a', 'b', 'd'}, {'a', 'c', 'd'}, {'b', 'c', 'd'}, {'a', 'b', 'c', 'd'}}
+Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
+  cardinality: 0 4 2
+  union: multiset{17, 17, 82, 82} multiset{12, 17, 17, 17, 82, 82}
+  intersection: multiset{} multiset{17}
+  difference: multiset{} multiset{17, 82, 82}
+  disjoint: true false
+  subset: true false true true
+  proper subset: true false false true
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
+  multiplicity: 0 2 1
+Test zero multiplicity:
+  printing: multiset{multiset{}, multiset{42}} multiset{12}
+  union: 1 1 1 1
+  membership: false false
+  equality: false true false
+  subset: true true true true false
+  strict subset: true false false true false
+  disjoint: true true true true
+Sequences: [] [17, 82, 17, 82] [12, 17]
+  cardinality: 0 4 2
+  update: [42, 82, 17, 82] [42, 17]
+  index: 17 12
+  subsequence ([lo..hi]): [82, 17] [17]
+  subsequence ([lo..]): [82, 17, 82] [17]
+  subsequence ([..hi]): [17, 82, 17][12]
+  subsequence ([..]): [] [17, 82, 17, 82] [12, 17]
+  concatenation: [17, 82, 17, 82] [17, 82, 17, 82, 12, 17]
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+Bound Bound Bound Bound Bound Bound
+ed ed ed ed ed ed
+'e' 'e' 'e' 'e' 'e' 'e'
+hello
+hEllo
+[2, 4, 6, 8, 10]
+[2, 0, 6, 8, 10]
+true false false
+true true false true
+false false false true
+  eq covariance: true true
+Strings:  uRuR gu
+  cardinality: 0 4 2
+  concatenation: uRuR uRuRgu
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+  constructed as sequence: guru
+  mix: hello-d ddd-hello
+Maps: map[] map[17 := 2, 82 := 2] map[12 := 26, 17 := 0]
+  cardinality: 0 2 2
+  keys: {} {17, 82} {12, 17}
+  values: {} {2} {0, 26}
+  items: {} {(17, 2), (82, 2)} {(12, 26), (17, 0)}
+  update: 6 (1 0) 6 (2 2 2) 6 (2 2 0)
+  lookup: false 2 0
+m: map[Color.Blue := 30, Color.Yellow := 21]
+keys: {Color.Blue, Color.Yellow}
+values: {21, 30}
+items: {(Color.Blue, 30), (Color.Yellow, 21)}
+3 2 4
+70 52 66
+8 67 67
+4 4 3
+true false true false
+true false false false
+false false true
+false false false true
+0 20 4
+198 20 4
+0 2 false
+true true true false
+0 20 4
+198 20 4
+0 2 false
+false false true
+false true true true
+jack wendy null
+jack null null
+ronald ronald false
+true true true false
+jack wendy null
+jack null null
+ronald ronald false
+2: 0 1 1
+3: 0 1 2
+There are 0 occurrences of 58 in the multiset
+There are 536870912 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of null in the multiset
+Map===
+|s|=1 |u|=1
+s[1]=123 u[1]=40
+|S|=1 |U|=1
+S[1]=123 U[1]=41
+Seq===
+|s|=2 |u|=2
+123 42, 123 42, 123 42
+|s|=2 |u|=2
+123 43, 123 43, 123 43
+|s|=2 |u|=2
+123 44, 123 44, 123 44
+Multiset===
+|s|=2 |u|=4
+1 3
+|s|=2 |u|=4
+1 3
+
+Dafny program verifier did not attempt verification
+Sets: {} {17, 82} {12, 17}
+  cardinality: 0 2 2
+  union: {17, 82} {17, 82, 12}
+  intersection: {} {17}
+  difference: {} {82}
+  disjoint: true false
+  subset: true false true
+  proper subset: true false false
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  eq covariance: 1 true true
+false true
+|s|=4 |S|=16
+{{}, {'a'}, {'b'}, {'c'}, {'d'}, {'a', 'b'}, {'a', 'c'}, {'b', 'c'}, {'a', 'd'}, {'b', 'd'}, {'c', 'd'}, {'a', 'b', 'c'}, {'a', 'b', 'd'}, {'a', 'c', 'd'}, {'b', 'c', 'd'}, {'a', 'b', 'c', 'd'}}
+Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
+  cardinality: 0 4 2
+  union: multiset{17, 17, 82, 82} multiset{17, 17, 17, 82, 82, 12}
+  intersection: multiset{} multiset{17}
+  difference: multiset{} multiset{17, 82, 82}
+  disjoint: true false
+  subset: true false true true
+  proper subset: true false false true
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
+  multiplicity: 0 2 1
+Test zero multiplicity:
+  printing: multiset{multiset{}, multiset{42}} multiset{12}
+  union: 1 1 1 1
+  membership: false false
+  equality: false true false
+  subset: true true true true false
+  strict subset: true false false true false
+  disjoint: true true true true
+Sequences: [] [17, 82, 17, 82] [12, 17]
+  cardinality: 0 4 2
+  update: [42, 82, 17, 82] [42, 17]
+  index: 17 12
+  subsequence ([lo..hi]): [82, 17] [17]
+  subsequence ([lo..]): [82, 17, 82] [17]
+  subsequence ([..hi]): [17, 82, 17][12]
+  subsequence ([..]): [] [17, 82, 17, 82] [12, 17]
+  concatenation: [17, 82, 17, 82] [17, 82, 17, 82, 12, 17]
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+Bound Bound Bound Bound Bound Bound
+ed ed ed ed ed ed
+'e' 'e' 'e' 'e' 'e' 'e'
+hello
+hEllo
+[2, 4, 6, 8, 10]
+[2, 0, 6, 8, 10]
+true false false
+true true false true
+false false false true
+  eq covariance: true true
+Strings:  uRuR gu
+  cardinality: 0 4 2
+  concatenation: uRuR uRuRgu
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+  constructed as sequence: guru
+  mix: hello-d ddd-hello
+Maps: map[] map[17 := 2, 82 := 2] map[17 := 0, 12 := 26]
+  cardinality: 0 2 2
+  keys: {} {17, 82} {17, 12}
+  values: {} {2} {0, 26}
+  items: {} {(17, 2), (82, 2)} {(17, 0), (12, 26)}
+  update: 6 (1 0) 6 (2 2 2) 6 (2 2 0)
+  lookup: false 2 0
+m: map[Color.Blue := 30, Color.Yellow := 21]
+keys: {Color.Blue, Color.Yellow}
+values: {30, 21}
+items: {(Color.Blue, 30), (Color.Yellow, 21)}
+3 2 4
+70 52 66
+8 67 67
+4 4 3
+true false true false
+true false false false
+false false true
+false false false true
+0 20 4
+198 20 4
+0 2 false
+true true true false
+0 20 4
+198 20 4
+0 2 false
+false false true
+false true true true
+jack wendy null
+jack null null
+ronald ronald false
+true true true false
+jack wendy null
+jack null null
+ronald ronald false
+2: 0 1 1
+3: 0 1 2
+There are 0 occurrences of 58 in the multiset
+There are 536870912 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of null in the multiset
+Map===
+|s|=1 |u|=1
+s[1]=123 u[1]=40
+|S|=1 |U|=1
+S[1]=123 U[1]=41
+Seq===
+|s|=2 |u|=2
+123 42, 123 42, 123 42
+|s|=2 |u|=2
+123 43, 123 43, 123 43
+|s|=2 |u|=2
+123 44, 123 44, 123 44
+Multiset===
+|s|=2 |u|=4
+1 3
+|s|=2 |u|=4
+1 3
+
+Dafny program verifier did not attempt verification
+Sets: {} {17, 82} {12, 17}
+  cardinality: 0 2 2
+  union: {17, 82} {17, 82, 12}
+  intersection: {} {17}
+  difference: {} {82}
+  disjoint: true false
+  subset: true false true
+  proper subset: true false false
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  eq covariance: 1 true true
+false true
+|s|=4 |S|=16
+{{}, {'a'}, {'b'}, {'c'}, {'d'}, {'a', 'b'}, {'a', 'c'}, {'b', 'c'}, {'a', 'd'}, {'b', 'd'}, {'c', 'd'}, {'a', 'b', 'c'}, {'a', 'b', 'd'}, {'a', 'c', 'd'}, {'b', 'c', 'd'}, {'a', 'b', 'c', 'd'}}
+Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
+  cardinality: 0 4 2
+  union: multiset{17, 17, 82, 82} multiset{17, 17, 17, 82, 82, 12}
+  intersection: multiset{} multiset{17}
+  difference: multiset{} multiset{17, 82, 82}
+  disjoint: true false
+  subset: true false true true
+  proper subset: true false false true
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
+  multiplicity: 0 2 1
+Test zero multiplicity:
+  printing: multiset{multiset{}, multiset{42}} multiset{12}
+  union: 1 1 1 1
+  membership: false false
+  equality: false true false
+  subset: true true true true false
+  strict subset: true false false true false
+  disjoint: true true true true
+Sequences: [] [17, 82, 17, 82] [12, 17]
+  cardinality: 0 4 2
+  update: [42, 82, 17, 82] [42, 17]
+  index: 17 12
+  subsequence ([lo..hi]): [82, 17] [17]
+  subsequence ([lo..]): [82, 17, 82] [17]
+  subsequence ([..hi]): [17, 82, 17][12]
+  subsequence ([..]): [] [17, 82, 17, 82] [12, 17]
+  concatenation: [17, 82, 17, 82] [17, 82, 17, 82, 12, 17]
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+Bound Bound Bound Bound Bound Bound
+ed ed ed ed ed ed
+'e' 'e' 'e' 'e' 'e' 'e'
+hello
+hEllo
+[2, 4, 6, 8, 10]
+[2, 0, 6, 8, 10]
+true false false
+true true false true
+false false false true
+  eq covariance: true true
+Strings:  uRuR gu
+  cardinality: 0 4 2
+  concatenation: uRuR uRuRgu
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+  constructed as sequence: guru
+  mix: hello-d ddd-hello
+Maps: map[] map[17 := 2, 82 := 2] map[17 := 0, 12 := 26]
+  cardinality: 0 2 2
+  keys: {} {17, 82} {17, 12}
+  values: {} {2} {0, 26}
+  items: {} {(17, 2), (82, 2)} {(17, 0), (12, 26)}
+  update: 6 (1 0) 6 (2 2 2) 6 (2 2 0)
+  lookup: false 2 0
+m: map[Color.Blue := 30, Color.Yellow := 21]
+keys: {Color.Blue, Color.Yellow}
+values: {30, 21}
+items: {(Color.Blue, 30), (Color.Yellow, 21)}
+3 2 4
+70 52 66
+8 67 67
+4 4 3
+true false true false
+true false false false
+false false true
+false false false true
+0 20 4
+198 20 4
+0 2 false
+true true true false
+0 20 4
+198 20 4
+0 2 false
+false false true
+false true true true
+jack wendy null
+jack null null
+ronald ronald false
+true true true false
+jack wendy null
+jack null null
+ronald ronald false
+2: 0 1 1
+3: 0 1 2
+There are 0 occurrences of 58 in the multiset
+There are 536870912 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of null in the multiset
+Map===
+|s|=1 |u|=1
+s[1]=123 u[1]=40
+|S|=1 |U|=1
+S[1]=123 U[1]=41
+Seq===
+|s|=2 |u|=2
+123 42, 123 42, 123 42
+|s|=2 |u|=2
+123 43, 123 43, 123 43
+|s|=2 |u|=2
+123 44, 123 44, 123 44
+Multiset===
+|s|=2 |u|=4
+1 3
+|s|=2 |u|=4
+1 3
+
+Dafny program verifier did not attempt verification
+Sets: {} {17, 82} {17, 12}
+  cardinality: 0 2 2
+  union: {17, 82} {17, 82, 12}
+  intersection: {} {17}
+  difference: {} {82}
+  disjoint: true false
+  subset: true false true
+  proper subset: true false false
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  eq covariance: 1 true true
+false true
+|s|=4 |S|=16
+{{}, {'a'}, {'b'}, {'c'}, {'d'}, {'a', 'b'}, {'a', 'c'}, {'b', 'c'}, {'a', 'd'}, {'b', 'd'}, {'c', 'd'}, {'a', 'b', 'c'}, {'a', 'b', 'd'}, {'a', 'c', 'd'}, {'b', 'c', 'd'}, {'a', 'b', 'c', 'd'}}
+Multisets: multiset{} multiset{17, 17, 82, 82} multiset{17, 12}
+  cardinality: 0 4 2
+  union: multiset{17, 17, 82, 82} multiset{17, 17, 17, 82, 82, 12}
+  intersection: multiset{} multiset{17}
+  difference: multiset{} multiset{17, 82, 82}
+  disjoint: true false
+  subset: true false true true
+  proper subset: true false false true
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{17, 17, 12}
+  multiplicity: 0 2 1
+Test zero multiplicity:
+  printing: multiset{multiset{}, multiset{42}} multiset{12}
+  union: 1 1 1 1
+  membership: false false
+  equality: false true false
+  subset: true true true true false
+  strict subset: true false false true false
+  disjoint: true true true true
+Sequences: [] [17, 82, 17, 82] [12, 17]
+  cardinality: 0 4 2
+  update: [42, 82, 17, 82] [42, 17]
+  index: 17 12
+  subsequence ([lo..hi]): [82, 17] [17]
+  subsequence ([lo..]): [82, 17, 82] [17]
+  subsequence ([..hi]): [17, 82, 17][12]
+  subsequence ([..]): [] [17, 82, 17, 82] [12, 17]
+  concatenation: [17, 82, 17, 82] [17, 82, 17, 82, 12, 17]
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+Bound Bound Bound Bound Bound Bound
+ed ed ed ed ed ed
+'e' 'e' 'e' 'e' 'e' 'e'
+hello
+hEllo
+[2, 4, 6, 8, 10]
+[2, 0, 6, 8, 10]
+true false false
+true true false true
+false false false true
+  eq covariance: true true
+Strings:  uRuR gu
+  cardinality: 0 4 2
+  concatenation: uRuR uRuRgu
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+  constructed as sequence: guru
+  mix: hello-d ddd-hello
+Maps: map[] map[17 := 2, 82 := 2] map[17 := 0, 12 := 26]
+  cardinality: 0 2 2
+  keys: {} {17, 82} {17, 12}
+  values: {} {2} {0, 26}
+  items: {} {(17, 2), (82, 2)} {(17, 0), (12, 26)}
+  update: 6 (1 0) 6 (2 2 2) 6 (2 2 0)
+  lookup: false 2 0
+m: map[Color.Yellow := 21, Color.Blue := 30]
+keys: {Color.Yellow, Color.Blue}
+values: {21, 30}
+items: {(Color.Yellow, 21), (Color.Blue, 30)}
+3 2 4
+70 52 66
+8 67 67
+4 4 3
+true false true false
+true false false false
+false false true
+false false false true
+0 20 4
+198 20 4
+0 2 false
+true true true false
+0 20 4
+198 20 4
+0 2 false
+false false true
+false true true true
+jack wendy null
+jack null null
+ronald ronald false
+true true true false
+jack wendy null
+jack null null
+ronald ronald false
+2: 0 1 1
+3: 0 1 2
+There are 0 occurrences of 58 in the multiset
+There are 536870912 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of null in the multiset
+Map===
+|s|=1 |u|=1
+s[1]=123 u[1]=40
+|S|=1 |U|=1
+S[1]=123 U[1]=41
+Seq===
+|s|=2 |u|=2
+123 42, 123 42, 123 42
+|s|=2 |u|=2
+123 43, 123 43, 123 43
+|s|=2 |u|=2
+123 44, 123 44, 123 44
+Multiset===
+|s|=2 |u|=4
+1 3
+|s|=2 |u|=4
+1 3
+
+Dafny program verifier did not attempt verification
+Sets: {} {17, 82} {17, 12}
+  cardinality: 0 2 2
+  union: {17, 82} {17, 82, 12}
+  intersection: {} {17}
+  difference: {} {82}
+  disjoint: true false
+  subset: true false true
+  proper subset: true false false
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  eq covariance: 1 true true
+false true
+|s|=4 |S|=16
+{{}, {'a'}, {'b'}, {'c'}, {'d'}, {'a', 'b'}, {'a', 'c'}, {'b', 'c'}, {'a', 'd'}, {'b', 'd'}, {'c', 'd'}, {'a', 'b', 'c'}, {'a', 'b', 'd'}, {'a', 'c', 'd'}, {'b', 'c', 'd'}, {'a', 'b', 'c', 'd'}}
+Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
+  cardinality: 0 4 2
+  union: multiset{17, 17, 82, 82} multiset{17, 17, 17, 82, 82, 12}
+  intersection: multiset{} multiset{17}
+  difference: multiset{} multiset{17, 82, 82}
+  disjoint: true false
+  subset: true false true true
+  proper subset: true false false true
+  superset: false true true
+  proper superset: false true false
+  membership: false true true
+  update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
+  multiplicity: 0 2 1
+Test zero multiplicity:
+  printing: multiset{multiset{}, multiset{42}} multiset{12}
+  union: 1 1 1 1
+  membership: false false
+  equality: false true false
+  subset: true true true true false
+  strict subset: true false false true false
+  disjoint: true true true true
+Sequences: [] [17, 82, 17, 82] [12, 17]
+  cardinality: 0 4 2
+  update: [42, 82, 17, 82] [42, 17]
+  index: 17 12
+  subsequence ([lo..hi]): [82, 17] [17]
+  subsequence ([lo..]): [82, 17, 82] [17]
+  subsequence ([..hi]): [17, 82, 17][12]
+  subsequence ([..]): [] [17, 82, 17, 82] [12, 17]
+  concatenation: [17, 82, 17, 82] [17, 82, 17, 82, 12, 17]
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+Bound Bound Bound Bound Bound Bound
+ed ed ed ed ed ed
+'e' 'e' 'e' 'e' 'e' 'e'
+hello
+hEllo
+[2, 4, 6, 8, 10]
+[2, 0, 6, 8, 10]
+true false false
+true true false true
+false false false true
+  eq covariance: true true
+Strings:  uRuR gu
+  cardinality: 0 4 2
+  concatenation: uRuR uRuRgu
+  prefix: true false true
+  proper prefix: true false false
+  membership: false true true
+  constructed as sequence: guru
+  mix: hello-d ddd-hello
+Maps: map[] map[82 := 2, 17 := 2] map[17 := 0, 12 := 26]
+  cardinality: 0 2 2
+  keys: {} {17, 82} {17, 12}
+  values: {} {2} {0, 26}
+  items: {} {(82, 2), (17, 2)} {(17, 0), (12, 26)}
+  update: 6 (1 0) 6 (2 2 2) 6 (2 2 0)
+  lookup: false 2 0
+m: map[Color.Blue := 30, Color.Yellow := 21]
+keys: {Color.Blue, Color.Yellow}
+values: {21, 30}
+items: {(Color.Blue, 30), (Color.Yellow, 21)}
+3 2 4
+70 52 66
+8 67 67
+4 4 3
+true false true false
+true false false false
+false false true
+false false false true
+0 20 4
+198 20 4
+0 2 false
+true true true false
+0 20 4
+198 20 4
+0 2 false
+false false true
+false true true true
+jack wendy null
+jack null null
+ronald ronald false
+true true true false
+jack wendy null
+jack null null
+ronald ronald false
+2: 0 1 1
+3: 0 1 2
+There are 0 occurrences of 58 in the multiset
+There are 536870912 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of 58 in the multiset
+There are 633825300114114700748351602688 occurrences of null in the multiset
+Map===
+|s|=1 |u|=1
+s[1]=123 u[1]=40
+|S|=1 |U|=1
+S[1]=123 U[1]=41
+Seq===
+|s|=2 |u|=2
+123 42, 123 42, 123 42
+|s|=2 |u|=2
+123 43, 123 43, 123 43
+|s|=2 |u|=2
+123 44, 123 44, 123 44
+Multiset===
+|s|=2 |u|=4
+1 3
+|s|=2 |u|=4
+1 3
diff --git a/Test/unicodechars/comp/NativeNumbers.dfy b/Test/unicodechars/comp/NativeNumbers.dfy
new file mode 100644
index 00000000000..764b4b3b384
--- /dev/null
+++ b/Test/unicodechars/comp/NativeNumbers.dfy
@@ -0,0 +1,9 @@
+// Skip JavaScript because JavaScript doesn't have the same native types
+
+// RUN: %dafny /compile:0 /verifyAllModules /unicodeChar:1 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /spillTargetCode:2 /compileTarget:py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+include "../../comp/NativeNumbers.dfy"
\ No newline at end of file
diff --git a/Test/unicodechars/comp/NativeNumbers.dfy.expect b/Test/unicodechars/comp/NativeNumbers.dfy.expect
new file mode 100644
index 00000000000..b0fc6754f84
--- /dev/null
+++ b/Test/unicodechars/comp/NativeNumbers.dfy.expect
@@ -0,0 +1,338 @@
+
+Dafny program verifier finished with 25 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+Casting:
+
+Small numbers:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+5 5 5 5 5 5 5 5 5
+6 6 6 6 6 6 6 6 6
+7 7 7 7 7 7 7 7 7
+8 8 8 8 8 8 8 8 8
+
+Large unsigned numbers:
+255 255 255 255 255 255 255 255
+65535 65535 65535 65535 65535 65535
+4294967295 4294967295 4294967295 4294967295
+18446744073709551615 18446744073709551615
+
+Int to large unsigned:
+255 65535 4294967295 18446744073709551615
+
+Cast from cardinality operator:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+
+Characters:
+'C' 67 67 67 67 67 67 67 67 67
+0 127 32767 65535 65535 255 65535 65535 65535
+
+Defaults:
+
+0 0 0 0 0 0 0 0 0
+
+Byte arithmetic:
+
+20 30
+10 10 18
+
+Short arithmetic:
+
+20 30
+10 10 18
+
+Bitvectors:
+
+0 3 4 1
+
+Comparison to zero:
+
+int8:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int16:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int32:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int64:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint8:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint16:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint32:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint64:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+
+
+Dafny program verifier did not attempt verification
+Casting:
+
+Small numbers:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+5 5 5 5 5 5 5 5 5
+6 6 6 6 6 6 6 6 6
+7 7 7 7 7 7 7 7 7
+8 8 8 8 8 8 8 8 8
+
+Large unsigned numbers:
+255 255 255 255 255 255 255 255
+65535 65535 65535 65535 65535 65535
+4294967295 4294967295 4294967295 4294967295
+18446744073709551615 18446744073709551615
+
+Int to large unsigned:
+255 65535 4294967295 18446744073709551615
+
+Cast from cardinality operator:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+
+Characters:
+'C' 67 67 67 67 67 67 67 67 67
+0 127 32767 65535 65535 255 65535 65535 65535
+
+Defaults:
+
+0 0 0 0 0 0 0 0 0
+
+Byte arithmetic:
+
+20 30
+10 10 18
+
+Short arithmetic:
+
+20 30
+10 10 18
+
+Bitvectors:
+
+0 3 4 1
+
+Comparison to zero:
+
+int8:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int16:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int32:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int64:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint8:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint16:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint32:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint64:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+
+
+Dafny program verifier did not attempt verification
+Casting:
+
+Small numbers:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+5 5 5 5 5 5 5 5 5
+6 6 6 6 6 6 6 6 6
+7 7 7 7 7 7 7 7 7
+8 8 8 8 8 8 8 8 8
+
+Large unsigned numbers:
+255 255 255 255 255 255 255 255
+65535 65535 65535 65535 65535 65535
+4294967295 4294967295 4294967295 4294967295
+18446744073709551615 18446744073709551615
+
+Int to large unsigned:
+255 65535 4294967295 18446744073709551615
+
+Cast from cardinality operator:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+
+Characters:
+'C' 67 67 67 67 67 67 67 67 67
+0 127 32767 65535 65535 255 65535 65535 65535
+
+Defaults:
+
+0 0 0 0 0 0 0 0 0
+
+Byte arithmetic:
+
+20 30
+10 10 18
+
+Short arithmetic:
+
+20 30
+10 10 18
+
+Bitvectors:
+
+0 3 4 1
+
+Comparison to zero:
+
+int8:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int16:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int32:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int64:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint8:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint16:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint32:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint64:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+
+
+Dafny program verifier did not attempt verification
+Casting:
+
+Small numbers:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+5 5 5 5 5 5 5 5 5
+6 6 6 6 6 6 6 6 6
+7 7 7 7 7 7 7 7 7
+8 8 8 8 8 8 8 8 8
+
+Large unsigned numbers:
+255 255 255 255 255 255 255 255
+65535 65535 65535 65535 65535 65535
+4294967295 4294967295 4294967295 4294967295
+18446744073709551615 18446744073709551615
+
+Int to large unsigned:
+255 65535 4294967295 18446744073709551615
+
+Cast from cardinality operator:
+0 0 0 0 0 0 0 0 0
+1 1 1 1 1 1 1 1 1
+2 2 2 2 2 2 2 2 2
+3 3 3 3 3 3 3 3 3
+4 4 4 4 4 4 4 4 4
+
+Characters:
+'C' 67 67 67 67 67 67 67 67 67
+0 127 32767 65535 65535 255 65535 65535 65535
+
+Defaults:
+
+0 0 0 0 0 0 0 0 0
+
+Byte arithmetic:
+
+20 30
+10 10 18
+
+Short arithmetic:
+
+20 30
+10 10 18
+
+Bitvectors:
+
+0 3 4 1
+
+Comparison to zero:
+
+int8:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int16:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int32:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+int64:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint8:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint16:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint32:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+uint64:
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+
diff --git a/Test/unicodechars/comp/Numbers.dfy b/Test/unicodechars/comp/Numbers.dfy
new file mode 100644
index 00000000000..2c9170fe4d7
--- /dev/null
+++ b/Test/unicodechars/comp/Numbers.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:0 /verifyAllModules /unicodeChar:1 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+include "../../comp/Numbers.dfy"
\ No newline at end of file
diff --git a/Test/unicodechars/comp/Numbers.dfy.expect b/Test/unicodechars/comp/Numbers.dfy.expect
new file mode 100644
index 00000000000..6fa2f59f340
--- /dev/null
+++ b/Test/unicodechars/comp/Numbers.dfy.expect
@@ -0,0 +1,567 @@
+
+Dafny program verifier finished with 59 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+0
+0
+3
+-5
+2147483647 (aka C# int.MaxValue)
+2147483648 (aka 2^31)
+2147483649
+4294967295 (aka C# uint.MaxValue)
+4294967296 (aka 2^32)
+9007199254740991 (aka JavaScript Number.MAX_SAFE_INTEGER)
+9007199254740992 (aka 2^53)
+-9007199254740991 (aka JavaScript Number.MIN_SAFE_INTEGER)
+-9007199254740992
+9223372036854775807 (aka C# long.MaxValue)
+9223372036854775808 (aka 2^63)
+9223372036854775809
+18446744073709551615 (aka C# ulong.MaxValue)
+18446744073709551616 (aka 2^64)
+1267650600228229401496703205376 (aka 2^100)
+170141183460469231731687303715884105727 (aka M_39)
+0.0
+0.0
+3.0
+-5.0
+3.14
+-2.71
+1000000000.0 (aka a billion)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+17014118346046923173168730371588410572.7 (aka 1/10 of M_39)
+0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001 (aka 1/googol)
+35 27 -27
+124 -124
+-124 124
+'g' 'Q' '2'
+7 3 31
+-8 1 -31
+-7 3 31
+8 1 -31
+0 0 0
+0 0 0
+uint8:  10:1 0:231
+uint16: 2848:7 0:65511
+uint32: 186737707:10 0:4294967271
+uint64: 802032351030850069:4 0:18446744073709551591
+via real: 7:12 -8:1 -7:12 8:1
+int:      7:12 -8:1 -7:12 8:1 -12:0 12:0
+int8:     7:12 -8:1 -7:12 8:1 -12:0 12:0
+int16:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int32:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int64:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+0.2
+35.2 27.2 -27.2
+124.8 -124.8
+-124.8 124.8
+(312.0 / 40.0) (1248.0 / 40.0)
+(-312.0 / 40.0) (-1248.0 / 40.0)
+(-312.0 / 40.0) (1248.0 / 40.0)
+(312.0 / 40.0) (-1248.0 / 40.0)
+0.0 0.0 0.0 
+120.0 120.0 (24.0 / 3.0) (-24.0 / 3.0) 
+123.4567 -123.4567 0.1234 -0.1234 (24.0 / 30.0) 
+0.2 0.02 0.00002 
+-0.2 -0.02 -0.00002 
+(20.0 / 3.0) (-20.0 / 3.0) (-20.0 / 3.0) (20.0 / 3.0) 
+0.0 0.0 0.81 0.81 (8100.0 / 8100.0)
+true false
+0 2 2 2
+0 3 6 46
+0 1 36 2116
+0 0 0 0
+29 2 2 4294967283 2
+29 2 2 9007199254740979 2
+0 0 0 9
+0 0 0 9
+0 0 0 9
+0 4294967295 1267650600228229401496703205375 6
+8 4
+18 72 4
+0
+200 300
+100 100 18
+2
+-2
+-2
+2
+0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
+1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
+42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
+int:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+NativeType:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+false true false true
+true false true false
+false true false true
+true false true false
+20 23 23 88 880
+
+Dafny program verifier did not attempt verification
+0
+0
+3
+-5
+2147483647 (aka C# int.MaxValue)
+2147483648 (aka 2^31)
+2147483649
+4294967295 (aka C# uint.MaxValue)
+4294967296 (aka 2^32)
+9007199254740991 (aka JavaScript Number.MAX_SAFE_INTEGER)
+9007199254740992 (aka 2^53)
+-9007199254740991 (aka JavaScript Number.MIN_SAFE_INTEGER)
+-9007199254740992
+9223372036854775807 (aka C# long.MaxValue)
+9223372036854775808 (aka 2^63)
+9223372036854775809
+18446744073709551615 (aka C# ulong.MaxValue)
+18446744073709551616 (aka 2^64)
+1267650600228229401496703205376 (aka 2^100)
+170141183460469231731687303715884105727 (aka M_39)
+0.0
+0.0
+3.0
+-5.0
+3.14
+-2.71
+1000000000.0 (aka a billion)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+17014118346046923173168730371588410572.7 (aka 1/10 of M_39)
+0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001 (aka 1/googol)
+35 27 -27
+124 -124
+-124 124
+'g' 'Q' '2'
+7 3 31
+-8 1 -31
+-7 3 31
+8 1 -31
+0 0 0
+0 0 0
+uint8:  10:1 0:231
+uint16: 2848:7 0:65511
+uint32: 186737707:10 0:4294967271
+uint64: 802032351030850069:4 0:18446744073709551591
+via real: 7:12 -8:1 -7:12 8:1
+int:      7:12 -8:1 -7:12 8:1 -12:0 12:0
+int8:     7:12 -8:1 -7:12 8:1 -12:0 12:0
+int16:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int32:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int64:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+0.2
+35.2 27.2 -27.2
+124.8 -124.8
+-124.8 124.8
+(312.0 / 40.0) (1248.0 / 40.0)
+(-312.0 / 40.0) (-1248.0 / 40.0)
+(-312.0 / 40.0) (1248.0 / 40.0)
+(312.0 / 40.0) (-1248.0 / 40.0)
+0.0 0.0 0.0 
+120.0 120.0 (24.0 / 3.0) (-24.0 / 3.0) 
+123.4567 -123.4567 0.1234 -0.1234 (24.0 / 30.0) 
+0.2 0.02 0.00002 
+-0.2 -0.02 -0.00002 
+(20.0 / 3.0) (-20.0 / 3.0) (-20.0 / 3.0) (20.0 / 3.0) 
+0.0 0.0 0.81 0.81 (8100.0 / 8100.0)
+true false
+0 2 2 2
+0 3 6 46
+0 1 36 2116
+0 0 0 0
+29 2 2 4294967283 2
+29 2 2 9007199254740979 2
+0 0 0 9
+0 0 0 9
+0 0 0 9
+0 4294967295 1267650600228229401496703205375 6
+8 4
+18 72 4
+0
+200 300
+100 100 18
+2
+-2
+-2
+2
+0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
+1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
+42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
+int:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+NativeType:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+false true false true
+true false true false
+false true false true
+true false true false
+20 23 23 88 880
+
+Dafny program verifier did not attempt verification
+0
+0
+3
+-5
+2147483647 (aka C# int.MaxValue)
+2147483648 (aka 2^31)
+2147483649
+4294967295 (aka C# uint.MaxValue)
+4294967296 (aka 2^32)
+9007199254740991 (aka JavaScript Number.MAX_SAFE_INTEGER)
+9007199254740992 (aka 2^53)
+-9007199254740991 (aka JavaScript Number.MIN_SAFE_INTEGER)
+-9007199254740992
+9223372036854775807 (aka C# long.MaxValue)
+9223372036854775808 (aka 2^63)
+9223372036854775809
+18446744073709551615 (aka C# ulong.MaxValue)
+18446744073709551616 (aka 2^64)
+1267650600228229401496703205376 (aka 2^100)
+170141183460469231731687303715884105727 (aka M_39)
+0.0
+0.0
+3.0
+-5.0
+3.14
+-2.71
+1000000000.0 (aka a billion)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+17014118346046923173168730371588410572.7 (aka 1/10 of M_39)
+0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001 (aka 1/googol)
+35 27 -27
+124 -124
+-124 124
+'g' 'Q' '2'
+7 3 31
+-8 1 -31
+-7 3 31
+8 1 -31
+0 0 0
+0 0 0
+uint8:  10:1 0:231
+uint16: 2848:7 0:65511
+uint32: 186737707:10 0:4294967271
+uint64: 802032351030850069:4 0:18446744073709551591
+via real: 7:12 -8:1 -7:12 8:1
+int:      7:12 -8:1 -7:12 8:1 -12:0 12:0
+int8:     7:12 -8:1 -7:12 8:1 -12:0 12:0
+int16:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int32:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int64:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+0.2
+35.2 27.2 -27.2
+124.8 -124.8
+-124.8 124.8
+7.8 31.2
+-7.8 -31.2
+-7.8 31.2
+7.8 -31.2
+0.0 0.0 0.0 
+120.0 120.0 8.0 -8.0 
+123.4567 -123.4567 0.1234 -0.1234 0.8 
+0.2 0.02 0.00002 
+-0.2 -0.02 -0.00002 
+(20.0 / 3.0) (-20.0 / 3.0) (-20.0 / 3.0) (20.0 / 3.0) 
+0.0 0.0 0.81 0.81 1.0
+true false
+0 2 2 2
+0 3 6 46
+0 1 36 2116
+0 0 0 0
+29 2 2 4294967283 2
+29 2 2 9007199254740979 2
+0 0 0 9
+0 0 0 9
+0 0 0 9
+0 4294967295 1267650600228229401496703205375 6
+8 4
+18 72 4
+0
+200 300
+100 100 18
+2
+-2
+-2
+2
+0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
+1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
+42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
+int:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+NativeType:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+false true false true
+true false true false
+false true false true
+true false true false
+20 23 23 88 880
+
+Dafny program verifier did not attempt verification
+0
+0
+3
+-5
+2147483647 (aka C# int.MaxValue)
+2147483648 (aka 2^31)
+2147483649
+4294967295 (aka C# uint.MaxValue)
+4294967296 (aka 2^32)
+9007199254740991 (aka JavaScript Number.MAX_SAFE_INTEGER)
+9007199254740992 (aka 2^53)
+-9007199254740991 (aka JavaScript Number.MIN_SAFE_INTEGER)
+-9007199254740992
+9223372036854775807 (aka C# long.MaxValue)
+9223372036854775808 (aka 2^63)
+9223372036854775809
+18446744073709551615 (aka C# ulong.MaxValue)
+18446744073709551616 (aka 2^64)
+1267650600228229401496703205376 (aka 2^100)
+170141183460469231731687303715884105727 (aka M_39)
+0.0
+0.0
+3.0
+-5.0
+3.14
+-2.71
+1000000000.0 (aka a billion)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+17014118346046923173168730371588410572.7 (aka 1/10 of M_39)
+0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001 (aka 1/googol)
+35 27 -27
+124 -124
+-124 124
+'g' 'Q' '2'
+7 3 31
+-8 1 -31
+-7 3 31
+8 1 -31
+0 0 0
+0 0 0
+uint8:  10:1 0:231
+uint16: 2848:7 0:65511
+uint32: 186737707:10 0:4294967271
+uint64: 802032351030850069:4 0:18446744073709551591
+via real: 7:12 -8:1 -7:12 8:1
+int:      7:12 -8:1 -7:12 8:1 -12:0 12:0
+int8:     7:12 -8:1 -7:12 8:1 -12:0 12:0
+int16:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int32:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int64:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+0.2
+35.2 27.2 -27.2
+124.8 -124.8
+-124.8 124.8
+(312.0 / 40.0) (1248.0 / 40.0)
+(-312.0 / 40.0) (-1248.0 / 40.0)
+(-312.0 / 40.0) (1248.0 / 40.0)
+(312.0 / 40.0) (-1248.0 / 40.0)
+0.0 0.0 0.0 
+120.0 120.0 (24.0 / 3.0) (-24.0 / 3.0) 
+123.4567 -123.4567 0.1234 -0.1234 (24.0 / 30.0) 
+0.2 0.02 0.00002 
+-0.2 -0.02 -0.00002 
+(20.0 / 3.0) (-20.0 / 3.0) (-20.0 / 3.0) (20.0 / 3.0) 
+0.0 0.0 0.81 0.81 (8100.0 / 8100.0)
+true false
+0 2 2 2
+0 3 6 46
+0 1 36 2116
+0 0 0 0
+29 2 2 4294967283 2
+29 2 2 9007199254740979 2
+0 0 0 9
+0 0 0 9
+0 0 0 9
+0 4294967295 1267650600228229401496703205375 6
+8 4
+18 72 4
+0
+200 300
+100 100 18
+2
+-2
+-2
+2
+0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
+1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
+42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
+int:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+NativeType:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+false true false true
+true false true false
+false true false true
+true false true false
+20 23 23 88 880
+
+Dafny program verifier did not attempt verification
+0
+0
+3
+-5
+2147483647 (aka C# int.MaxValue)
+2147483648 (aka 2^31)
+2147483649
+4294967295 (aka C# uint.MaxValue)
+4294967296 (aka 2^32)
+9007199254740991 (aka JavaScript Number.MAX_SAFE_INTEGER)
+9007199254740992 (aka 2^53)
+-9007199254740991 (aka JavaScript Number.MIN_SAFE_INTEGER)
+-9007199254740992
+9223372036854775807 (aka C# long.MaxValue)
+9223372036854775808 (aka 2^63)
+9223372036854775809
+18446744073709551615 (aka C# ulong.MaxValue)
+18446744073709551616 (aka 2^64)
+1267650600228229401496703205376 (aka 2^100)
+170141183460469231731687303715884105727 (aka M_39)
+0.0
+0.0
+3.0
+-5.0
+3.14
+-2.71
+1000000000.0 (aka a billion)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+0.0000000000667408 (aka G)
+17014118346046923173168730371588410572.7 (aka 1/10 of M_39)
+0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001 (aka 1/googol)
+35 27 -27
+124 -124
+-124 124
+'g' 'Q' '2'
+7 3 31
+-8 1 -31
+-7 3 31
+8 1 -31
+0 0 0
+0 0 0
+uint8:  10:1 0:231
+uint16: 2848:7 0:65511
+uint32: 186737707:10 0:4294967271
+uint64: 802032351030850069:4 0:18446744073709551591
+via real: 7:12 -8:1 -7:12 8:1
+int:      7:12 -8:1 -7:12 8:1 -12:0 12:0
+int8:     7:12 -8:1 -7:12 8:1 -12:0 12:0
+int16:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int32:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+int64:    7:12 -8:1 -7:12 8:1 -12:0 12:0
+0.2
+35.2 27.2 -27.2
+124.8 -124.8
+-124.8 124.8
+7.8 31.2
+-7.8 -31.2
+-7.8 31.2
+7.8 -31.2
+0.0 0.0 0.0 
+120.0 120.0 8.0 -8.0 
+123.4567 -123.4567 0.1234 -0.1234 0.8 
+0.2 0.02 0.00002 
+-0.2 -0.02 -0.00002 
+(20.0 / 3.0) (-20.0 / 3.0) (-20.0 / 3.0) (20.0 / 3.0) 
+0.0 0.0 0.81 0.81 1.0
+true false
+0 2 2 2
+0 3 6 46
+0 1 36 2116
+0 0 0 0
+29 2 2 4294967283 2
+29 2 2 9007199254740979 2
+0 0 0 9
+0 0 0 9
+0 0 0 9
+0 4294967295 1267650600228229401496703205375 6
+8 4
+18 72 4
+0
+200 300
+100 100 18
+2
+-2
+-2
+2
+0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
+1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
+42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
+int:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+NativeType:
+-42	 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+0	 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
+23	 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+120 120.0 120 120 120 'x'
+120 120.0 120 120 120 'x'
+120 120
+false true false true
+true false true false
+false true false true
+true false true false
+20 23 23 88 880