fix: Default to /unicodeChar:0 in legacy CLI as well (#3635)

This was accidentally missed from #3623. Mostly I just updated expect files or added `/unicodeChar:0` where the testing coverage wasn't really relevant, but in a few cases I added `/unicodeChar:1` variants under `Test/unicodechars` where testing both modes was better. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · Feb 27, 2023 · a424583 · a424583
2 parents fb88ca7 + 04162f4
commit a424583
Show file tree

Hide file tree

Showing 68 changed files with 574 additions and 153 deletions.
diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
@@ -64,7 +64,7 @@ datatype with a single non-ghost constructor that has a single
  RegisterLegacyUi(CommonOptionBag.Output, ParseFileInfo, "Compilation options", "out");
  RegisterLegacyUi(CommonOptionBag.UnicodeCharacters, ParseBoolean, "Language feature selection", "unicodeChar", @"
 0 - The char type represents any UTF-16 code unit.
-1 (default) - The char type represents any Unicode scalar value.".TrimStart());
+1 (default) - The char type represents any Unicode scalar value.".TrimStart(), defaultValue: true);
  RegisterLegacyUi(CommonOptionBag.Plugin, ParseStringElement, "Plugins", defaultValue: new List<string>());
  RegisterLegacyUi(CommonOptionBag.Prelude, ParseFileInfo, "Input configuration", "dprelude");
 

diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs
@@ -1077,7 +1077,7 @@ class C {
  }
 
  method test(c: C?) {
- assert c == null || c.c1 != c.c2 || c.c1 != '\u1023';
+ assert c == null || c.c1 != c.c2 || c.c1 != '\U{1023}';
  }
  }".TrimStart();
  var documentItem = CreateTestDocument(source);

diff --git a/Test/allocated1/dafny0/Char.dfy b/Test/allocated1/dafny0/Char.dfy
@@ -1,3 +1,3 @@
-// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /unicodeChar:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 include "../../dafny0/Char.dfy"
diff --git a/Test/allocated1/dafny0/Strings.dfy b/Test/allocated1/dafny0/Strings.dfy
@@ -1,3 +1,3 @@
-// RUN: %dafny /verifyAllModules /allocated:1 /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /verifyAllModules /allocated:1 /compile:3 /unicodeChar:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 include "../../dafny0/Strings.dfy"
diff --git a/Test/allocated1/dafny0/Termination.dfy b/Test/allocated1/dafny0/Termination.dfy
@@ -1,3 +1,3 @@
-// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /unicodeChar:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 include "../../dafny0/Termination.dfy"
diff --git a/Test/c++/arrays.dfy b/Test/c++/arrays.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/bit-vectors.dfy b/Test/c++/bit-vectors.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint64 = i:int | 0 <= i < 0x10000000000000000

diff --git a/Test/c++/class.dfy b/Test/c++/class.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/const.dfy b/Test/c++/const.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module Holder {

diff --git a/Test/c++/datatypes.dfy b/Test/c++/datatypes.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/extern.dfy b/Test/c++/extern.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" ExternDefs.h > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module {:extern "Extern"} Extern {

diff --git a/Test/c++/functions.dfy b/Test/c++/functions.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" ExternDefs.h > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module {:extern "Extern"} Extern {

diff --git a/Test/c++/generic.dfy b/Test/c++/generic.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class Test<T> {

diff --git a/Test/c++/hello.dfy b/Test/c++/hello.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {

diff --git a/Test/c++/ints.dfy b/Test/c++/ints.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype sbyte = i:int | -0x80 <= i < 0x80

diff --git a/Test/c++/maps.dfy b/Test/c++/maps.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/recursion.dfy b/Test/c++/recursion.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/returns.dfy b/Test/c++/returns.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint64 = i:int | 0 <= i < 0x10000000000000000

diff --git a/Test/c++/seqs.dfy b/Test/c++/seqs.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint8 = i:int | 0 <= i < 0x100

diff --git a/Test/c++/sets.dfy b/Test/c++/sets.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/tuple.dfy b/Test/c++/tuple.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp ExternDefs.h "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 ExternDefs.h "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/while.dfy b/Test/c++/while.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp "%s" > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/comp/Collections.dfy b/Test/comp/Collections.dfy
@@ -1,9 +1,9 @@
-// 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:js "%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:js "%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/Comprehensions.dfy b/Test/comp/Comprehensions.dfy
@@ -1,9 +1,9 @@
-// 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:js "%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:js "%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/Datatype.dfy.expect b/Test/comp/Datatype.dfy.expect
@@ -18,7 +18,7 @@ Stream.Next
 {Berry.Smultron, Berry.Jordgubb, Berry.Hallon}
 CoBerry.Hjortron true true false
 false
-42 q hello
+42 'q' hello
 1701
 Record.Record(58, true)
 199
@@ -42,7 +42,7 @@ Stream.Next
 {Berry.Smultron, Berry.Jordgubb, Berry.Hallon}
 CoBerry.Hjortron true true false
 false
-42 q hello
+42 'q' hello
 1701
 Record.Record(58, true)
 199
@@ -66,7 +66,7 @@ Stream.Next
 {Berry.Smultron, Berry.Jordgubb, Berry.Hallon}
 CoBerry.Hjortron true true false
 false
-42 q hello
+42 'q' hello
 1701
 Record.Record(58, true)
 199
@@ -90,7 +90,7 @@ Stream.Next
 {Berry.Jordgubb, Berry.Smultron, Berry.Hallon}
 CoBerry.Hjortron true true false
 false
-42 q hello
+42 'q' hello
 1701
 Record.Record(58, true)
 199
@@ -114,7 +114,7 @@ Stream.Next
 {Berry.Hallon, Berry.Smultron, Berry.Jordgubb}
 CoBerry.Hjortron true true false
 false
-42 q hello
+42 'q' hello
 1701
 Record.Record(58, true)
 199

diff --git a/Test/comp/ErasableTypeWrappers.dfy b/Test/comp/ErasableTypeWrappers.dfy
@@ -1,9 +1,9 @@
-// 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:js "%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:js "%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"
 
 datatype SingletonRecord = SingletonRecord(u: int)

diff --git a/Test/comp/ExternDafnyString.dfy b/Test/comp/ExternDafnyString.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/Conversions.java %S/ExternDafnyString.java > "%t"
+// RUN: %dafny /compile:3 /unicodeChar:0 /compileTarget:java "%s" %S/Conversions.java %S/ExternDafnyString.java > "%t"
 // RUN: %diff "%s.expect" "%t"
 // In this example, the extern method obtains a Java string and returns it as a Dafny string.
 

diff --git a/Test/comp/ExternJavaString.dfy b/Test/comp/ExternJavaString.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/Conversions.java %S/ExternJavaString.java > "%t"
+// RUN: %dafny /compile:3 /unicodeChar:0 /compileTarget:java "%s" %S/Conversions.java %S/ExternJavaString.java > "%t"
 // RUN: %diff "%s.expect" "%t"
 // In this example, the extern method obtains a Java string and returns it as such.
 // The Dafny code converts that Java string to a Dafny string.

diff --git a/Test/comp/GoModule.dfy b/Test/comp/GoModule.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 "%s" /compileTarget:go > "%t"
+// RUN: %dafny /compile:3 /unicodeChar:0 /spillTargetCode:2 "%s" /compileTarget:go > "%t"
 // note: putting /compileTarget:go after "%s" overrides user-provided option
 // RUN: %diff "%s.expect" "%t"
 

diff --git a/Test/comp/JsModule.dfy b/Test/comp/JsModule.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 "%s" /compileTarget:js > "%t"
+// RUN: %dafny /compile:3 /unicodeChar:0 "%s" /compileTarget:js > "%t"
 // note: putting /compileTarget:js after "%s" overrides user-provided option
 // RUN: %diff "%s.expect" "%t"
 

diff --git a/Test/comp/MoreAutoInit.dfy.expect b/Test/comp/MoreAutoInit.dfy.expect
@@ -127,7 +127,7 @@ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Co
  ++ [Consts_Compile.Uni.Uni] ++ []
  ** [] ++ [] ++ []
 15
-0-0 0.0-0.0 false-false D-D 0
+0-0 0.0-0.0 false-false 'D'-'D' 0
 0-0 0-0 0-0 0-0 0-0 0-0 0-0 0-0
 0-0 0-0 0-0 0-0 1 1
 0.0-0.0 68.0
@@ -269,7 +269,7 @@ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Co
  ++ [Consts_Compile.Uni.Uni] ++ []
  ** [] ++ [] ++ []
 15
-0-0 0.0-0.0 false-false D-D 0
+0-0 0.0-0.0 false-false 'D'-'D' 0
 0-0 0-0 0-0 0-0 0-0 0-0 0-0 0-0
 0-0 0-0 0-0 0-0 1 1
 0.0-0.0 68.0
@@ -411,7 +411,7 @@ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Co
  ++ [Consts_Compile.Uni.Uni] ++ []
  ** [] ++ [] ++ []
 15
-0-0 0.0-0.0 false-false D-D 0
+0-0 0.0-0.0 false-false 'D'-'D' 0
 0-0 0-0 0-0 0-0 0-0 0-0 0-0 0-0
 0-0 0-0 0-0 0-0 1 1
 0.0-0.0 68.0
@@ -553,7 +553,7 @@ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Co
  ++ [Consts_Compile.Uni.Uni] ++ []
  ** [] ++ [] ++ []
 15
-0-0 0.0-0.0 false-false D-D 0
+0-0 0.0-0.0 false-false 'D'-'D' 0
 0-0 0-0 0-0 0-0 0-0 0-0 0-0 0-0
 0-0 0-0 0-0 0-0 1 1
 0.0-0.0 68.0
@@ -695,7 +695,7 @@ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Consts_Compile.Uni.Uni ++ Co
  ++ [Consts_Compile.Uni.Uni] ++ []
  ** [] ++ [] ++ []
 15
-0-0 0.0-0.0 false-false D-D 0
+0-0 0.0-0.0 false-false 'D'-'D' 0
 0-0 0-0 0-0 0-0 0-0 0-0 0-0 0-0
 0-0 0-0 0-0 0-0 1 1
 0.0-0.0 68.0

diff --git a/Test/comp/Print.dfy b/Test/comp/Print.dfy
@@ -1,8 +1,8 @@
-// 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 /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: %diff "%s.expect" "%t"
 
 // Python salts hashes so they are not deterministic.

diff --git a/Test/comp/TypeParams.dfy.expect b/Test/comp/TypeParams.dfy.expect
@@ -6,7 +6,7 @@ Dafny program verifier did not attempt verification
 null null null null null
 {} multiset{} [] map[] {} map[]
 null null null null
-0 [] Q {} 0 Dt.D0(0)
+0 [] 'Q' {} 0 Dt.D0(0)
 false Color.Orange 42 {} false Dt.D0(false)
 NonemptyList.Atom(0)
 6 7 8 9
@@ -27,7 +27,7 @@ Dafny program verifier did not attempt verification
 null null null null null
 {} multiset{} [] map[] {} map[]
 null null null null
-0 [] Q {} 0 Dt.D0(0)
+0 [] 'Q' {} 0 Dt.D0(0)
 false Color.Orange 42 {} false Dt.D0(false)
 NonemptyList.Atom(0)
 6 7 8 9
@@ -48,7 +48,7 @@ Dafny program verifier did not attempt verification
 null null null null null
 {} multiset{} [] map[] {} map[]
 null null null null
-0 [] Q {} 0 Dt.D0(0)
+0 [] 'Q' {} 0 Dt.D0(0)
 false Color.Orange 42 {} false Dt.D0(false)
 NonemptyList.Atom(0)
 6 7 8 9
@@ -69,7 +69,7 @@ Dafny program verifier did not attempt verification
 null null null null null
 {} multiset{} [] map[] {} map[]
 null null null null
-0 [] Q {} 0 Dt.D0(0)
+0 [] 'Q' {} 0 Dt.D0(0)
 false Color.Orange 42 {} false Dt.D0(false)
 NonemptyList.Atom(0)
 6 7 8 9
@@ -90,7 +90,7 @@ Dafny program verifier did not attempt verification
 null null null null null
 {} multiset{} [] map[] {} map[]
 null null null null
-0 [] Q {} 0 Dt.D0(0)
+0 [] 'Q' {} 0 Dt.D0(0)
 false Color.Orange 42 {} false Dt.D0(false)
 NonemptyList.Atom(0)
 6 7 8 9

diff --git a/Test/comp/compile1quiet/CompileRunQuietly.dfy b/Test/comp/compile1quiet/CompileRunQuietly.dfy
@@ -1,19 +1,19 @@
-// RUN: %dafny /compileTarget:cs "%s" > "%t"
+// RUN: %dafny /unicodeChar:0 /compileTarget:cs "%s" > "%t"
 // RUN: dotnet %S/CompileRunQuietly.dll >> "%t"
 
-// RUN: %dafny /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /unicodeChar:0 /compileTarget:js "%s" >> "%t"
 // RUN: node %S/CompileRunQuietly.js >> "%t"
 
-// RUN: %dafny /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /unicodeChar:0 /compileTarget:go "%s" >> "%t"
 // RUN: %S/CompileRunQuietly >> "%t"
 
-// RUN: %dafny /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /unicodeChar:0 /compileTarget:java "%s" >> "%t"
 // RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileRunQuietly-java CompileRunQuietly >> "%t"
 
-// RUN: %dafny /compileTarget:cpp "%s" >> "%t"
+// RUN: %dafny /unicodeChar:0 /compileTarget:cpp "%s" >> "%t"
 // RUN: %S/CompileRunQuietly.exe >> "%t"
 
-// RUN: %dafny /compileTarget:py "%s" >> "%t"
+// RUN: %dafny /unicodeChar:0 /compileTarget:py "%s" >> "%t"
 // RUN: python3 %S/CompileRunQuietly-py/CompileRunQuietly.py >> "%t"
 
  // RUN: %diff "%s.expect" "%t"