Deprecate unicode-char

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -1993,8 +1993,9 @@ protected override void EmitActualTypeArgs(List<Type> typeArgs, IToken tok, Conc
 
     protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) {
       var wStmts = wr.Fork();
-      var typeArgs = arg.Type.AsArrowType == null ? "" : $"<{TypeName(arg.Type, wr, null, null)}>";
-      var suffix = arg.Type.IsStringType && UnicodeCharEnabled ? ".ToVerbatimString(false)" : "";
+      var type = DatatypeWrapperEraser.SimplifyTypeAndTrimNewtypes(Options, arg.Type);
+      var typeArgs = type.AsArrowType == null ? "" : $"<{TypeName(type, wr, null, null)}>";
+      var suffix = type.IsStringType && UnicodeCharEnabled ? ".ToVerbatimString(false)" : "";
       wr.WriteLine($"{DafnyHelpersClass}.Print{typeArgs}(({Expr(arg, false, wStmts)}){suffix});");
     }
 

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -1903,7 +1903,7 @@ protected override void EmitMultiAssignment(List<Expression> lhsExprs, List<ILva
     }
 
     protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) {
-      var isString = arg.Type.IsStringType;
+      var isString = DatatypeWrapperEraser.SimplifyTypeAndTrimNewtypes(Options, arg.Type).IsStringType;
       var wStmts = wr.Fork();
       if (isString && UnicodeCharEnabled) {
         wr.Write("_dafny.Print(");

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -1142,7 +1142,7 @@ protected override void EmitActualTypeArgs(List<Type> typeArgs, IToken tok, Conc
     // ----- Statements -------------------------------------------------------------
 
     protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) {
-      bool isString = arg.Type.NormalizeToAncestorType().IsStringType;
+      bool isString = DatatypeWrapperEraser.SimplifyTypeAndTrimNewtypes(Options, arg.Type).IsStringType;
       bool isStringLiteral = arg is StringLiteralExpr;
       bool isGeneric = arg.Type.NormalizeToAncestorType().AsSeqType is { Arg.IsTypeParameter: true };
       var wStmts = wr.Fork();

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -862,7 +862,7 @@ protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) {
     }
 
     private void EmitToString(ConcreteSyntaxTree wr, Expression arg, ConcreteSyntaxTree wStmts) {
-      if (UnicodeCharEnabled && arg.Type.IsStringType) {
+      if (UnicodeCharEnabled && DatatypeWrapperEraser.SimplifyTypeAndTrimNewtypes(Options, arg.Type).IsStringType) {
         TrParenExpr(arg, wr, false, wStmts);
         wr.Write(".VerbatimString(False)");
       } else {

Source/DafnyCore/Generic/ErrorReporter.cs

@@ -154,6 +154,16 @@ public void Warning(MessageSource source, string errorId, IToken tok, string msg
     Message(source, ErrorLevel.Warning, errorId, tok, msg);
   }
 
+  public void Deprecated(MessageSource source, string errorId, IToken tok, string msg) {
+    Contract.Requires(tok != null);
+    Contract.Requires(msg != null);
+    if (Options.DeprecationNoise != 0) {
+      Warning(source, errorId, tok, msg);
+    } else {
+      Info(source, tok, msg, errorId);
+    }
+  }
+
   public void Deprecated(MessageSource source, Enum errorId, IToken tok, string msg) {
     Contract.Requires(tok != null);
     Contract.Requires(msg != null);

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -184,7 +184,7 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
 js - Compile to JavaScript.
 java - Compile to Java.
 py - Compile to Python.
-cpp - Compile to C++.
+cpp - (experimental) Compile to C++.
 
 Note that the C++ backend has various limitations (see Docs/Compilation/Cpp.md). This includes lack of support for BigIntegers (aka int), most higher order functions, and advanced features like traits or co-inductive types.".TrimStart()
   ) {
@@ -195,6 +195,7 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
     @"
 false - The char type represents any UTF-16 code unit.
 true - The char type represents any Unicode scalar value.".TrimStart()) {
+    IsHidden = true
   };
 
   public static readonly Option<bool> AllowAxioms = new("--allow-axioms", () => false,

Source/DafnyDriver/CliCompilation.cs

@@ -10,6 +10,7 @@
 using System.Threading.Tasks;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
@@ -152,6 +153,11 @@ public void Start() {
   public bool VerifiedAssertions { get; private set; }
 
   public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed) {
+    if (!Options.Get(CommonOptionBag.UnicodeCharacters) && Options.Backend is not CppBackend) {
+      Compilation.Reporter.Deprecated(MessageSource.Verifier, "unicodeCharDeprecated", Token.Cli,
+        "the option unicode-char has been deprecated.");
+    }
+
     var canVerifyResults = new Dictionary<ICanVerify, CliCanVerifyState>();
     using var subscription = Compilation.Updates.Subscribe(ev => {
 

Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs

@@ -714,7 +714,8 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
       }
 
       // compile the program into an assembly
-      var (compiledCorrectly, compilationResult) = await compiler.CompileTargetProgram(dafnyProgramName, targetProgramText, callToMain, targetPaths.Filename, otherFileNames,
+      var (compiledCorrectly, compilationResult) = await compiler.CompileTargetProgram(dafnyProgramName,
+        targetProgramText, callToMain, targetPaths.Filename, otherFileNames,
         hasMain && options.RunAfterCompile, outputWriter);
       if (compiledCorrectly && options.RunAfterCompile) {
         if (hasMain) {

Source/DafnyStandardLibraries/src/Std/Unicode/UnicodeStrings.dfy

@@ -13,7 +13,7 @@
   * of the `char` type and hence the `string` type,
   * this module must be implemented differently for each option value.
   * Currently, the only available implementation is for `--unicode-char:true`,
-  * and the implementation for `--unicode-char:false` is upcoming.
+  * and the implementation for `--unicode-char false` is upcoming.
   *
   * If you also want to maintain code that works for either `--unicode-char` value,
   * implement your logic in an abstract module that imports this one.

Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTestsOption.dfy

@@ -1,11 +1,11 @@
 // RUN: %verify "%s" > "%t"
-// RUN: %translate cs %args %s --include-runtime --include-test-runner --unicode-char false --no-verify --output %S/Output/manual/program.cs >> "%t"
+// RUN: %translate cs %args %s --include-runtime --include-test-runner --no-verify --output %S/Output/manual/program.cs >> "%t"
 // RUN: ! dotnet run -v q --property WarningLevel=0 --project %S/RunAllTests.csproj >> "%t"
-// RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:cs "%s" >> "%t"
-// RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:java "%s" >> "%t"
-// RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:go "%s" >> "%t"
-// RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:js "%s" >> "%t"
-// RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:py "%s" >> "%t"
+// RUN: ! %baredafny test %args --no-verify --target:cs "%s" >> "%t"
+// RUN: ! %baredafny test %args --no-verify --target:java "%s" >> "%t"
+// RUN: ! %baredafny test %args --no-verify --target:go "%s" >> "%t"
+// RUN: ! %baredafny test %args --no-verify --target:js "%s" >> "%t"
+// RUN: ! %baredafny test %args --no-verify --target:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t" 
 
 include "../../exceptions/VoidOutcomeDt.dfy"

Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTestsOption.dfy.expect

@@ -11,7 +11,7 @@ Passing3: PASSED
 Failing2: FAILED
 	RunAllTestsOption.dfy(31,2): expectation violation
 FailingReturnValue: FAILED
-	VoidOutcome.VoidFailure(Whoopsie)
+	VoidOutcome.VoidFailure("Whoopsie")
 [Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
 
 
@@ -25,7 +25,7 @@ Passing3: PASSED
 Failing2: FAILED
 	RunAllTestsOption.dfy(31,2): expectation violation
 FailingReturnValue: FAILED
-	VoidOutcome.VoidFailure(Whoopsie)
+	VoidOutcome.VoidFailure("Whoopsie")
 [Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
 
 
@@ -39,7 +39,7 @@ Passing3: PASSED
 Failing2: FAILED
 	RunAllTestsOption.dfy(31,2): expectation violation
 FailingReturnValue: FAILED
-	VoidOutcome.VoidFailure(Whoopsie)
+	VoidOutcome.VoidFailure("Whoopsie")
 [Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
 
 
@@ -53,7 +53,7 @@ Passing3: PASSED
 Failing2: FAILED
 	RunAllTestsOption.dfy(31,2): expectation violation
 FailingReturnValue: FAILED
-	VoidOutcome.VoidFailure(Whoopsie)
+	VoidOutcome.VoidFailure("Whoopsie")
 [Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
 
 
@@ -67,7 +67,7 @@ Passing3: PASSED
 Failing2: FAILED
 	RunAllTestsOption.dfy(31,2): expectation violation
 FailingReturnValue: FAILED
-	VoidOutcome.VoidFailure(Whoopsie)
+	VoidOutcome.VoidFailure("Whoopsie")
 [Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
 
 
@@ -81,6 +81,6 @@ Passing3: PASSED
 Failing2: FAILED
 	RunAllTestsOption.dfy(31,2): expectation violation
 FailingReturnValue: FAILED
-	VoidOutcome.VoidFailure(Whoopsie)
+	VoidOutcome.VoidFailure("Whoopsie")
 [Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy

@@ -1,11 +1,11 @@
 
 // Generating and Running Block-Based Tests:
 // RUN: %baredafny generate-tests %args Block %S/TestGenerationNoInliningEnumerativeDefinitions.dfy > %t-tests.dfy
-// RUN: %baredafny test %args --unicode-char:false --target:cs "%t-tests.dfy" >> "%t"
+// RUN: %baredafny test %args --target:cs "%t-tests.dfy" >> "%t"
 
 // Generating and Running Path-Based Tests:
 // RUN: %baredafny generate-tests %args Path %S/TestGenerationNoInliningEnumerativeDefinitions.dfy > %t-tests.dfy
-// RUN: %baredafny test %args --unicode-char:false --target:cs "%t-tests.dfy" >> "%t"
+// RUN: %baredafny test %args --target:cs "%t-tests.dfy" >> "%t"
 
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: .*Dafny program verifier finished with 2 verified, 0 errors*

Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationWithInliningQuantifiedDefinitions.dfy

@@ -1,6 +1,6 @@
 // Generating and Running Path-Based Tests:
 // RUN: %baredafny generate-tests %args Path %S/TestGenerationWithInliningQuantifiedDefinitions.dfy > %t-tests.dfy
-// RUN: %baredafny test %args --unicode-char:false --target:cs "%t-tests.dfy" >> "%t"
+// RUN: %baredafny test %args --target:cs "%t-tests.dfy" >> "%t"
 
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: .*Dafny program verifier finished with 5 verified, 0 errors*

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/arrays.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/bit-vectors.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint64 = i:int | 0 <= i < 0x10000000000000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/class.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/const.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 module Holder {
   const x:bool := false

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/datatypes.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/generic.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 class Test<T> {
   var t:T

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/hello.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 method Main() {
   print "Hello world\n";

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/ints.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype sbyte = i:int | -0x80 <= i < 0x80
 newtype byte = i:int | 0 <= i < 0x100

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/maps.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/recursion.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/returns.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint64 = i:int | 0 <= i < 0x10000000000000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/seqs.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint8 = i:int | 0 <= i < 0x100
 newtype uint32 = i:int | 0 <= i < 0x100000000

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/sets.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/while.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --allow-deprecation --unicode-char false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy

@@ -1,5 +1,4 @@
-// NONUNIFORM: https://github.com/dafny-lang/dafny/issues/2582
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment
 
 method LinearSearch(a: array<int>, key: int) returns (n: nat)
   ensures 0 <= n <= a.Length

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy.expect

@@ -5,8 +5,8 @@
 [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 
+'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 
@@ -18,34 +18,34 @@ 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 
+'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 
+('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)
+('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
+'D' 'D' 'D' 
+'D' 'D' 'D' 
+'D' 'D' 'D' 
+'D' 'D' 'r' ('D', 'D', 'r')
+'D' 'D' 'r'
 [19, 18, 9, 8]
  true
  false
@@ -81,14 +81,14 @@ hello [0, 1, 2, 3, 4] [2, 2, 2, 2, 2]
 [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
-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]
-DDDDDDDDDDagggggaggg
+['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
+'D' 'k' 'n'
 false false
 true true
 false false

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Collections.dfy

@@ -1,5 +1,5 @@
 // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation
 
 method Main() {
   Sets();

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Collections.dfy.expect

@@ -12,7 +12,7 @@ Sets: {} {17, 82} {12, 17}
   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}}
+{{}, {'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}
@@ -48,7 +48,7 @@ Sequences: [] [17, 82, 17, 82] [12, 17]
   membership: false true true
 Bound Bound Bound Bound Bound Bound
 ed ed ed ed ed ed
-e e e e e e
+'e' 'e' 'e' 'e' 'e' 'e'
 hello
 hEllo
 [2, 4, 6, 8, 10]