diff --git a/.github/workflows/check-deep-tests-reusable.yml b/.github/workflows/check-deep-tests-reusable.yml
index 72996ae803..eb38ecebc9 100644
--- a/.github/workflows/check-deep-tests-reusable.yml
+++ b/.github/workflows/check-deep-tests-reusable.yml
@@ -1,6 +1,7 @@
 name: Check Deep Tests (Reusable Workflow)
 
 on:
+  workflow_dispatch:
   workflow_call:
 
 jobs:
diff --git a/.github/workflows/check-for-workflow-run.js b/.github/workflows/check-for-workflow-run.js
index 1b0b3d8490..ced1918289 100644
--- a/.github/workflows/check-for-workflow-run.js
+++ b/.github/workflows/check-for-workflow-run.js
@@ -16,13 +16,18 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
   const runFilterDesc = sha ? `${workflow_id} on ${sha}` : workflow_id
   for (const run of result.data.workflow_runs) {
     if ((!sha || run.head_sha === sha)) {
-      if (run.conclusion === "success") {
-        // The SHA is fully tested, exit with success
-        console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
-        return
-      } else if (run.status === "failure" || run.status === "timed_out") {
-        core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
-        return
+      // The status property can be one of: “queued”, “in_progress”, or “completed”.
+      if (run.status === "completed") {
+        // The conclusion property can be one of:
+        // “success”, “failure”, “neutral”, “cancelled”, “skipped”, “timed_out”, or “action_required”.
+        if (run.conclusion === "success") {
+          // The SHA is fully tested, exit with success
+          console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
+          return
+        } else if (run.conclusion === "failure" || run.conclusion === "timed_out") {
+          core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
+          return
+        }
       }
     }
   }
diff --git a/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs b/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs
index 0256db2fb2..e2e83a3a0a 100644
--- a/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs
+++ b/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs
@@ -23,11 +23,15 @@ public IndentationFormatter(TokenNewIndentCollector formatter) {
   /// Creates an IndentationFormatter for the given program,
   /// by immediately processing all nodes and assigning indentations to most structural tokens 
   /// </summary>
-  public static IndentationFormatter ForProgram(Program program, bool reduceBlockiness = true) {
-    var tokenNewIndentCollector = new TokenNewIndentCollector(program) {
+  public static IndentationFormatter ForProgram(Program program, Uri fileToFormat, bool reduceBlockiness = true) {
+    var tokenNewIndentCollector = new TokenNewIndentCollector(program, fileToFormat) {
       ReduceBlockiness = reduceBlockiness
     };
     foreach (var child in program.DefaultModuleDef.PreResolveChildren) {
+      var isPhysicalToken = child.Tok.line != 0;
+      if (isPhysicalToken && child.Tok.Uri != fileToFormat) {
+        continue;
+      }
       if (child is TopLevelDecl topLevelDecl) {
         tokenNewIndentCollector.SetDeclIndentation(topLevelDecl, 0);
       } else if (child is Include include) {
diff --git a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs
index ca0597ec55..0a2c218065 100644
--- a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs
+++ b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs
@@ -83,8 +83,9 @@ private Indentations PosToIndentations(int pos) {
   public int binOpIndent = -1;
   public int binOpArgIndent = -1;
 
-  internal TokenNewIndentCollector(Program program) {
+  internal TokenNewIndentCollector(Program program, Uri fileToFormat) {
     this.program = program;
+    this.fileToFormat = fileToFormat;
     preResolve = true;
   }
 
@@ -222,6 +223,7 @@ public int GetRightAlignIndentAfter(IToken token, int indentFallback) {
   }
 
   private static readonly Regex FollowedByNewlineRegex = new Regex("^[ \t]*([\r\n]|//)");
+  private readonly Uri fileToFormat;
 
   public static bool IsFollowedByNewline(IToken token) {
     return FollowedByNewlineRegex.IsMatch(token.TrailingTrivia);
@@ -231,7 +233,7 @@ public static bool IsFollowedByNewline(IToken token) {
   // 'inline' is the hypothetical indentation of this token if it was on its own line
   // 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation
   public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) {
-    if (token.FromIncludeDirective(program) || (token.line == 0 && token.col == 0)) {
+    if (token.Uri != fileToFormat || (token.line == 0 && token.col == 0)) {
       // Just ignore this token.
       return;
     }
diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs
index 21b2959b1e..3515cb202a 100644
--- a/Source/DafnyCore/AST/Members/ICodeContext.cs
+++ b/Source/DafnyCore/AST/Members/ICodeContext.cs
@@ -170,4 +170,6 @@ public interface RedirectingTypeDecl : ICallable {
   SubsetTypeDecl.WKind WitnessKind { get; }
   Expression/*?*/ Witness { get; }  // non-null iff WitnessKind is Compiled or Ghost
   FreshIdGenerator IdGenerator { get; }
+
+  [FilledInDuringResolution] bool ConstraintIsCompilable { get; set; }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs
index 215d2439b4..8455b0f63e 100644
--- a/Source/DafnyCore/AST/SystemModuleManager.cs
+++ b/Source/DafnyCore/AST/SystemModuleManager.cs
@@ -103,6 +103,7 @@ public SystemModuleManager(DafnyOptions options) {
     NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"),
       new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
       new List<TypeParameter>(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax);
+    ((RedirectingTypeDecl)NatDecl).ConstraintIsCompilable = true;
     SystemModule.SourceDecls.Add(NatDecl);
     // create trait 'object'
     ObjectDecl = new TraitDecl(RangeToken.NoToken, new Name("object"), SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), false, null);
diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
index abd9b684fd..ce41305f19 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
+++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
@@ -15,6 +15,12 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect
   public SubsetTypeDecl.WKind WitnessKind { get; set; } = SubsetTypeDecl.WKind.CompiledZero;
   public Expression/*?*/ Witness { get; set; } // non-null iff WitnessKind is Compiled or Ghost
   [FilledInDuringResolution] public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers)
+
+  [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; }
+
+  [FilledInDuringResolution] public bool NativeTypeRangeImpliesAllConstraints; // indicates that all values in the range of the native type are values of the newtype
+  [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype
+
   public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List<Type> parentTraits,
     List<MemberDecl> members, Attributes attributes, bool isRefining)
     : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining, parentTraits) {
@@ -24,6 +30,7 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Ty
     Contract.Requires(isRefining ^ (baseType != null));
     Contract.Requires(members != null);
     BaseType = baseType;
+    this.NewSelfSynonym();
   }
   public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint,
     SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs
index a7549b338a..8d235f2708 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs
+++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs
@@ -11,8 +11,10 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl, ICanAutoReve
   public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special }
   public readonly WKind WitnessKind;
   public Expression/*?*/ Witness;  // non-null iff WitnessKind is Compiled or Ghost
-  [FilledInDuringResolution] public bool ConstraintIsCompilable;
   [FilledInDuringResolution] public bool CheckedIfConstraintIsCompilable = false; // Set to true lazily by the Resolver when the Resolver fills in "ConstraintIsCompilable".
+
+  [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; }
+
   public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, ModuleDefinition module,
     BoundVar id, Expression constraint, WKind witnessKind, Expression witness,
     Attributes attributes)
diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs
index 4017f3bdad..308b7f542f 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs
+++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs
@@ -64,6 +64,12 @@ public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
   ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } }
   BoundVar RedirectingTypeDecl.Var { get { return null; } }
   Expression RedirectingTypeDecl.Constraint { get { return null; } }
+
+  bool RedirectingTypeDecl.ConstraintIsCompilable {
+    get => false;
+    set => throw new NotSupportedException();
+  }
+
   SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return SubsetTypeDecl.WKind.CompiledZero; } }
   Expression RedirectingTypeDecl.Witness { get { return null; } }
   FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
index 61a7c3b705..f5c283f664 100644
--- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
@@ -3291,6 +3291,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         } else {
           Contract.Assert(false, $"not implemented for C#: {e.E.Type} -> {e.ToType}");
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for C#: {e.E.Type} -> {e.ToType}");
       }
diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
index 7f7b64650c..1db454938d 100644
--- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
+++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
@@ -2356,11 +2356,14 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
             wr.Write(".{0}()", Capitalize(GetNativeTypeName(nt)));
           }
         }
-      } else {
-        Contract.Assert(e.E.Type.IsBigOrdinalType);
+      } else if (e.E.Type.IsBigOrdinalType) {
         Contract.Assert(e.ToType.IsNumericBased(Type.NumericPersuasion.Int));
         // identity will do
         wr.Append(Expr(e.E, inLetExprBody, wStmts));
+      } else {
+        // identity will do
+        Contract.Assert(e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null);
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       }
     }
 
diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
index ea506f6cae..359434bd4c 100644
--- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
+++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
@@ -3576,6 +3576,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
             wr.Write(".{0}()", Capitalize(GetNativeTypeName(nt)));
           }
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for go: {e.E.Type} -> {e.ToType}");
       }
diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
index face2a1e8d..d2c7254b86 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -4186,6 +4186,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         } else {
           Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}");
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}");
       }
diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
index 249c8395a6..fc31dc63a2 100644
--- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
+++ b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
@@ -2432,6 +2432,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         if (e.ToType.IsCharType) {
           wr.Write(").toNumber())");
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for javascript: {e.E.Type} -> {e.ToType}");
       }
diff --git a/Source/DafnyCore/Compilers/Python/PythonBackend.cs b/Source/DafnyCore/Compilers/Python/PythonBackend.cs
index 41189692bb..247f858e9a 100644
--- a/Source/DafnyCore/Compilers/Python/PythonBackend.cs
+++ b/Source/DafnyCore/Compilers/Python/PythonBackend.cs
@@ -4,6 +4,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using System.Runtime.InteropServices;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -46,6 +47,17 @@ private static string FindModuleName(string externFilename) {
     return Path.GetExtension(externFilename) == ".py" ? Path.GetFileNameWithoutExtension(externFilename) : null;
   }
 
+  private static readonly Dictionary<OSPlatform, string> PlatformDefaults = new() {
+    {OSPlatform.Linux, "python3"},
+    {OSPlatform.Windows, "python"},
+    {OSPlatform.FreeBSD, "python3"},
+    {OSPlatform.OSX, "python3"},
+  };
+  private static string DefaultPythonCommand => PlatformDefaults.SingleOrDefault(
+      kv => RuntimeInformation.IsOSPlatform(kv.Key),
+      new(OSPlatform.Linux, "python3")
+    ).Value;
+
   bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) {
     // Grossly, we need to look in the file to figure out where to put it
     var moduleName = FindModuleName(externFilename);
@@ -88,7 +100,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
       }
     }
     if (!runAfterCompile) {
-      var psi = PrepareProcessStartInfo("python3");
+      var psi = PrepareProcessStartInfo(DefaultPythonCommand);
       psi.Arguments = $"-m compileall -q {Path.GetDirectoryName(targetFilename)}";
       return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling Python files.");
     }
@@ -99,7 +111,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
     string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter,
     TextWriter errorWriter) {
     Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
-    var psi = PrepareProcessStartInfo("python3", Options.MainArgs.Prepend(targetFilename));
+    var psi = PrepareProcessStartInfo(DefaultPythonCommand, Options.MainArgs.Prepend(targetFilename));
     psi.EnvironmentVariables["PYTHONIOENCODING"] = "utf8";
     return 0 == RunProcess(psi, outputWriter, errorWriter);
   }
diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
index 0e7a3d1527..82673af45f 100644
--- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs
+++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
@@ -669,10 +669,10 @@ private ConcreteSyntaxTree CreateGuardedForeachLoop(
       ) {
       wr = CreateForeachLoop(tmpVarName, collectionElementType, tok, out var collectionWriter, wr);
       collection(collectionWriter);
-      wr = MaybeInjectSubtypeConstraint(tmpVarName, collectionElementType, boundVar.Type, inLetExprBody, tok, wr);
+      wr = MaybeInjectSubtypeConstraintWrtTraits(tmpVarName, collectionElementType, boundVar.Type, inLetExprBody, tok, wr);
       EmitDowncastVariableAssignment(IdName(boundVar), boundVar.Type, tmpVarName, collectionElementType,
           introduceBoundVar, tok, wr);
-      wr = MaybeInjectSubsetConstraint(boundVar, boundVar.Type, collectionElementType, inLetExprBody, tok, wr);
+      wr = MaybeInjectSubsetConstraint(boundVar, boundVar.Type, inLetExprBody, tok, wr);
       return wr;
     }
 
@@ -686,7 +686,7 @@ protected abstract Action<ConcreteSyntaxTree> GetSubtypeCondition(
       string tmpVarName, Type boundVarType, IToken tok, ConcreteSyntaxTree wPreconditions);
 
     /// <summary>
-    /// Emit an (already verified) downcast assignment like:
+    /// Emit an upcast or (already verified) downcast assignment like:
     /// 
     ///     var boundVarName:boundVarType := tmpVarName as boundVarType;
     ///     [[bodyWriter]]
@@ -1410,6 +1410,13 @@ protected abstract void EmitMapDisplay(MapType mt, IToken tok, List<ExpressionPa
     /// </summary>
     protected abstract string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr);
 
+    /// <summary>
+    /// Returns a pair (ty, f) where
+    ///   * "f" is a closure that, to a given writer, emits code that enumerates an integer-valued range from
+    ///     "wLo" to "wHi" using the target type of "type"
+    ///   * "ty" is a Dafny type whose target type is the same as the target type of "type"
+    /// It is assumed that "type" is some integer-based type (not a bitvector type, for example).
+    /// </summary>
     protected virtual (Type, Action<ConcreteSyntaxTree>) EmitIntegerRange(Type type, Action<ConcreteSyntaxTree> wLo, Action<ConcreteSyntaxTree> wHi) {
       Type result;
       if (AsNativeType(type) != null) {
@@ -3776,6 +3783,12 @@ protected virtual ConcreteSyntaxTree EmitAnd(Action<ConcreteSyntaxTree> lhs, Con
       return wr;
     }
 
+    /// <summary>
+    /// Returns a type whose target type is the same as the target type of the values returned by the emitted enumeration.
+    /// The output value of "collectionWriter" is an action that emits the enumeration.
+    /// Note that, while the values returned bny the enumeration have the target representation of "bv.Type", they may
+    /// not be legal "bv.Type" values -- that is, it could be that "bv.Type" has further constraints that need to be checked.
+    /// </summary>
     Type CompileCollection(ComprehensionExpr.BoundedPool bound, IVariable bv, bool inLetExprBody, bool includeDuplicates,
         Substituter/*?*/ su, out Action<ConcreteSyntaxTree> collectionWriter, ConcreteSyntaxTree wStmts,
         List<ComprehensionExpr.BoundedPool>/*?*/ bounds = null, List<BoundVar>/*?*/ boundVars = null, int boundIndex = 0) {
@@ -5527,13 +5540,13 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
           var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_");
           ConcreteSyntaxTree newWBody = CreateLambda(new List<Type> { collectionElementType }, e.tok, new List<string> { tmpVarName }, Type.Bool, wBody, wStmts, untyped: true);
           wStmts = newWBody.Fork();
-          newWBody = MaybeInjectSubtypeConstraint(
+          newWBody = MaybeInjectSubtypeConstraintWrtTraits(
             tmpVarName, collectionElementType, bv.Type,
             inLetExprBody, e.tok, newWBody, true, e is ForallExpr);
           EmitDowncastVariableAssignment(
             IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody);
           newWBody = MaybeInjectSubsetConstraint(
-            bv, bv.Type, collectionElementType, inLetExprBody, e.tok, newWBody, true, e is ForallExpr);
+            bv, bv.Type, inLetExprBody, e.tok, newWBody, isReturning: true, elseReturnValue: e is ForallExpr);
           wBody = newWBody;
         }
         EmitExpr(logicalBody, inLetExprBody, wBody, wStmts);
@@ -5698,7 +5711,7 @@ protected void WriteTypeDescriptors(TopLevelDecl decl, List<Type> typeArguments,
     ///        ...
     ///     }
     /// 
-    /// MaybeInjectSubtypeConstraint emits a subtype constraint that tmpVarName should be of type boundVarType, typically of the form
+    /// MaybeInjectSubtypeConstraintWrtTraits emits a subtype constraint that tmpVarName should be of type boundVarType, typically of the form
     /// 
     ///       if([tmpVarName] is [boundVarType]) {
     ///         // This is where 'wr' will write
@@ -5708,19 +5721,21 @@ protected void WriteTypeDescriptors(TopLevelDecl decl, List<Type> typeArguments,
     /// to use in the lambdas used by forall and exists statements:
     ///
     ///       if([tmpVarName] is [boundVarType]) {
-    ///         return // This is where 'wr' will write
+    ///         // This is where 'wr' will write
     ///       } else {
     ///         return [elseReturnValue];
     ///       }
     ///
     /// </summary>
-    /// <returns></returns>
-    private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName,
-      Type collectionElementType, Type boundVarType, bool inLetExprBody,
-      IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false
-      ) {
-      var iterationValuesNeedToBeChecked = IsTargetSupertype(collectionElementType, boundVarType);
-      if (iterationValuesNeedToBeChecked) {
+    private ConcreteSyntaxTree MaybeInjectSubtypeConstraintWrtTraits(string tmpVarName, Type collectionElementType, Type boundVarType,
+      bool inLetExprBody, IToken tok, ConcreteSyntaxTree wr,
+      bool isReturning = false, bool elseReturnValue = false) {
+
+      if (Type.IsSupertype(boundVarType, collectionElementType)) {
+        // Every value of the collection enumeration is a value of the bound variable's type, so the assignment can be done unconditionally.
+        // (The caller may still need to insert an upcast, depending on the target language.)
+      } else {
+        // We need to perform a run-time check to see if the collection value can be assigned to the bound variable.
         var preconditions = wr.Fork();
         var conditions = GetSubtypeCondition(tmpVarName, boundVarType, tok, preconditions);
         if (conditions == null) {
@@ -5732,9 +5747,7 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName,
             wr = EmitBlock(wr);
             var wStmts = wr.Fork();
             wr = EmitReturnExpr(wr);
-            var elseLiteral = new LiteralExpr(tok, elseReturnValue) {
-              Type = Type.Bool
-            };
+            var elseLiteral = Expression.CreateBoolLiteral(tok, elseReturnValue);
             EmitExpr(elseLiteral, inLetExprBody, wr, wStmts);
           }
           wr = thenWriter;
@@ -5743,50 +5756,48 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName,
       return wr;
     }
 
+    /// <summary>
+    /// If needed, emit an if-statement wrapper that checks that the value stored in "boundVar" satisfies any (subset-type or newtype) constraints
+    /// of "boundVarType".
+    /// </summary>
     private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type boundVarType,
-      Type collectionElementType, bool inLetExprBody,
-      IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false,
-      bool isSubfiltering = false) {
-      if (!boundVarType.Equals(collectionElementType, true) &&
-          boundVarType.NormalizeExpand(true) is UserDefinedType {
-            TypeArgs: var typeArgs,
-            ResolvedClass:
-            SubsetTypeDecl {
-              TypeArgs: var typeParametersArgs,
-              Var: var variable,
-              Constraint: var constraint
+      bool inLetExprBody, IToken tok, ConcreteSyntaxTree wr,
+      bool isReturning = false, bool elseReturnValue = false, bool isSubfiltering = false) {
+
+      if (boundVarType.NormalizeExpandKeepConstraints() is UserDefinedType { ResolvedClass: RedirectingTypeDecl and var declWithConstraint } udt) {
+        if (declWithConstraint is SubsetTypeDecl or NewtypeDecl { NativeTypeRangeImpliesAllConstraints: false }) {
+          // the type is a subset type or newtype with non-trivial constraints
+
+          var baseType = (declWithConstraint.Var?.Type ?? ((NewtypeDecl)declWithConstraint).BaseType).NormalizeExpandKeepConstraints();
+          if (baseType is UserDefinedType { ResolvedClass: SubsetTypeDecl or NewtypeDecl } normalizedVariableType) {
+            wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType,
+              inLetExprBody, tok, wr, isReturning: isReturning, elseReturnValue: elseReturnValue, isSubfiltering: true);
+          }
+
+          if (declWithConstraint.Var != null) {
+            var typeMap = TypeParameter.SubstitutionMap(declWithConstraint.TypeArgs, udt.TypeArgs);
+            var instantiatedBaseType = baseType.Subst(typeMap);
+            var theValue = new ConversionExpr(tok, new IdentifierExpr(tok, boundVar), instantiatedBaseType) { Type = instantiatedBaseType };
+            var subContract = new Substituter(null,
+              new Dictionary<IVariable, Expression>() {
+                {declWithConstraint.Var, theValue}
+              },
+              typeMap
+            );
+            var constraintInContext = subContract.Substitute(declWithConstraint.Constraint);
+            var wStmts = wr.Fork();
+            var thenWriter = EmitIf(out var guardWriter, hasElse: isReturning, wr);
+            EmitExpr(constraintInContext, inLetExprBody, guardWriter, wStmts);
+            if (isReturning) {
+              var elseBranch = wr;
+              elseBranch = EmitBlock(elseBranch);
+              elseBranch = EmitReturnExpr(elseBranch);
+              wStmts = elseBranch.Fork();
+              EmitExpr(new LiteralExpr(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts);
             }
-          }) {
-        if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType {
-          ResolvedClass: SubsetTypeDecl
-        } normalizedVariableType) {
-          wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, collectionElementType,
-              inLetExprBody, tok, wr, isReturning, elseReturnValue, true);
-        }
-
-        var bvIdentifier = new IdentifierExpr(tok, boundVar);
-        var typeParameters = TypeParameter.SubstitutionMap(typeParametersArgs, typeArgs);
-        var subContract = new Substituter(null,
-          new Dictionary<IVariable, Expression>()
-          {
-            {variable, bvIdentifier}
-          },
-          new Dictionary<TypeParameter, Type>(
-            typeParameters
-          )
-        );
-        var constraintInContext = subContract.Substitute(constraint);
-        var wStmts = wr.Fork();
-        var thenWriter = EmitIf(out var guardWriter, hasElse: isReturning, wr);
-        EmitExpr(constraintInContext, inLetExprBody, guardWriter, wStmts);
-        if (isReturning) {
-          var elseBranch = wr;
-          elseBranch = EmitBlock(elseBranch);
-          elseBranch = EmitReturnExpr(elseBranch);
-          wStmts = elseBranch.Fork();
-          EmitExpr(new LiteralExpr(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts);
-        }
-        wr = thenWriter;
+            wr = thenWriter;
+          }
+        }
       }
 
       if (isReturning && !isSubfiltering) {
diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs
index 36bb9f2151..8a22e60103 100644
--- a/Source/DafnyCore/DafnyConsolePrinter.cs
+++ b/Source/DafnyCore/DafnyConsolePrinter.cs
@@ -69,7 +69,7 @@ private string GetFileLine(Uri uri, int lineIndex) {
         // Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep
         // an in-memory version of each file it parses.
         var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken);
-        var reader = file.GetContent();
+        using var reader = file.GetContent();
         lines = Util.Lines(reader).ToList();
       } catch (Exception) {
         lines = new List<string>();
diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery.cs
index f7ccac387f..8ac1512104 100644
--- a/Source/DafnyCore/Resolver/BoundsDiscovery.cs
+++ b/Source/DafnyCore/Resolver/BoundsDiscovery.cs
@@ -303,7 +303,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
       // Note, in the following loop, it's important to go backwards, because DiscoverAllBounds_Aux_SingleVar assumes "knownBounds" has been
       // filled in for higher-indexed variables.
       for (var j = bvars.Count; 0 <= --j;) {
-        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds);
+        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds, out _);
         knownBounds[j] = ComprehensionExpr.BoundedPool.GetBest(bounds);
 #if DEBUG_PRINT
         if (knownBounds[j] is ComprehensionExpr.IntBoundedPool) {
@@ -321,9 +321,11 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
       return knownBounds;
     }
 
-    public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {
+    public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr,
+      out bool constraintConsistsSolelyOfRangeConstraints) where VT : IVariable {
       expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type), expr);
-      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true, new List<ComprehensionExpr.BoundedPool>() { null });
+      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true,
+        new List<ComprehensionExpr.BoundedPool>() { null }, out constraintConsistsSolelyOfRangeConstraints);
     }
 
     /// <summary>
@@ -331,7 +333,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
     /// that is not bounded.
     /// </summary>
     private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr,
-      bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {
+      bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds, out bool constraintConsistsSolelyOfRangeConstraints) where VT : IVariable {
       Contract.Requires(bvars != null);
       Contract.Requires(0 <= j && j < bvars.Count);
       Contract.Requires(expr != null);
@@ -354,7 +356,14 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
       }
 
       // Go through the conjuncts of the range expression to look for bounds.
+      // Only very specific conjuncts qualify for "constraintConsistsSolelyOfRangeConstraints". To make the bookkeeping
+      // of these simple, we count the total number of conjuncts and the number of qualifying conjuncts. Then, after the
+      // loop, we can compare these.
+      var totalNumberOfConjuncts = 0;
+      var conjunctsQualifyingAsRangeConstraints = 0;
       foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {
+        totalNumberOfConjuncts++;
+
         if (conjunct is IdentifierExpr) {
           var ide = (IdentifierExpr)conjunct;
           if (ide.Var == (IVariable)bv) {
@@ -426,6 +435,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
           case BinaryExpr.ResolvedOpcode.SeqEq:
           case BinaryExpr.ResolvedOpcode.MultiSetEq:
           case BinaryExpr.ResolvedOpcode.MapEq:
+            conjunctsQualifyingAsRangeConstraints++;
             var otherOperand = whereIsBv == 0 ? e1 : e0;
             bounds.Add(new ComprehensionExpr.ExactBoundedPool(otherOperand));
             break;
@@ -435,6 +445,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
             throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct
           case BinaryExpr.ResolvedOpcode.Lt:
             if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int)) {
+              conjunctsQualifyingAsRangeConstraints++;
               if (whereIsBv == 0) {
                 // bv < E
                 bounds.Add(new ComprehensionExpr.IntBoundedPool(null, e1));
@@ -445,6 +456,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
             }
             break;
           case BinaryExpr.ResolvedOpcode.Le:
+            conjunctsQualifyingAsRangeConstraints++;
             if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int)) {
               if (whereIsBv == 0) {
                 // bv <= E
@@ -469,6 +481,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
             break;
         }
       }
+      constraintConsistsSolelyOfRangeConstraints = conjunctsQualifyingAsRangeConstraints == totalNumberOfConjuncts;
       return bounds;
     }
 
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index b8a980b412..b697df8ac0 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -1166,6 +1166,25 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
       // Compute ghost interests, figure out native types, check agreement among datatype destructors, and determine tail calls.
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         foreach (TopLevelDecl d in declarations) {
+          void CheckIfCompilable(RedirectingTypeDecl declWithConstraint) {
+            var constraintIsCompilable = true;
+
+            // Check base type
+            var baseType = (declWithConstraint.Var?.Type ?? ((NewtypeDecl)declWithConstraint).BaseType).NormalizeExpandKeepConstraints();
+            if (baseType.AsRedirectingType is (SubsetTypeDecl or NewtypeDecl) and var baseDecl) {
+              CheckIfCompilable(baseDecl);
+              constraintIsCompilable &= baseDecl.ConstraintIsCompilable;
+            }
+
+            // Check the type's constraint
+            if (declWithConstraint.Constraint != null) {
+              constraintIsCompilable &= ExpressionTester.CheckIsCompilable(Options, null, declWithConstraint.Constraint,
+                new CodeContextWrapper(declWithConstraint, true));
+            }
+
+            declWithConstraint.ConstraintIsCompilable = constraintIsCompilable;
+          }
+
           if (d is IteratorDecl) {
             var iter = (IteratorDecl)d;
             iter.SubExpressions.ForEach(e => CheckExpression(e, this, iter));
@@ -1177,9 +1196,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
           } else if (d is SubsetTypeDecl subsetTypeDecl) {
             Contract.Assert(subsetTypeDecl.Constraint != null);
             CheckExpression(subsetTypeDecl.Constraint, this, new CodeContextWrapper(subsetTypeDecl, true));
-            subsetTypeDecl.ConstraintIsCompilable =
-              ExpressionTester.CheckIsCompilable(Options, null, subsetTypeDecl.Constraint, new CodeContextWrapper(subsetTypeDecl, true));
-            subsetTypeDecl.CheckedIfConstraintIsCompilable = true;
+            CheckIfCompilable(subsetTypeDecl);
 
             if (subsetTypeDecl.Witness != null) {
               CheckExpression(subsetTypeDecl.Witness, this, new CodeContextWrapper(subsetTypeDecl, subsetTypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost));
@@ -1193,13 +1210,15 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
             if (newtypeDecl.Var != null) {
               Contract.Assert(newtypeDecl.Constraint != null);
               CheckExpression(newtypeDecl.Constraint, this, new CodeContextWrapper(newtypeDecl, true));
-              if (newtypeDecl.Witness != null) {
-                CheckExpression(newtypeDecl.Witness, this, new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost));
-              }
             }
-            if (newtypeDecl.Witness != null && newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
-              var codeContext = new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost);
-              ExpressionTester.CheckIsCompilable(Options, this, newtypeDecl.Witness, codeContext);
+            CheckIfCompilable(newtypeDecl);
+
+            if (newtypeDecl.Witness != null) {
+              CheckExpression(newtypeDecl.Witness, this, new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost));
+              if (newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
+                var codeContext = new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost);
+                ExpressionTester.CheckIsCompilable(Options, this, newtypeDecl.Witness, codeContext);
+              }
             }
 
             FigureOutNativeType(newtypeDecl);
@@ -1628,8 +1647,11 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
           }
         }
       }
-      // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint
-      new SubsetConstraintGhostChecker(this.Reporter).Traverse(declarations);
+
+      if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+        // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint
+        new SubsetConstraintGhostChecker(this.Reporter).Traverse(declarations);
+      }
     }
 
     /// <summary>
@@ -2107,11 +2129,13 @@ private void FigureOutNativeType(NewtypeDecl dd) {
         ddConstraint = ddWhereConstraintsAre.Constraint;
       }
       List<ComprehensionExpr.BoundedPool> bounds;
+      bool constraintConsistsSolelyOfRangeConstraints;
       if (ddVar == null) {
         // There are no bounds at all
         bounds = new List<ComprehensionExpr.BoundedPool>();
+        constraintConsistsSolelyOfRangeConstraints = true;
       } else {
-        bounds = DiscoverAllBounds_SingleVar(ddVar, ddConstraint);
+        bounds = DiscoverAllBounds_SingleVar(ddVar, ddConstraint, out constraintConsistsSolelyOfRangeConstraints);
       }
 
       // Find which among the allowable native types can hold "dd". Give an
@@ -2161,6 +2185,13 @@ void UpdateBounds(BigInteger? lo, BigInteger? hi) {
       foreach (var nativeT in bigEnoughNativeTypes) {
         if (Options.Backend.SupportedNativeTypes.Contains(nativeT.Name)) {
           dd.NativeType = nativeT;
+          if (constraintConsistsSolelyOfRangeConstraints) {
+            dd.NativeTypeRangeImpliesAllConstraints = true;
+          }
+          if (constraintConsistsSolelyOfRangeConstraints && nativeT.Sel != NativeType.Selection.Number &&
+              lowBound == nativeT.LowerBound && highBound == nativeT.UpperBound) {
+            dd.TargetTypeCoversAllBitPatterns = true;
+          }
           break;
         }
       }
@@ -2169,8 +2200,13 @@ void UpdateBounds(BigInteger? lo, BigInteger? hi) {
         // one particular native type, in which case that must have been the one picked.
         if (nativeTypeChoices != null && nativeTypeChoices.Count == 1) {
           Contract.Assert(dd.NativeType == nativeTypeChoices[0]);
+          if (dd.TargetTypeCoversAllBitPatterns) {
+            reporter.Info(MessageSource.Resolver, dd.tok,
+              $"newtype {dd.Name} is target-complete for {{:nativeType \"{dd.NativeType.Name}\"}}");
+          }
         } else {
           var detectedRange = emptyRange ? "empty" : $"{lowBound} .. {highBound}";
+          var targetComplete = dd.TargetTypeCoversAllBitPatterns ? "target-complete " : "";
           reporter.Info(MessageSource.Resolver, dd.tok,
             $"newtype {dd.Name} resolves as {{:nativeType \"{dd.NativeType.Name}\"}} (detected range: {detectedRange})");
         }
diff --git a/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs b/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs
index 5c4fbae71e..f7b3db3939 100644
--- a/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs
+++ b/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs
@@ -81,28 +81,16 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN
       return base.Traverse(expr, field, parent);
     }
 
-    string what = e.WhatKind;
-
     if (e is QuantifierExpr or SetComprehension or MapComprehension) {
       foreach (var boundVar in e.BoundVars) {
-        if (boundVar.Type.AsSubsetType is {
-          Constraint: var constraint,
-          ConstraintIsCompilable: false and var constraintIsCompilable
-        } and var subsetTypeDecl
-           ) {
-          if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) {
-            // Builtin types were never resolved.
-            constraintIsCompilable =
-              ExpressionTester.CheckIsCompilable(reporter.Options, null, constraint, new CodeContextWrapper(subsetTypeDecl, true));
-            subsetTypeDecl.CheckedIfConstraintIsCompilable = true;
-            subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable;
-          }
+        if (boundVar.Type.NormalizeExpandKeepConstraints().AsRedirectingType is (SubsetTypeDecl or NewtypeDecl) and var declWithConstraint) {
+          if (!declWithConstraint.ConstraintIsCompilable) {
 
-          if (!constraintIsCompilable) {
             IToken finalToken = boundVar.tok;
-            if (constraint.tok.line != 0) {
+            if (declWithConstraint.Constraint != null && declWithConstraint.Constraint.tok.line != 0) {
               var errorCollector = new FirstErrorCollector(reporter.Options);
-              ExpressionTester.CheckIsCompilable(null, errorCollector, constraint, new CodeContextWrapper(subsetTypeDecl, true));
+              ExpressionTester.CheckIsCompilable(null, errorCollector, declWithConstraint.Constraint,
+                new CodeContextWrapper(declWithConstraint, true));
               if (errorCollector.Collected) {
                 finalToken = new NestedToken(finalToken, errorCollector.FirstCollectedToken,
                   "The constraint is not compilable because " + errorCollector.FirstCollectedMessage
@@ -110,7 +98,8 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN
               }
             }
             this.reporter.Error(MessageSource.Resolver, finalToken,
-              $"{boundVar.Type} is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in {what}.");
+              $"{boundVar.Type} is a {declWithConstraint.WhatKind} and its constraint is not compilable, " +
+              $"hence it cannot yet be used as the type of a bound variable in {e.WhatKind}.");
           }
         }
       }
diff --git a/Source/DafnyCore/Rewriters/ExpectContracts.cs b/Source/DafnyCore/Rewriters/ExpectContracts.cs
index 79feda0ddb..738996a252 100644
--- a/Source/DafnyCore/Rewriters/ExpectContracts.cs
+++ b/Source/DafnyCore/Rewriters/ExpectContracts.cs
@@ -1,7 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using Microsoft.Extensions.Logging.Abstractions;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny;
@@ -222,39 +221,50 @@ private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers
   }
 
   /// <summary>
-  /// Add wrappers for certain top-level declarations in the given module.
-  /// This runs after the first pass of resolution so that it has access to
-  /// ghostness information, attributes and call targets.
+  /// Adds wrappers for certain top-level declarations in the given
+  /// program and redirects callers to call those wrappers instead of
+  /// the original members.
+  ///
+  /// This runs after resolution so that it has access to ghostness
+  /// information, attributes and call targets and after verification
+  /// because that makes the interaction with the refinement transformer
+  /// more straightforward.
   /// </summary>
-  /// <param name="moduleDefinition">The module to generate wrappers for and in.</param>
-  internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition) {
-    // Keep a list of members to wrap so that we don't modify the collection we're iterating over.
-    List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new();
-
-    moduleDefinition.CallRedirector = new(Reporter);
-
-    // Find module members to wrap.
-    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-      foreach (var decl in topLevelDecl.Members) {
-        if (ShouldGenerateWrapper(decl)) {
-          membersToWrap.Add((topLevelDecl, decl));
+  /// <param name="program">The program to generate wrappers for and in.</param>
+  public override void PostVerification(Program program) {
+    // Create wrappers
+    foreach (var moduleDefinition in program.Modules()) {
+
+      // Keep a list of members to wrap so that we don't modify the collection we're iterating over.
+      List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new();
+
+      moduleDefinition.CallRedirector = new(Reporter);
+
+      // Find module members to wrap.
+      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+        foreach (var decl in topLevelDecl.Members) {
+          if (ShouldGenerateWrapper(decl)) {
+            membersToWrap.Add((topLevelDecl, decl));
+          }
         }
       }
-    }
 
-    // Generate a wrapper for each of the members identified above.
-    foreach (var (topLevelDecl, decl) in membersToWrap) {
-      GenerateWrapper(moduleDefinition, topLevelDecl, decl);
-    }
-    moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations;
-  }
+      // Generate a wrapper for each of the members identified above. This
+      // need to happen after all declarations to wrap have been identified
+      // because it adds new declarations and would invalidate the iterator
+      // used during identification.
+      foreach (var (topLevelDecl, decl) in membersToWrap) {
+        GenerateWrapper(moduleDefinition, topLevelDecl, decl);
+      }
+      moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations;
 
-  public override void PostVerification(Program program) {
-    foreach (var module in program.CompileModules) {
-      foreach (var topLevelDecl in module.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      // Put redirections in place. Any wrappers to call will be in either
+      // this module or to a previously-processed module, so they'll already
+      // exist.
+      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
         foreach (var decl in topLevelDecl.Members) {
           if (decl is ICallable callable) {
-            module.CallRedirector?.Visit(callable, decl);
+            moduleDefinition.CallRedirector?.Visit(callable, decl);
           }
         }
       }
@@ -264,7 +274,7 @@ public override void PostVerification(Program program) {
       return;
     }
 
-    foreach (var module in program.CompileModules) {
+    foreach (var module in program.Modules()) {
       if (module.CallRedirector == null) {
         continue;
       }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
index cca3b5ce9b..7d376e6195 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
@@ -755,7 +755,7 @@ IEnumerable<Expression> GuessWitnesses(BoundVar x, Expression expr) {
       yield return lit;
     }
 
-    var bounds = ModuleResolver.DiscoverAllBounds_SingleVar(x, expr);
+    var bounds = ModuleResolver.DiscoverAllBounds_SingleVar(x, expr, out _);
     foreach (var bound in bounds) {
       if (bound is ComprehensionExpr.IntBoundedPool) {
         var bnd = (ComprehensionExpr.IntBoundedPool)bound;
diff --git a/Source/DafnyDriver.Test/FormatterCommandTest.cs b/Source/DafnyDriver.Test/FormatterCommandTest.cs
new file mode 100644
index 0000000000..cd3ae0260a
--- /dev/null
+++ b/Source/DafnyDriver.Test/FormatterCommandTest.cs
@@ -0,0 +1,65 @@
+using System.Diagnostics;
+using System.IO.Pipelines;
+using System.Reactive.Concurrency;
+using System.Reflection;
+using System.Text;
+using Microsoft.Dafny;
+using Microsoft.Extensions.Logging.Abstractions;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.JsonRpc.Client;
+using OmniSharp.Extensions.JsonRpc.Serialization;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace DafnyDriver.Test;
+
+public class FormatterCommandTest {
+  [Fact]
+  public async Task GitIssueVSCode452FormattingWorksOnBigFiles() {
+    // We write to a temporary file
+    var oneSource = (int i) => $@"function Test{i}(x: int): int
+// This returns {i} if x is greater than 20
+{{
+  if x < 10 then
+                  0
+                  else if x < 20 then
+                                       1
+                                          else {i}
+}}
+
+";
+
+    var oneSourceFormatted = (int i) => $@"function Test{i}(x: int): int
+  // This returns {i} if x is greater than 20
+{{
+  if x < 10 then
+    0
+  else if x < 20 then
+    1
+  else {i}
+}}
+
+";
+    var source = "";
+    var sourceFormatted = "";
+    for (var i = 0; i < 1000; i++) {
+      source += oneSource(i);
+      sourceFormatted += oneSourceFormatted(i);
+    }
+
+    var file = Path.GetTempFileName() + ".dfy";
+
+    await File.WriteAllTextAsync(file, source);
+    StringWriter strWriter = new StringWriter();
+    var options = DafnyOptions.Create(strWriter, null,
+      file
+      );
+
+    var exitValue = await FormatCommand.DoFormatting(options);
+    Assert.Equal(0, (int)exitValue);
+
+    var result = await File.ReadAllTextAsync(file);
+    Assert.Equal(sourceFormatted, result);
+    File.Delete(file);
+  }
+}
diff --git a/Source/DafnyDriver/Commands/FormatCommand.cs b/Source/DafnyDriver/Commands/FormatCommand.cs
index 130f69a702..62ba02ef9e 100644
--- a/Source/DafnyDriver/Commands/FormatCommand.cs
+++ b/Source/DafnyDriver/Commands/FormatCommand.cs
@@ -9,7 +9,7 @@
 
 namespace Microsoft.Dafny;
 
-static class FormatCommand {
+public static class FormatCommand {
 
   public static IEnumerable<Option> Options => DafnyCommands.FormatOptions;
 
@@ -72,8 +72,9 @@ public static async Task<ExitValue> DoFormatting(DafnyOptions options) {
           OnDiskFileSystem.Instance, options, new Uri(tempFileName), Token.NoToken);
       }
 
-      using var content = dafnyFile.GetContent();
+      var content = dafnyFile.GetContent();
       var originalText = await content.ReadToEndAsync();
+      content.Close(); // Manual closing because we want to overwrite
       dafnyFile.GetContent = () => new StringReader(originalText);
       // Might not be totally optimized but let's do that for now
       var err = DafnyMain.Parse(new List<DafnyFile> { dafnyFile }, programName, options, out var dafnyProgram);
@@ -86,7 +87,7 @@ public static async Task<ExitValue> DoFormatting(DafnyOptions options) {
         var result = originalText;
         if (firstToken != null) {
           result = Formatting.__default.ReindentProgramFromFirstToken(firstToken,
-            IndentationFormatter.ForProgram(dafnyProgram));
+            IndentationFormatter.ForProgram(dafnyProgram, file.Uri));
           if (result != originalText) {
             neededFormatting += 1;
             if (doCheck) {
diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs
index 1749a61af1..50a14ccf99 100644
--- a/Source/DafnyLanguageServer/Workspace/Compilation.cs
+++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs
@@ -428,7 +428,7 @@ public void CancelPendingUpdates() {
       firstToken = firstToken.Prev;
     }
     var result = Formatting.__default.ReindentProgramFromFirstToken(firstToken,
-      IndentationFormatter.ForProgram(program));
+      IndentationFormatter.ForProgram(program, firstToken.Uri));
 
     var lastToken = firstToken;
     while (lastToken.Next != null) {
diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs
index 03fdcab515..a545ba4197 100644
--- a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs
+++ b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs
@@ -38,7 +38,8 @@ public bool OpenDocument(TextDocumentItem document) {
     string existingText = "";
     try {
       if (OnDiskFileSystem.Instance.Exists(uri)) {
-        existingText = OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd();
+        using var fileStream = OnDiskFileSystem.Instance.ReadFile(uri);
+        existingText = fileStream.ReadToEnd();
       }
     } catch (IOException) {
       // If we don't manage to detect whether this document already existed ond disc,
diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs
index 0e7aa59c25..ef393b30b4 100644
--- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs
+++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs
@@ -75,7 +75,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
 
         var reprinted = firstToken != null && firstToken.line > 0
           ? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
-            IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
+            IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
           : programString;
         EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram);
         if (expectedProgram != reprinted) {
@@ -100,7 +100,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
         });
         var reprintedCloned = firstToken != null && firstToken.line > 0
           ? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
-            IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
+            IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
           : programString;
         EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram);
         if (expectedProgram != reprintedCloned) {
@@ -112,7 +112,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
         DafnyMain.Resolve(dafnyProgram);
         reprinted = firstToken != null && firstToken.line > 0
           ? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
-            IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
+            IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
           : programString;
         if (expectedProgram != reprinted) {
           options.ErrorWriter.WriteLine("Formatting after resolution generates an error:");
@@ -131,7 +131,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
         firstToken = dafnyProgram.GetFirstTokenForUri(uri);
         var reprinted2 = firstToken != null && firstToken.line > 0
           ? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
-            IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
+            IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
           : reprinted;
         if (reprinted != reprinted2) {
           Console.Write("Double formatting is not stable:\n");
diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs
index 7cfd8e3a5f..18bad05f7c 100644
--- a/Source/DafnyPipeline.Test/FormatterIssues.cs
+++ b/Source/DafnyPipeline.Test/FormatterIssues.cs
@@ -1,4 +1,6 @@
-using JetBrains.Annotations;
+using System;
+using System.IO;
+using JetBrains.Annotations;
 using Xunit;
 using Xunit.Abstractions;
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs
new file mode 100644
index 0000000000..c6d90d8e16
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs
@@ -0,0 +1,10 @@
+using System.Numerics;
+
+namespace M {
+
+  public partial class __default {
+    public static BigInteger ExternMethod() {
+      return new BigInteger(5);
+    }
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs
new file mode 100644
index 0000000000..efd74ded43
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs
@@ -0,0 +1,10 @@
+using System.Numerics;
+
+namespace M {
+
+  public partial class __default {
+    public static BigInteger ExternMethod() {
+      return new BigInteger(-5);
+    }
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy
index eeabf52dd9..b9d761d758 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %baredafny test %args --no-verify --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t
+// RUN: ! %baredafny test %args --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s"
 // CHECK: .*Foo____dafny__checked\(x\).*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect
index 347491a3cc..0cf0890ae3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect
@@ -1,7 +1,7 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
 CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.
 CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state.
-
-Dafny program verifier did not attempt verification
 FooTest: FAILED
 	CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12)
 BarTest: FAILED
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy
new file mode 100644
index 0000000000..499fdeab85
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy
@@ -0,0 +1,14 @@
+// RUN: %run "%s" --input "%S/AbstractExtern1.cs" --test-assumptions Externs
+// RUN: %exits-with 3 %run "%s" --input "%S/AbstractExtern2.cs" --test-assumptions Externs
+abstract module A {
+    method {:extern "ExternMethod"} Method() returns (r: int)
+      ensures r > 0
+}
+
+module M refines A {
+}
+
+method Main() {
+  var x := M.Method();
+  print x, "\n";
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy
index 4cd380a97d..8986374753 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %dafny /compile:4 /noVerify /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t
+// RUN: ! %dafny /compile:4 /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/TestedExterns.cs" "%s"
 // CHECK-NOT: .*Foo____dafny__checked\(x\).*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect
index 489654892a..3d25b4f587 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect
@@ -1,7 +1,7 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
 CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.
 CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state.
-
-Dafny program verifier did not attempt verification
 TestedExterns.dfy(10,17): Warning: No :test code calls NotCalled
 FooTest: FAILED
 	CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy
new file mode 100644
index 0000000000..56d6e389f1
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy
@@ -0,0 +1,15 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=0 "%s"
+
+module A
+{
+  export
+    provides T
+
+  newtype T = int
+}
+
+module B
+{
+  import A
+  type X = A.T
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy.expect
new file mode 100644
index 0000000000..012f5b9937
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy
new file mode 100644
index 0000000000..172c568fe6
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy
@@ -0,0 +1,200 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
+
+method Main() {
+  Tests.Test();
+  SubsetTypeSubsetType.Test();
+  SubsetTypeNewtype.Test();
+  NewtypeSubsetType.Test();
+  NewtypeNewtype.Test();
+}
+
+module Tests {
+  ghost predicate P(x: int) { x != 3 }
+
+  type PlainInt = int // type synonym
+  type PInt = x: int | P(x)
+  type PNat = x: int | 0 <= x && P(x)
+
+  newtype MyPlainInt = int
+  newtype MyPInt = x: int | P(x)
+  newtype MyPNat = x: int | 0 <= x && P(x)
+
+  class Cell {
+    const k: int
+    constructor (k: int) { this.k := k; }
+  }
+
+  type Cell5 = c: Cell | c.k == 5 witness *
+
+  method Test() {
+    var nats;
+    nats := set nx: nat | 2 <= nx < 5;
+    print |nats|, "\n"; // 3
+
+    var r0, r1, r2;
+    r0 := set n0: PlainInt | 0 <= n0 < 5;
+    r1 := set n1: PInt | 2 <= n1 < 5; // error: this set comprehension is not compilable
+    r2 := set n2: PNat | n2 < 5; // error: this set comprehension is not compilable
+    print |r0|, " ", |r1|, " ", |r2|, "\n"; // 5 2 4
+    var b0, b1;
+    b0 := forall k0: PInt | 2 <= k0 < 5 :: k0 != 3; // error: this set comprehension is not compilable
+    b1 := forall k1: PNat | k1 < 5 :: k1 != 4; // error: this set comprehension is not compilable
+    print b0, " ", b1, "\n"; // true false
+
+    var s0, s1, s2;
+    s0 := set m0: MyPlainInt | 0 <= m0 < 5;
+    s1 := set m1: MyPInt | 2 <= m1 < 5; // error: this set comprehension is not compilable
+    s2 := set m2: MyPNat | m2 < 5; // error: this set comprehension is not compilable
+    print |s0|, " ", |s1|, " ", |s2|, "\n"; // 5 2 4
+    b0 := forall l0: MyPInt | 2 <= l0 < 5 :: l0 as int != 3; // error: this set comprehension is not compilable
+    b1 := forall l1: MyPNat | l1 < 5 :: l1 != 4; // error: this set comprehension is not compilable
+    print b0, " ", b1, "\n"; // true false
+
+    var c0 := new Cell(4);
+    var c1 := new Cell(5);
+    var cc: set<Cell?> := {null, c0, c1};
+    var cc'0 := set y0: Cell? | y0 in cc;
+    var cc'1 := set y1: Cell | y1 in cc;
+    var cc'2 := set y2: Cell5 | y2 in cc;
+    print |cc|, " ", |cc'0|, " ", |cc'1|, " ", |cc'2|, "\n"; // 3 3 2 1
+  }
+}
+
+// check a compilable constraint with a non-compilable base type
+
+module SubsetTypeSubsetType {
+  ghost predicate P(x: int) { x != 3 }
+
+  type NonCompilableTest = x: int | P(x)
+  type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  type Type0 = x: NonCompilableTest | true
+  type Type1 = NonCompilableTest
+  type Type2 = x: NonCompilableTestInt32 | true
+  type Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  type CompilableTest = x: int | Q(x) && x < 8
+  type Type4 = x: CompilableTest | true
+  type Type5 = CompilableTest
+  type Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module SubsetTypeNewtype {
+  ghost predicate P(x: int) { x != 3 }
+
+  type NonCompilableTest = x: int | P(x)
+  type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  newtype Type0 = x: NonCompilableTest | true
+  newtype Type1 = NonCompilableTest
+  newtype Type2 = x: NonCompilableTestInt32 | true
+  newtype Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  type CompilableTest = x: int | Q(x) && x < 8
+  newtype Type4 = x: CompilableTest | true
+  newtype Type5 = CompilableTest
+  newtype Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module NewtypeSubsetType {
+  ghost predicate P(x: int) { x != 3 }
+
+  newtype NonCompilableTest = x: int | P(x)
+  newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  type Type0 = x: NonCompilableTest | true
+  type Type1 = NonCompilableTest
+  type Type2 = x: NonCompilableTestInt32 | true
+  type Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  newtype CompilableTest = x: int | Q(x) && x < 8
+  type Type4 = x: CompilableTest | true
+  type Type5 = CompilableTest
+  type Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module NewtypeNewtype {
+  ghost predicate P(x: int) { x != 3 }
+
+  newtype NonCompilableTest = x: int | P(x)
+  newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  newtype Type0 = x: NonCompilableTest | true
+  newtype Type1 = NonCompilableTest
+  newtype Type2 = x: NonCompilableTestInt32 | true
+  newtype Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  newtype CompilableTest = x: int | Q(x) && x < 8
+  newtype Type4 = x: CompilableTest | true
+  newtype Type5 = CompilableTest
+  newtype Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable
+    r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy.expect
new file mode 100644
index 0000000000..644f539fc2
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy.expect
@@ -0,0 +1,26 @@
+git-issue-697i.dfy(37,14): Error: PInt is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(16,23)
+git-issue-697i.dfy(38,14): Error: PNat is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(17,33)
+git-issue-697i.dfy(41,17): Error: PInt is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(16,23)
+git-issue-697i.dfy(42,17): Error: PNat is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(17,33)
+git-issue-697i.dfy(47,14): Error: MyPInt is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(20,28)
+git-issue-697i.dfy(48,14): Error: MyPNat is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(21,38)
+git-issue-697i.dfy(50,17): Error: MyPInt is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(20,28)
+git-issue-697i.dfy(51,17): Error: MyPNat is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(21,38)
+git-issue-697i.dfy(86,14): Error: Type0 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(87,14): Error: Type1 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(69,36)
+git-issue-697i.dfy(88,14): Error: Type2 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(89,14): Error: Type3 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(70,76)
+git-issue-697i.dfy(120,14): Error: Type0 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(121,14): Error: Type1 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(122,14): Error: Type2 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(123,14): Error: Type3 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(154,14): Error: Type0 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(155,14): Error: Type1 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(137,39)
+git-issue-697i.dfy(156,14): Error: Type2 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(157,14): Error: Type3 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(138,79)
+git-issue-697i.dfy(188,14): Error: Type0 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(189,14): Error: Type1 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(190,14): Error: Type2 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(191,14): Error: Type3 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
+git-issue-697i.dfy(12,7): Error: not resolving module '_module' because there were errors in resolving its nested module 'Tests'
+25 resolution/type errors detected in git-issue-697i.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy
new file mode 100644
index 0000000000..b47a2f4cc6
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy
@@ -0,0 +1,305 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+method Main() {
+  Tests.Test();
+
+  AnotherTest.Test();
+
+  SubsetTypeSubsetType.Test();
+  SubsetTypeNewtype.Test();
+  NewtypeSubsetType.Test();
+  NewtypeNewtype.Test();
+
+  MoreNativeTypes.Test();
+
+  Regressions.Test0();
+  Regressions.Test1();
+
+  EvolvingNativeTypes.Test();
+}
+
+module Tests {
+  predicate P(x: int) { x != 3 }
+
+  type PlainInt = int // type synonym
+  type PInt = x: int | P(x)
+  type PNat = x: int | 0 <= x && P(x)
+
+  newtype MyPlainInt = int
+  newtype MyPInt = x: int | P(x)
+  newtype MyPNat = x: int | 0 <= x && P(x)
+
+  class Cell {
+    const k: int
+    constructor (k: int) { this.k := k; }
+  }
+
+  type Cell5 = c: Cell | c.k == 5 witness *
+
+  method Test() {
+    var nats;
+    nats := set nx: nat | 2 <= nx < 5;
+    print |nats|, "\n"; // 3
+
+    var r0, r1, r2;
+    r0 := set n0: PlainInt | 0 <= n0 < 5;
+    r1 := set n1: PInt | 2 <= n1 < 5;
+    r2 := set n2: PNat | n2 < 5;
+    print |r0|, " ", |r1|, " ", |r2|, "\n"; // 5 2 4
+    var b0, b1;
+    b0 := forall k0: PInt | 2 <= k0 < 5 :: k0 != 3;
+    b1 := forall k1: PNat | k1 < 5 :: k1 != 4;
+    print b0, " ", b1, "\n"; // true false
+
+    var s0, s1, s2;
+    s0 := set m0: MyPlainInt | 0 <= m0 < 5;
+    s1 := set m1: MyPInt | 2 <= m1 < 5;
+    s2 := set m2: MyPNat | m2 < 5;
+    print |s0|, " ", |s1|, " ", |s2|, "\n"; // 5 2 4
+    b0 := forall l0: MyPInt | 2 <= l0 < 5 :: l0 as int != 3;
+    b1 := forall l1: MyPNat | l1 < 5 :: l1 != 4;
+    print b0, " ", b1, "\n"; // true false
+
+    var c0 := new Cell(4);
+    var c1 := new Cell(5);
+    var cc: set<Cell?> := {null, c0, c1};
+    var cc'0 := set y0: Cell? | y0 in cc;
+    var cc'1 := set y1: Cell | y1 in cc;
+    var cc'2 := set y2: Cell5 | y2 in cc;
+    print |cc|, " ", |cc'0|, " ", |cc'1|, " ", |cc'2|, "\n"; // 3 3 2 1
+  }
+}
+
+module AnotherTest {
+  predicate P(s: seq<int>) { |s| <= 1 }
+
+  type T = seq<int>
+  type SST = s: T | P(s)
+
+  method Test() {
+    var a0: T := [];
+    var a1: T := [25];
+    var a2: T := [100, 101];
+    var a3: T := [22];
+    var S: set<T> := { a0, a1, a2, a3 };
+    var s1 := set m: SST | m in S;
+    print |s1|, "\n"; // 3
+  }
+}
+
+module SubsetTypeSubsetType {
+  predicate P(x: int) { x != 3 }
+
+  type NonCompilableTest = x: int | P(x)
+  type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  type Type0 = x: NonCompilableTest | true
+  type Type1 = NonCompilableTest
+  type Type2 = x: NonCompilableTestInt32 | true
+  type Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  type CompilableTest = x: int | Q(x) && x < 8
+  type Type4 = x: CompilableTest | true
+  type Type5 = CompilableTest
+  type Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6;
+    r1 := set y: Type1 | 2 <= y < 6;
+    r2 := set y: Type2 | 2 <= y < 6;
+    r3 := set y: Type3 | 2 <= y < 6;
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module SubsetTypeNewtype {
+  predicate P(x: int) { x != 3 }
+
+  type NonCompilableTest = x: int | P(x)
+  type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  newtype Type0 = x: NonCompilableTest | true
+  newtype Type1 = NonCompilableTest
+  newtype Type2 = x: NonCompilableTestInt32 | true
+  newtype Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  type CompilableTest = x: int | Q(x) && x < 8
+  newtype Type4 = x: CompilableTest | true
+  newtype Type5 = CompilableTest
+  newtype Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6;
+    r1 := set y: Type1 | 2 <= y < 6;
+    r2 := set y: Type2 | 2 <= y < 6;
+    r3 := set y: Type3 | 2 <= y < 6;
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module NewtypeSubsetType {
+  predicate P(x: int) { x != 3 }
+
+  newtype NonCompilableTest = x: int | P(x)
+  newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  type Type0 = x: NonCompilableTest | true
+  type Type1 = NonCompilableTest
+  type Type2 = x: NonCompilableTestInt32 | true
+  type Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  newtype CompilableTest = x: int | Q(x) && x < 8
+  type Type4 = x: CompilableTest | true
+  type Type5 = CompilableTest
+  type Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6;
+    r1 := set y: Type1 | 2 <= y < 6;
+    r2 := set y: Type2 | 2 <= y < 6;
+    r3 := set y: Type3 | 2 <= y < 6;
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module NewtypeNewtype {
+  predicate P(x: int) { x != 3 }
+
+  newtype NonCompilableTest = x: int | P(x)
+  newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x)
+
+  newtype Type0 = x: NonCompilableTest | true
+  newtype Type1 = NonCompilableTest
+  newtype Type2 = x: NonCompilableTestInt32 | true
+  newtype Type3 = NonCompilableTestInt32
+
+  predicate Q(x: int) { x != 5 }
+
+  newtype CompilableTest = x: int | Q(x) && x < 8
+  newtype Type4 = x: CompilableTest | true
+  newtype Type5 = CompilableTest
+  newtype Type6 = x: CompilableTest | 0 <= x
+
+  method Test() {
+    var r0, r1, r2, r3;
+    r0 := set y: Type0 | 2 <= y < 6;
+    r1 := set y: Type1 | 2 <= y < 6;
+    r2 := set y: Type2 | 2 <= y < 6;
+    r3 := set y: Type3 | 2 <= y < 6;
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3
+
+    var r4, r5, r6;
+    r4 := set y: Type4 | 2 <= y;
+    r5 := set y: Type5 | 2 <= y;
+    r6 := set y: Type6 | 2 <= y;
+    print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5
+  }
+}
+
+module MoreNativeTypes {
+  type LoSubset = x: int | -0x8000_0000 <= x
+  newtype LoNewtype = x: int | -0x8000_0000 <= x
+
+  newtype Int32a = x: LoSubset | x < 0x8000_0000
+  newtype Int32b = x: LoNewtype | x < 0x8000_0000
+
+  type Int32c = x: Int32a | x != 3
+  type Int32d = x: Int32b | x != 3
+  newtype Int32e = x: Int32a | x != 3
+  newtype Int32f = x: Int32b | x != 3
+
+  method Test() {
+    var r0, r1;
+    r0 := set y: Int32a | 2 <= y < 6;
+    r1 := set y: Int32b | 2 <= y < 6;
+
+    var r2, r3, r4, r5;
+    r2 := set y: Int32c | 2 <= y < 6;
+    r3 := set y: Int32d | 2 <= y < 6;
+    r4 := set y: Int32e | 2 <= y < 6;
+    r5 := set y: Int32f | 2 <= y < 6;
+
+    print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, " ", |r4|, " ", |r5|, "\n"; // 4 4 3 3 3 3
+  }
+}
+
+module Regressions {
+  type byte = x | x < 256 && x != 7 && 0 <= x
+
+  predicate P(x: int) { x == 7 || x == 9 }
+
+  method Test0() {
+    var s := set b: byte | 5 <= b < 12 && P(b as int);
+    assert 9 in s;
+    var u :| u in s;
+    print u, "\n"; // 9
+  }
+
+  // -----------------------------
+
+  newtype NewByte = x | x < 256 && x != 7 && 0 <= x
+
+  newtype ByteBase = x: int | x != 7
+  type Byyyte = x: ByteBase | x < 256 && 0 <= x
+
+  predicate Filter(x: int) {
+    x % 2 == 1 && x < 10
+  }
+
+  method Test1() {
+    var s := set b: byte | Filter(b as int);
+    var t := set b: NewByte | Filter(b as int);
+    var u := set b: Byyyte | Filter(b as int);
+
+    print |s|, " ", |t|, " ", |u|, "\n"; // 4 4 4
+  }
+}
+
+module EvolvingNativeTypes {
+  newtype Nat = x: int | 0 <= x && x != 1
+  newtype uint32 = x: Nat | x < 0x1_0000_0000 && x != 3
+  newtype byte = x: uint32 | x < 256 && x != 5
+  newtype Not7Either = x: byte | x != 7
+
+  predicate R(x: int) {
+    match x
+    case 5 => true
+    case 1 | 3 | 7 | 9 => true
+    case _ => false
+  }
+
+  method Test() {
+    assert R(7);
+    var u: byte :| R(u as int) && u != 9;
+    assert R(9);
+    var v: Not7Either :| R(v as int);
+    print u, " ", v, "\n"; // 7 9
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.expect
new file mode 100644
index 0000000000..d70a0d3c3a
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.expect
@@ -0,0 +1,19 @@
+3
+5 2 4
+true false
+5 2 4
+true false
+3 3 2 1
+3
+3 3 3 3
+5 5 5
+3 3 3 3
+5 5 5
+3 3 3 3
+5 5 5
+3 3 3 3
+5 5 5
+4 4 3 3 3 3
+9
+4 4 4
+7 9
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect
new file mode 100644
index 0000000000..f4e6be29b1
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect
@@ -0,0 +1,49 @@
+git-issue-697j.dfy(41,12): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(45,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(46,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(47,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(50,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(51,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(55,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(56,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(57,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(59,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(60,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(110,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(111,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(112,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(113,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(117,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(118,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(119,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(144,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(145,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(146,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(147,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(151,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(152,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(153,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(178,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(179,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(180,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(181,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(185,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(186,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(187,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(212,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(213,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(214,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(215,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(219,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(220,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(221,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(240,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(241,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(244,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(245,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(246,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(247,10): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(259,13): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(277,13): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(278,13): Warning: /!\ No terms found to trigger on.
+git-issue-697j.dfy(279,13): Warning: /!\ No terms found to trigger on.
diff --git a/docs/dev/news/4919.fix b/docs/dev/news/4919.fix
new file mode 100644
index 0000000000..a1ed74df99
--- /dev/null
+++ b/docs/dev/news/4919.fix
@@ -0,0 +1 @@
+Compile run-time constraint checks for newtypes in comprehensions
diff --git a/docs/dev/news/4930.fix b/docs/dev/news/4930.fix
new file mode 100644
index 0000000000..e5715cf937
--- /dev/null
+++ b/docs/dev/news/4930.fix
@@ -0,0 +1 @@
+Initialize additional fields in the AST