diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml
index 2b1fc10479a..a36595910f6 100644
--- a/.github/workflows/msbuild.yml
+++ b/.github/workflows/msbuild.yml
@@ -161,7 +161,7 @@ jobs:
           output: both
           # Fail if less than 86% total coverage, measured across all packages combined.
           # Report "yellow" status if less than 90% total coverage.
-          thresholds: '86 90'
+          thresholds: '85 90'
 
       - name: Code coverage report (LSP)
         uses: irongut/CodeCoverageSummary@v1.3.0
diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs
index 1d1db731578..9e28b8bfce7 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs
@@ -77,6 +77,10 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext re
     Contract.Requires(this != null);
     Contract.Requires(resolutionContext != null);
 
+    if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) {
+      resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_assign_such_that_forbidden,
+        Tok, "assign-such-that statement forbidden by the --enforce-determinism option");
+    }
     base.GenResolve(resolver, resolutionContext);
 
     if (AssumeToken != null) {
diff --git a/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs b/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs
index 73e32f52b8e..6146bc29952 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs
@@ -16,4 +16,10 @@ private HavocRhs(Cloner cloner, HavocRhs havocRhs) : base(cloner, havocRhs) {
   public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
   public override IEnumerable<INode> Children => Enumerable.Empty<Node>();
   public override IEnumerable<INode> PreResolveChildren => Enumerable.Empty<Node>();
+
+  public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+    if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) {
+      resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_nondeterminism_forbidden, Tok, "nondeterministic assignment forbidden by the --enforce-determinism option");
+    }
+  }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs
index 60e52485d2a..4ad76ab0c4f 100644
--- a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs
+++ b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs
@@ -57,4 +57,49 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       formatter.VisitAlternatives(Alternatives, indentBefore);
     });
   }
+
+  public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+    if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism && 2 <= Alternatives.Count) {
+      resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_case_based_if_forbidden, Tok,
+        "case-based if statement forbidden by the --enforce-determinism option");
+    }
+    ResolveAlternatives(resolver, Alternatives, null, resolutionContext);
+  }
+
+  public static void ResolveAlternatives(INewOrOldResolver resolver, List<GuardedAlternative> alternatives,
+    AlternativeLoopStmt loopToCatchBreaks, ResolutionContext resolutionContext) {
+    Contract.Requires(alternatives != null);
+    Contract.Requires(resolutionContext != null);
+
+    // first, resolve the guards
+    foreach (var alternative in alternatives) {
+      int prevErrorCount = resolver.Reporter.Count(ErrorLevel.Error);
+      resolver.ResolveExpression(alternative.Guard, resolutionContext);  // follows from postcondition of ResolveExpression
+      bool successfullyResolved = resolver.Reporter.Count(ErrorLevel.Error) == prevErrorCount;
+      resolver.ConstrainTypeExprBool(alternative.Guard, "condition is expected to be of type bool, but is {0}");
+    }
+
+    if (loopToCatchBreaks != null) {
+      resolver.LoopStack.Add(loopToCatchBreaks);  // push
+    }
+    foreach (var alternative in alternatives) {
+      resolver.Scope.PushMarker();
+      resolver.DominatingStatementLabels.PushMarker();
+      if (alternative.IsBindingGuard) {
+        var exists = (ExistsExpr)alternative.Guard;
+        foreach (var v in exists.BoundVars) {
+          resolver.ScopePushAndReport(resolver.Scope, v, "bound-variable");
+        }
+      }
+      resolver.ResolveAttributes(alternative, resolutionContext);
+      foreach (Statement ss in alternative.Body) {
+        resolver.ResolveStatementWithLabels(ss, resolutionContext);
+      }
+      resolver.DominatingStatementLabels.PopMarker();
+      resolver.Scope.PopMarker();
+    }
+    if (loopToCatchBreaks != null) {
+      resolver.LoopStack.RemoveAt(resolver.LoopStack.Count - 1);  // pop
+    }
+  }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs
index 78b9ed3bbaf..ed5717638e4 100644
--- a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs
+++ b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs
@@ -86,4 +86,36 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     }
     return false;
   }
+
+  public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+    if (Guard != null) {
+      if (!resolutionContext.IsGhost && IsBindingGuard && resolver.Options.ForbidNondeterminism) {
+        resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_binding_if_forbidden, Tok, "binding if statement forbidden by the --enforce-determinism option");
+      }
+      resolver.ResolveExpression(Guard, resolutionContext);
+      resolver.ConstrainTypeExprBool(Guard, "condition is expected to be of type bool, but is {0}");
+    } else {
+      if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) {
+        resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_nondeterministic_if_forbidden, Tok, "nondeterministic if statement forbidden by the --enforce-determinism option");
+      }
+    }
+
+    resolver.Scope.PushMarker();
+    if (IsBindingGuard) {
+      var exists = (ExistsExpr)Guard;
+      foreach (var v in exists.BoundVars) {
+        resolver.ScopePushAndReport(resolver.Scope, v.Name, v, v.Tok, "bound-variable");
+      }
+    }
+    resolver.DominatingStatementLabels.PushMarker();
+    resolver.ResolveBlockStatement(Thn, resolutionContext);
+    resolver.DominatingStatementLabels.PopMarker();
+    resolver.Scope.PopMarker();
+
+    if (Els != null) {
+      resolver.DominatingStatementLabels.PushMarker();
+      resolver.ResolveStatement(Els, resolutionContext);
+      resolver.DominatingStatementLabels.PopMarker();
+    }
+  }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
index 334b46688d2..7551fe9fd3d 100644
--- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
+++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
@@ -98,11 +98,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               var rhsTypes = new List<Type>();
               foreach (var assignStmt in assignStmts) {
                 var rhs = assignStmt.Rhs;
-                if (rhs is HavocRhs) {
-                  if (Options.ForbidNondeterminism) {
-                    Error(ErrorId.c_nondeterminism_forbidden, rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
-                  }
-                } else {
+                if (rhs is not HavocRhs) {
                   var lhs = assignStmt.Lhs;
                   rhss.Add(rhs);
                   lhss.Add(lhs);
@@ -129,9 +125,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             var s = assignStmt;
             Contract.Assert(s.Lhs is not SeqSelectExpr expr || expr.SelectOne);  // multi-element array assignments are not allowed
             if (s.Rhs is HavocRhs) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_nondeterminism_forbidden, s.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
-              }
             } else if (s.Rhs is TypeRhs typeRhs) {
               var lvalue = CreateLvalue(s.Lhs, wr, wStmts);
               wStmts = wr.Fork();
@@ -157,9 +150,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
           }
         case AssignSuchThatStmt thatStmt: {
             var s = thatStmt;
-            if (Options.ForbidNondeterminism) {
-              Error(ErrorId.c_assign_such_that_forbidden, s.Tok, "assign-such-that statement forbidden by the --enforce-determinism option", wr);
-            }
             var lhss = s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var);  // the resolver allows only IdentifierExpr left-hand sides
             var missingBounds = BoundedPool.MissingBounds(lhss, s.Bounds, BoundedPool.PoolVirtues.Enumerable);
             if (missingBounds.Count != 0) {
@@ -216,9 +206,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
         case IfStmt ifStmt: {
             IfStmt s = ifStmt;
             if (s.Guard == null) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_nondeterministic_if_forbidden, s.Tok, "nondeterministic if statement forbidden by the --enforce-determinism option", wr);
-              }
               // we can compile the branch of our choice
               ConcreteSyntaxTree guardWriter;
               if (s.Els == null) {
@@ -241,10 +228,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
                 Coverage.UnusedInstrumentationPoint(s.Els.Tok, "else branch");
               }
             } else {
-              if (s.IsBindingGuard && Options.ForbidNondeterminism) {
-                Error(ErrorId.c_binding_if_forbidden, s.Tok, "binding if statement forbidden by the --enforce-determinism option", wr);
-              }
-
               var coverageForElse = Coverage.IsRecording && !(s.Els is IfStmt);
               var thenWriter = EmitIf(out var guardWriter, s.Els != null || coverageForElse, wr);
               EmitExpr(s.IsBindingGuard ? ((ExistsExpr)s.Guard).AlphaRename("eg_d") : s.Guard, false, guardWriter, wStmts);
@@ -272,9 +255,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
           }
         case AlternativeStmt alternativeStmt: {
             var s = alternativeStmt;
-            if (Options.ForbidNondeterminism && 2 <= s.Alternatives.Count) {
-              Error(ErrorId.c_case_based_if_forbidden, s.Tok, "case-based if statement forbidden by the --enforce-determinism option", wr);
-            }
             foreach (var alternative in s.Alternatives) {
               var thn = EmitIf(out var guardWriter, true, wr);
               EmitExpr(alternative.IsBindingGuard ? ((ExistsExpr)alternative.Guard).AlphaRename("eg_d") : alternative.Guard, false, guardWriter, wStmts);
@@ -294,9 +274,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               return;
             }
             if (s.Guard == null) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_non_deterministic_loop_forbidden, s.Tok, "nondeterministic loop forbidden by the --enforce-determinism option", wr);
-              }
               // This loop is allowed to stop iterating at any time. We choose to never iterate, but we still
               // emit a loop structure. The structure "while (false) { }" comes to mind, but that results in
               // an "unreachable code" error from Java, so we instead use "while (true) { break; }".
@@ -312,9 +289,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             break;
           }
         case AlternativeLoopStmt loopStmt: {
-            if (Options.ForbidNondeterminism) {
-              Error(ErrorId.c_case_based_loop_forbidden, loopStmt.Tok, "case-based loop forbidden by the --enforce-determinism option", wr);
-            }
             if (loopStmt.Alternatives.Count != 0) {
               var w = CreateWhileLoop(out var whileGuardWriter, wr);
               EmitExpr(Expression.CreateBoolLiteral(loopStmt.tok, true), false, whileGuardWriter, wStmts);
@@ -361,9 +335,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             }
             var s0 = (AssignStmt)s.S0;
             if (s0.Rhs is HavocRhs) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_nondeterminism_forbidden, s0.Rhs.Tok, "nondeterministic assignment forbidden by --enforce-determinism", wr);
-              }
               // The forall statement says to havoc a bunch of things.  This can be efficiently compiled
               // into doing nothing.
               return;
@@ -527,8 +498,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             var s = modifyStmt;
             if (s.Body != null) {
               TrStmt(s.Body, wr);
-            } else if (Options.ForbidNondeterminism) {
-              Error(ErrorId.c_bodyless_modify_statement_forbidden, s.Tok, "modify statement without a body forbidden by the --enforce-determinism option", wr);
             }
 
             break;
diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
index b996ea13cec..2bcef3478f0 100644
--- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
@@ -1611,11 +1611,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
           }
         } else if (d is IteratorDecl) {
           var iter = (IteratorDecl)d;
-          if (Options.ForbidNondeterminism && iter.Outs.Count > 0) {
-            Error(ErrorId.c_iterators_are_not_deterministic, iter.tok,
-              "since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option",
-              wr);
-          }
 
           var wIter = CreateIterator(iter, wr);
           if (iter.Body == null) {
@@ -1669,15 +1664,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
             }
           }
 
-          if (Options.ForbidNondeterminism &&
-              !classIsExtern &&
-              !cl.Members.Exists(member => member is Constructor) &&
-              cl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) {
-            Error(ErrorId.c_constructorless_class_forbidden, cl.tok,
-              "since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option",
-              wr);
-          }
-
           if (include) {
             var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(cl),
               classIsExtern, cl.FullName,
diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 6ef92d58f0c..40f29a3b3b9 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -353,7 +353,8 @@ public enum ContractTestingMode {
     public bool WarnShadowing = false;
     public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version4;
     public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version4;
-    public int DefiniteAssignmentLevel = 1; // [0..5] 2 and 3 have the same effect, 4 turns off an array initialisation check and field initialization check, unless --enforce-determinism is used.
+
+    public int DefiniteAssignmentLevel { get; set; } = 1;
     public HashSet<string> LibraryFiles { get; set; } = new();
     public ContractTestingMode TestContracts = ContractTestingMode.None;
 
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index fe8b2223946..0c0ea425ff5 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -537,7 +537,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
 
     DafnyOptions.RegisterLegacyBinding(EnforceDeterminism, (options, value) => {
       options.ForbidNondeterminism = value;
-      options.DefiniteAssignmentLevel = 4;
+      if (!options.Get(RelaxDefiniteAssignment)) {
+        options.DefiniteAssignmentLevel = 4;
+      }
     });
     RelaxDefiniteAssignment.AddValidator(optionResult => {
       var enforceDeterminismResult = optionResult.FindResultFor(EnforceDeterminism);
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index d3d3eadbe7a..033c02f71e1 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -51,7 +51,6 @@ static DafnyCommands() {
   public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
     BoogieOptionBag.HiddenNoVerify,
-    CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,
     DeveloperOptionBag.Bootstrapping,
@@ -110,6 +109,7 @@ static DafnyCommands() {
     CommonOptionBag.WarnMissingConstructorParenthesis,
     PrintStmt.TrackPrintEffectsOption,
     CommonOptionBag.AllowAxioms,
+    CommonOptionBag.EnforceDeterminism,
     MethodOrFunction.AllowExternalContracts,
     DafnyProject.FindProjectOption
   }).Concat(ParserOptions).ToList();
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index 18d48daf379..4d27481471b 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -1478,6 +1478,22 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
       // Further checks
       // ----------------------------------------------------------------------------
 
+      foreach (TopLevelDecl d in declarations) {
+        if (d is ClassLikeDecl classLikeDecl) {
+          var classIsExtern = !Options.DisallowExterns && Attributes.Contains(classLikeDecl.Attributes, "extern");
+          if (Options.ForbidNondeterminism &&
+              !classIsExtern &&
+              !classLikeDecl.Members.Exists(member => member is Constructor) &&
+              classLikeDecl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) {
+            // This check should be moved to the resolver once we have a language construct to indicate the type is imported
+            // Instead of the extern attribute
+            Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_constructorless_class_forbidden,
+              classLikeDecl.tok,
+              "since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option");
+          }
+        }
+      }
+
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // Check that type-parameter variance is respected in type definitions
         foreach (TopLevelDecl d in declarations) {
@@ -2966,7 +2982,7 @@ public void ScopePushAndReport(Scope<IVariable> scope, IVariable v, string kind)
       ScopePushAndReport(scope, v.Name, v, v.Tok, kind);
     }
 
-    void ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {
+    public Scope<Thing>.PushResult ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {
       Contract.Requires(scope != null);
       Contract.Requires(name != null);
       Contract.Requires(thing != null);
@@ -2983,6 +2999,8 @@ void ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, ITo
           reporter.Warning(MessageSource.Resolver, ResolutionErrors.ErrorId.none, tok, "Shadowed {0} name: {1}", kind, name);
           break;
       }
+
+      return r;
     }
 
     /// <summary>
diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
index e0160e3cbc2..66a27e333de 100644
--- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
+++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
@@ -2925,6 +2925,11 @@ void ResolveIterator(IteratorDecl iter) {
       Contract.Requires(currentClass == null);
       Contract.Ensures(currentClass == null);
 
+      if (Options.ForbidNondeterminism && iter.Outs.Count > 0) {
+        Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_iterators_are_not_deterministic, iter.tok,
+          "since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option");
+      }
+
       var initialErrorCount = reporter.Count(ErrorLevel.Error);
 
       // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
@@ -3108,43 +3113,6 @@ public void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolut
       EnclosingStatementLabels.PopMarker();
     }
 
-    void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopStmt loopToCatchBreaks, ResolutionContext resolutionContext) {
-      Contract.Requires(alternatives != null);
-      Contract.Requires(resolutionContext != null);
-
-      // first, resolve the guards
-      foreach (var alternative in alternatives) {
-        int prevErrorCount = reporter.Count(ErrorLevel.Error);
-        ResolveExpression(alternative.Guard, resolutionContext);
-        Contract.Assert(alternative.Guard.Type != null);  // follows from postcondition of ResolveExpression
-        bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
-        ConstrainTypeExprBool(alternative.Guard, "condition is expected to be of type bool, but is {0}");
-      }
-
-      if (loopToCatchBreaks != null) {
-        LoopStack.Add(loopToCatchBreaks);  // push
-      }
-      foreach (var alternative in alternatives) {
-        scope.PushMarker();
-        DominatingStatementLabels.PushMarker();
-        if (alternative.IsBindingGuard) {
-          var exists = (ExistsExpr)alternative.Guard;
-          foreach (var v in exists.BoundVars) {
-            ScopePushAndReport(scope, v, "bound-variable");
-          }
-        }
-        ResolveAttributes(alternative, resolutionContext);
-        foreach (Statement ss in alternative.Body) {
-          ResolveStatementWithLabels(ss, resolutionContext);
-        }
-        DominatingStatementLabels.PopMarker();
-        scope.PopMarker();
-      }
-      if (loopToCatchBreaks != null) {
-        LoopStack.RemoveAt(LoopStack.Count - 1);  // pop
-      }
-    }
-
     /// <summary>
     /// Resolves the given call statement.
     /// Assumes all LHSs have already been resolved (and checked for mutability).
@@ -3775,8 +3743,8 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
           TypeRhs rr = (TypeRhs)s.Rhs;
           ResolveTypeRhs(rr, stmt, resolutionContext);
           AddAssignableConstraint(stmt.Tok, lhsType, rr.Type, "type {1} is not assignable to LHS (of type {0})");
-        } else if (s.Rhs is HavocRhs) {
-          // nothing else to do
+        } else if (s.Rhs is HavocRhs havocRhs) {
+          havocRhs.Resolve(this, resolutionContext);
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS
         }
@@ -3793,41 +3761,25 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
 
       } else if (stmt is IfStmt) {
         IfStmt s = (IfStmt)stmt;
-        if (s.Guard != null) {
-          ResolveExpression(s.Guard, resolutionContext);
-          Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression
-          ConstrainTypeExprBool(s.Guard, "condition is expected to be of type bool, but is {0}");
-        }
-
-        scope.PushMarker();
-        if (s.IsBindingGuard) {
-          var exists = (ExistsExpr)s.Guard;
-          foreach (var v in exists.BoundVars) {
-            ScopePushAndReport(scope, v, "bound-variable");
-          }
-        }
-        DominatingStatementLabels.PushMarker();
-        ResolveBlockStatement(s.Thn, resolutionContext);
-        DominatingStatementLabels.PopMarker();
-        scope.PopMarker();
-
-        if (s.Els != null) {
-          DominatingStatementLabels.PushMarker();
-          ResolveStatement(s.Els, resolutionContext);
-          DominatingStatementLabels.PopMarker();
-        }
-
+        s.Resolve(this, resolutionContext);
       } else if (stmt is AlternativeStmt) {
         var s = (AlternativeStmt)stmt;
-        ResolveAlternatives(s.Alternatives, null, resolutionContext);
-
+        s.Resolve(this, resolutionContext);
       } else if (stmt is OneBodyLoopStmt) {
         var s = (OneBodyLoopStmt)stmt;
-        if (s is WhileStmt whileS && whileS.Guard != null) {
-          ResolveExpression(whileS.Guard, resolutionContext);
-          Contract.Assert(whileS.Guard.Type != null);  // follows from postcondition of ResolveExpression
-          ConstrainTypeExprBool(whileS.Guard, "condition is expected to be of type bool, but is {0}");
-        } else if (s is ForLoopStmt forS) {
+        if (s is WhileStmt whileS) {
+          if (whileS.Guard != null) {
+            ResolveExpression(whileS.Guard, resolutionContext);
+            Contract.Assert(whileS.Guard.Type != null);  // follows from postcondition of ResolveExpression
+            ConstrainTypeExprBool(whileS.Guard, "condition is expected to be of type bool, but is {0}");
+          } else {
+            if (!resolutionContext.IsGhost && Options.ForbidNondeterminism) {
+              Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_non_deterministic_loop_forbidden, s.Tok,
+                "nondeterministic loop forbidden by the --enforce-determinism option");
+            }
+          }
+        }
+        if (s is ForLoopStmt forS) {
           var loopIndex = forS.LoopIndex;
           int prevErrorCount = reporter.Count(ErrorLevel.Error);
           ResolveType(loopIndex.Tok, loopIndex.Type, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null);
@@ -3872,9 +3824,12 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
 
       } else if (stmt is AlternativeLoopStmt) {
         var s = (AlternativeLoopStmt)stmt;
-        ResolveAlternatives(s.Alternatives, s, resolutionContext);
+        if (!resolutionContext.IsGhost && Options.ForbidNondeterminism) {
+          Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_case_based_loop_forbidden, s.Tok,
+            "case-based loop forbidden by the --enforce-determinism option");
+        }
+        AlternativeStmt.ResolveAlternatives(this, s.Alternatives, s, resolutionContext);
         ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, resolutionContext);
-
       } else if (stmt is ForallStmt) {
         var s = (ForallStmt)stmt;
 
@@ -3965,13 +3920,19 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
         }
 
       } else if (stmt is ModifyStmt) {
-        var s = (ModifyStmt)stmt;
-        ResolveAttributes(s.Mod, resolutionContext);
-        foreach (FrameExpression fe in s.Mod.Expressions) {
+        var modifyStmt = (ModifyStmt)stmt;
+        if (modifyStmt.Body == null) {
+          if (!resolutionContext.IsGhost && Options.ForbidNondeterminism) {
+            Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_bodyless_modify_statement_forbidden,
+              modifyStmt.Tok, "modify statement without a body forbidden by the --enforce-determinism option");
+          }
+        }
+        ResolveAttributes(modifyStmt.Mod, resolutionContext);
+        foreach (FrameExpression fe in modifyStmt.Mod.Expressions) {
           ResolveFrameExpression(fe, FrameExpressionUse.Modifies, resolutionContext);
         }
-        if (s.Body != null) {
-          ResolveBlockStatement(s.Body, resolutionContext);
+        if (modifyStmt.Body != null) {
+          ResolveBlockStatement(modifyStmt.Body, resolutionContext);
         }
 
       } else if (stmt is CalcStmt) {
diff --git a/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs b/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs
index 021c2808392..3e7101822a4 100644
--- a/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs
+++ b/Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs
@@ -17,4 +17,14 @@ public interface INewOrOldResolver {
   void ConstrainTypeExprBool(Expression expression, string message);
   void ResolveStatement(Statement statement, ResolutionContext resolutionContext);
   void ResolveTypeRhs(TypeRhs typeRhs, Statement statement, ResolutionContext resolutionContext);
+  void ResolveBlockStatement(BlockStmt blockS, ResolutionContext resolutionContext);
+
+  Scope<Thing>.PushResult ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok,
+    string kind) where Thing : class;
+
+  public void ScopePushAndReport(Scope<IVariable> scope, IVariable v, string kind) {
+    ScopePushAndReport(scope, v.Name, v, v.Tok, kind);
+  }
+
+  void ResolveStatementWithLabels(Statement statement, ResolutionContext resolutionContext);
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
index 129978be951..d514fcdbd94 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
@@ -25,7 +25,7 @@ public List<Statement> LoopStack {
     private List<Statement> loopStack = new();  // the enclosing loops (from which it is possible to break out)
     bool inBodyInitContext;  // "true" only if "currentMethod is Constructor"
 
-    void ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext) {
+    public void ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext) {
       Contract.Requires(blockStmt != null);
       Contract.Requires(resolutionContext != null);
 
@@ -48,7 +48,7 @@ void ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionCont
       }
     }
 
-    void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext) {
+    public void ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext) {
       Contract.Requires(stmt != null);
       Contract.Requires(resolutionContext != null);
 
@@ -252,8 +252,8 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
           var rr = (TypeRhs)s.Rhs;
           ResolveTypeRhs(rr, stmt, resolutionContext);
           AddSubtypeConstraint(lhsPreType, rr.PreType, stmt.Tok, "type {1} is not assignable to LHS (of type {0})");
-        } else if (s.Rhs is HavocRhs) {
-          // nothing else to do
+        } else if (s.Rhs is HavocRhs havocRhs) {
+          havocRhs.Resolve(this, resolutionContext);
         } else {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS
         }
@@ -266,41 +266,22 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
         ResolveBlockStatement(blockStmt, resolutionContext);
         scope.PopMarker();
 
-      } else if (stmt is IfStmt) {
-        var s = (IfStmt)stmt;
-        if (s.Guard != null) {
-          ResolveExpression(s.Guard, resolutionContext);
-          ConstrainTypeExprBool(s.Guard, "condition is expected to be of type bool, but is {0}");
-        }
-
-        scope.PushMarker();
-        if (s.IsBindingGuard) {
-          var exists = (ExistsExpr)s.Guard;
-          foreach (var v in exists.BoundVars) {
-            ScopePushAndReport(v, "bound-variable", false);
-          }
-        }
-        DominatingStatementLabels.PushMarker();
-        ResolveBlockStatement(s.Thn, resolutionContext);
-        DominatingStatementLabels.PopMarker();
-        scope.PopMarker();
-
-        if (s.Els != null) {
-          DominatingStatementLabels.PushMarker();
-          ResolveStatement(s.Els, resolutionContext);
-          DominatingStatementLabels.PopMarker();
-        }
-
+      } else if (stmt is IfStmt ifStmt) {
+        ifStmt.Resolve(this, resolutionContext);
       } else if (stmt is AlternativeStmt) {
         var s = (AlternativeStmt)stmt;
-        ResolveAlternatives(s.Alternatives, null, resolutionContext);
+        s.Resolve(this, resolutionContext);
 
       } else if (stmt is OneBodyLoopStmt oneBodyLoopStmt) {
         ResolveOneBodyLoopStmt(oneBodyLoopStmt, resolutionContext);
 
       } else if (stmt is AlternativeLoopStmt) {
         var s = (AlternativeLoopStmt)stmt;
-        ResolveAlternatives(s.Alternatives, s, resolutionContext);
+        if (!resolutionContext.IsGhost && Options.ForbidNondeterminism) {
+          Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_case_based_loop_forbidden, s.Tok,
+            "case-based loop forbidden by the --enforce-determinism option");
+        }
+        AlternativeStmt.ResolveAlternatives(this, s.Alternatives, s, resolutionContext);
         ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, resolutionContext);
 
       } else if (stmt is ForallStmt) {
@@ -391,6 +372,12 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
         }
 
       } else if (stmt is ModifyStmt modifyStmt) {
+        if (modifyStmt.Body == null) {
+          if (!resolutionContext.IsGhost && Options.ForbidNondeterminism) {
+            Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_bodyless_modify_statement_forbidden,
+              modifyStmt.Tok, "modify statement without a body forbidden by the --enforce-determinism option");
+          }
+        }
         ResolveAttributes(modifyStmt.Mod, resolutionContext, false);
         foreach (FrameExpression fe in modifyStmt.Mod.Expressions) {
           ResolveFrameExpression(fe, FrameExpressionUse.Modifies, resolutionContext.CodeContext);
@@ -424,11 +411,18 @@ private void ResolveOneBodyLoopStmt(OneBodyLoopStmt s, ResolutionContext resolut
       Contract.Requires(s != null);
       Contract.Requires(resolutionContext != null);
 
-      if (s is WhileStmt whileS && whileS.Guard != null) {
-        ResolveExpression(whileS.Guard, resolutionContext);
-        ConstrainTypeExprBool(whileS.Guard, "condition is expected to be of type bool, but is {0}");
-
-      } else if (s is ForLoopStmt forS) {
+      if (s is WhileStmt whileS) {
+        if (whileS.Guard != null) {
+          ResolveExpression(whileS.Guard, resolutionContext);
+          ConstrainTypeExprBool(whileS.Guard, "condition is expected to be of type bool, but is {0}");
+        } else {
+          if (!resolutionContext.IsGhost && Options.ForbidNondeterminism) {
+            Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_non_deterministic_loop_forbidden, s.Tok,
+              "nondeterministic loop forbidden by the --enforce-determinism option");
+          }
+        }
+      }
+      if (s is ForLoopStmt forS) {
         var loopIndex = forS.LoopIndex;
         resolver.ResolveType(loopIndex.tok, loopIndex.Type, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null);
         loopIndex.PreType = Type2PreType(loopIndex.Type);
@@ -1266,39 +1260,5 @@ public void CheckIsLvalue(Expression lhs, ResolutionContext resolutionContext) {
         ReportError(lhs, "LHS of assignment must denote a mutable variable or field");
       }
     }
-
-    void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopStmt loopToCatchBreaks, ResolutionContext resolutionContext) {
-      Contract.Requires(alternatives != null);
-      Contract.Requires(resolutionContext != null);
-
-      // first, resolve the guards
-      foreach (var alternative in alternatives) {
-        ResolveExpression(alternative.Guard, resolutionContext);
-        ConstrainExpressionToBoolFamily(alternative.Guard, "condition is expected to be of type bool, but is {0}");
-      }
-
-      if (loopToCatchBreaks != null) {
-        loopStack.Add(loopToCatchBreaks);  // push
-      }
-      foreach (var alternative in alternatives) {
-        scope.PushMarker();
-        DominatingStatementLabels.PushMarker();
-        if (alternative.IsBindingGuard) {
-          var exists = (ExistsExpr)alternative.Guard;
-          foreach (var v in exists.BoundVars) {
-            ScopePushAndReport(v, "bound-variable", false);
-          }
-        }
-        ResolveAttributes(alternative, resolutionContext, false);
-        foreach (Statement ss in alternative.Body) {
-          ResolveStatementWithLabels(ss, resolutionContext);
-        }
-        DominatingStatementLabels.PopMarker();
-        scope.PopMarker();
-      }
-      if (loopToCatchBreaks != null) {
-        loopStack.RemoveAt(loopStack.Count - 1);  // pop
-      }
-    }
   }
 }
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
index ae4bfffdc80..c3f1c519459 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
@@ -483,7 +483,7 @@ void ScopePushExpectSuccess(IVariable v, string kind, bool assignPreType = true)
       Contract.Assert(r == Scope<IVariable>.PushResult.Success);
     }
 
-    private Scope<Thing>.PushResult ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {
+    public Scope<Thing>.PushResult ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {
       Contract.Requires(scope != null);
       Contract.Requires(name != null);
       Contract.Requires(thing != null);
@@ -1173,6 +1173,11 @@ void ResolveIterator(IteratorDecl iter) {
       Contract.Requires(currentClass != null);
       Contract.Ensures(currentClass == null);
 
+      if (Options.ForbidNondeterminism && iter.Outs.Count > 0) {
+        Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_iterators_are_not_deterministic, iter.tok,
+          "since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option");
+      }
+
       var initialErrorCount = ErrorCount;
 
       // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
diff --git a/Source/DafnyLanguageServer/LanguageServer.cs b/Source/DafnyLanguageServer/LanguageServer.cs
index 2d15d60eebb..703fbc13e58 100644
--- a/Source/DafnyLanguageServer/LanguageServer.cs
+++ b/Source/DafnyLanguageServer/LanguageServer.cs
@@ -31,7 +31,6 @@ public class LanguageServer {
         DeveloperOptionBag.SplitPrint,
         DeveloperOptionBag.PassivePrint,
         DeveloperOptionBag.BoogiePrint,
-        CommonOptionBag.EnforceDeterminism,
         InternalDocstringRewritersPluginConfiguration.UseJavadocLikeDocstringRewriterOption,
         LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable
       }.Concat(DafnyCommands.VerificationOptions).
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
index 5b41109117e..efbb14093aa 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
index 2e52dcdc008..05b667c0ace 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
index 9114b3e675a..76712922d81 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
index dd6f2ce4eaa..a9a03b49ee0 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
index d6fe8035c8d..3cbe8a60a47 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
index fa7098329d3..0e92d6f70e7 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
index 653552ed23b..5b889ca5e9b 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ
diff --git a/Source/DafnyStandardLibraries/scripts/check-examples b/Source/DafnyStandardLibraries/scripts/check-examples
index 72f22dc9035..55704e82a16 100755
--- a/Source/DafnyStandardLibraries/scripts/check-examples
+++ b/Source/DafnyStandardLibraries/scripts/check-examples
@@ -268,7 +268,7 @@ do
               fi
               msg=
               if [ "$actualec" != "$ec" ]; then
-                echo EXPECTED EXIT CODE $ec, got $actualec
+                echo EXPECTED EXIT CODE $ec, got "$actualec"
                 FAIL=1
               fi
             else 
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml
index 867c9d20a22..461c37199c3 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml
@@ -7,7 +7,7 @@ includes = []
 # Options that help support more values of consuming context options
 # (mostly turning on any more restrictive verification)
 track-print-effects = true
-enforce-determinism = true
+enforce-determinism = false
 reads-clauses-on-methods = true
 
 # Options important for sustainable development
diff --git a/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml b/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml
index a7e65f28638..9270d335637 100644
--- a/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml
+++ b/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml
@@ -7,7 +7,7 @@ excludes = [
 # Options that help support more values of consuming context options
 # (mostly turning on any more restrictive verification)
 track-print-effects = true
-enforce-determinism = true
+enforce-determinism = false
 reads-clauses-on-methods = true
 
 # Options important for sustainable development
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy
index 48ed58160d2..024565ee406 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy
@@ -1,62 +1,6 @@
-// RUN: ! %verify "%s" > "%t"
-// RUN: ! %baredafny run %args --enforce-determinism "%s" >> "%t"
+// RUN: ! %verify --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-class C {
-  var f: real
-}
-
-predicate P(z: int) { true }
-
-method M(c: C, u: int) returns (r: int)
-  modifies c
-  decreases *
-{
-  var x := 3;  // fine
-  var y;  // this statement by itself is nondeterministic, but by itself is not an error
-  if u < 10 {
-    r := y;  // error: definite-assignment violation
-  } else if u < 20 {
-    y := 4;
-    r := y;  // fine
-  } else if u < 30 {
-    y := 4;
-    y := *;  // compiler error under deterministic rules
-    r := y;  // allowed by definite-assignment rules, but the previous line is reported by compiler
-  }
-  r := x;
-}
-
-method OutputParameters0(x: int) returns (s: int, t: int)
-{
-  return x, x+45;  // yes, this is legal
-}
-
-method OutputParameters1(x: int) returns (s: int, t: int)
-{
-  if x < 100 {
-    return;  // error (x2): this may leave s and t undefined
-  } else {
-    var y := x + s;  // error: this uses s before it may be defined
-  }
-}  // error: this may leave t undefined (s, too, but it has been checked on all paths leading here)
-
-method DeclWithHavoc()
-{
-  var a: int := *; // this counts as a definite assignment
-  var b: int;  // fine, since b is never used
-  var c := a;
-}
-
-type PossiblyEmpty = x: int | true witness *
-
-method MoreDeclWithHavoc()
-{
-  var a: PossiblyEmpty := *; // this does NOT count as a definite assignment for a possibly-empty type
-  var b: PossiblyEmpty;  // fine, since b is never used
-  var c := a; // error: a is used without being definitely assigned
-}
-
 class CK {
   var x: int
   var y: int
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy.expect
index 3a3b095195c..2cd5cf89b77 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminism.dfy.expect
@@ -1,20 +1,6 @@
-ForbidNondeterminism.dfy(18,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
-ForbidNondeterminism.dfy(38,4): Error: out-parameter 's', which is subject to definite-assignment rules, might be uninitialized at this return point
-ForbidNondeterminism.dfy(38,4): Error: out-parameter 't', which is subject to definite-assignment rules, might be uninitialized at this return point
-ForbidNondeterminism.dfy(40,17): Error: variable 's', which is subject to definite-assignment rules, might be uninitialized here
-ForbidNondeterminism.dfy(42,0): Error: out-parameter 't', which is subject to definite-assignment rules, might be uninitialized at this return point
-ForbidNondeterminism.dfy(57,11): Error: variable 'a', which is subject to definite-assignment rules, might be uninitialized here
+ForbidNondeterminism.dfy(9,2): Error: field 'y', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
+ForbidNondeterminism.dfy(14,11): Error: unless an initializer is provided for the array elements, a new array of 'int' must have empty size
+ForbidNondeterminism.dfy(15,11): Error: unless an initializer is provided for the array elements, a new array of 'bool' must have empty size
+ForbidNondeterminism.dfy(23,2): Error: field 'data', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
 
-Dafny program verifier finished with 3 verified, 6 errors
-ForbidNondeterminism.dfy(18,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
-ForbidNondeterminism.dfy(38,4): Error: out-parameter 's', which is subject to definite-assignment rules, might be uninitialized at this return point
-ForbidNondeterminism.dfy(38,4): Error: out-parameter 't', which is subject to definite-assignment rules, might be uninitialized at this return point
-ForbidNondeterminism.dfy(40,17): Error: variable 's', which is subject to definite-assignment rules, might be uninitialized here
-ForbidNondeterminism.dfy(42,0): Error: out-parameter 't', which is subject to definite-assignment rules, might be uninitialized at this return point
-ForbidNondeterminism.dfy(57,11): Error: variable 'a', which is subject to definite-assignment rules, might be uninitialized here
-ForbidNondeterminism.dfy(70,11): Error: unless an initializer is provided for the array elements, a new array of 'int' must have empty size
-ForbidNondeterminism.dfy(71,11): Error: unless an initializer is provided for the array elements, a new array of 'bool' must have empty size
-ForbidNondeterminism.dfy(65,2): Error: field 'y', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
-ForbidNondeterminism.dfy(79,2): Error: field 'data', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
-
-Dafny program verifier finished with 2 verified, 10 errors
+Dafny program verifier finished with 0 verified, 4 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismCompile.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismCompile.dfy.expect
deleted file mode 100644
index c796a1a3252..00000000000
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismCompile.dfy.expect
+++ /dev/null
@@ -1,18 +0,0 @@
-ForbidNondeterminismCompile.dfy(51,11): Warning: the modify statement with a block statement is deprecated
-
-Dafny program verifier finished with 6 verified, 0 errors
-ForbidNondeterminismCompile.dfy(17,7): Error: nondeterministic assignment forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(18,13): Error: nondeterministic assignment forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(19,4): Error: assign-such-that statement forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(20,2): Error: nondeterministic if statement forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(23,2): Error: case-based if statement forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(32,2): Error: binding if statement forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(35,2): Error: nondeterministic loop forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(40,2): Error: case-based loop forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(48,12): Error: nondeterministic assignment forbidden by --enforce-determinism
-ForbidNondeterminismCompile.dfy(50,2): Error: modify statement without a body forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(64,16): Error: nondeterministic assignment forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(4,6): Error: since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(79,9): Error: since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(90,6): Error: since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option
-Translation was aborted because errors were found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismCompile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismResolve.dfy
similarity index 68%
rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismCompile.dfy
rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismResolve.dfy
index c4920644933..2d8ed02bbbc 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismCompile.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismResolve.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %baredafny build %args --enforce-determinism "%s" --target cs > "%t"
+// RUN: ! %resolve --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C { // error: constructor-less class not allowed by determinism rules
@@ -101,3 +101,45 @@ class D {
     u := 90;
   }
 }
+
+ghost method M2(c: C)
+  modifies c
+{
+  var x := 3;  // fine
+  var y;  // this statement by itself is nondeterministic, but the verifier catches bad uses of "y"
+  y := 4;
+  y := *;  // error: nondeterministic
+  x, y := x, *;  // error: nondeterministic
+  y :| true;  // error: nondeterministic
+  if * {  // error: nondeterministic
+    x := x + 1;
+  }
+  if {  // error: nondeterministic
+    case true =>  x := x + 1;
+    case true =>  x := x + 2;
+  }
+  if c.f < 500.0 {
+    if {  // a one-case if is always deterministic
+      case c.f < 1000.0 => x := x + 1;
+    }
+  }
+  if z :| 10 <= z < 15 && P(z) {  // error: nondeterministic
+    x := z;
+  }
+  while *  // error: nondeterministic
+    decreases *
+  {
+    x := x + 1;
+  }
+  while  // error: nondeterministic
+    decreases if x <= 100 then 100-x else x
+  {
+    case x < 100 => x := x + 1;
+    case 100 < x => x := x - 1;
+  }
+  var a := new int[100](_ => 750);
+  forall i | 0 <= i < a.Length {
+    a[i] := *;  // error: nondeterministic
+  }
+  modify c;  // error: nondeterministic
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismResolve.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismResolve.dfy.expect
new file mode 100644
index 00000000000..0559c3b613f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForbidNondeterminismResolve.dfy.expect
@@ -0,0 +1,17 @@
+ForbidNondeterminismResolve.dfy(51,11): Warning: the modify statement with a block statement is deprecated
+ForbidNondeterminismResolve.dfy(17,7): Error: nondeterministic assignment forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(18,13): Error: nondeterministic assignment forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(19,4): Error: assign-such-that statement forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(20,2): Error: nondeterministic if statement forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(23,2): Error: case-based if statement forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(32,2): Error: binding if statement forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(35,2): Error: nondeterministic loop forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(40,2): Error: case-based loop forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(48,12): Error: nondeterministic assignment forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(50,2): Error: modify statement without a body forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(64,16): Error: nondeterministic assignment forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(130,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ForbidNondeterminismResolve.dfy(79,9): Error: since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(4,6): Error: since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option
+ForbidNondeterminismResolve.dfy(90,6): Error: since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option
+15 resolution/type errors detected in ForbidNondeterminismResolve.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy
index bce0d4ff9b8..e5cf712259c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 3 %baredafny build --show-snippets:false --use-basename-for-filename --enforce-determinism "%s" > "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method NondetIf() returns (x: int) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy.expect
index d02e6eada6c..c0df67e0608 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2959.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 2 verified, 0 errors
 git-issue-2959.dfy(5,2): Error: nondeterministic if statement forbidden by the --enforce-determinism option
 git-issue-2959.dfy(13,7): Error: nondeterministic assignment forbidden by the --enforce-determinism option
-Translation was aborted because errors were found
+2 resolution/type errors detected in git-issue-2959.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy
index 97359697131..43a9d2428cc 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy
@@ -437,6 +437,7 @@ method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
 
 class C {
   var x: int
+  constructor() {}
 }
 
 function {:testEntry} GetX(c: C): int
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
index 16096f0920b..d62764dd7ab 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect
@@ -454,17 +454,18 @@ method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
 
 class C {
   var x: int
+  constructor() {}
 }
 
 function {:testEntry} GetX(c: C): int
   reads c
 {
-  </span><span class="pc" id="445:3">c.x
-</span><span class="na" id="446:1">}
+  </span><span class="pc" id="446:3">c.x
+</span><span class="na" id="447:1">}
 
 method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
-  assume </span><span class="pc" id="449:10">t</span><span class="na" id="449:11">rue;
-  assert 1 + x </span><span class="fc" id="450:16">=</span><span class="na" id="450:17">= x + 1;
+  assume </span><span class="pc" id="450:10">t</span><span class="na" id="450:11">rue;
+  assert 1 + x </span><span class="fc" id="451:16">=</span><span class="na" id="451:17">= x + 1;
 }
 
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
index 10bf59ea072..1709907f977 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect
@@ -454,16 +454,17 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (
 
 </span><span class="na" id="438:1">class C {
   var x: int
+  constructor() {}
 }
 
 function {:testEntry} GetX(c: C): int
   reads c
 {
-  </span><span class="nc" id="445:3">c.</span><span class="na" id="445:5">x
+  </span><span class="nc" id="446:3">c.</span><span class="na" id="446:5">x
 }
 
 method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
-  assume </span><span class="nc" id="449:10">t</span><span class="na" id="449:11">rue;
+  assume </span><span class="nc" id="450:10">t</span><span class="na" id="450:11">rue;
   assert 1 + x == x + 1;
 }
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
index 34830695408..a953198340b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect
@@ -454,12 +454,13 @@ method {:testEntry} CalcStatementWithSideConditions(x: int) {
 
 </span><span class="na" id="438:1">class C {
   var x: int
+  constructor() {}
 }
 
-</span><span class="fc" id="442:1">function {:testEntry} GetX(c: C): int
-</span><span class="na" id="443:1">  reads c
+</span><span class="fc" id="443:1">function {:testEntry} GetX(c: C): int
+</span><span class="na" id="444:1">  reads c
 {
-</span><span class="fc" id="445:1">  c.x
+</span><span class="fc" id="446:1">  c.x
 }
 
 method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
@@ -467,7 +468,7 @@ method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
   assert 1 + x == x + 1;
 }
 
-</span><span class="na" id="453:1">}
+</span><span class="na" id="454:1">}
 
 </span></pre>
 <div class="footer">
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
index af02650fdbd..190aaf70aed 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect
@@ -454,17 +454,18 @@ method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) {
 
 class C {
   var x: int
+  constructor() {}
 }
 
 function {:testEntry} GetX(c: C): int
   reads c
 {
-  </span><span class="nc" id="445:3">c.</span><span class="pc" id="445:5">x
-</span><span class="na" id="446:1">}
+  </span><span class="nc" id="446:3">c.</span><span class="pc" id="446:5">x
+</span><span class="na" id="447:1">}
 
 method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) {
-  assume </span><span class="nc" id="449:10">t</span><span class="na" id="449:11">rue;
-  assert 1 + x </span><span class="fc" id="450:16">=</span><span class="na" id="450:17">= x + 1;
+  assume </span><span class="nc" id="450:10">t</span><span class="na" id="450:11">rue;
+  assert 1 + x </span><span class="fc" id="451:16">=</span><span class="na" id="451:17">= x + 1;
 }
 
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
index c85ea5d9b9b..2babb39106a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
@@ -172,6 +172,6 @@
 //
 // CHECK: Results for M.GetX \(well-formedness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencies.dfy\(445,5\)-\(445,5\): target object is never null
+// CHECK:       ProofDependencies.dfy\(446,5\)-\(446,5\): target object is never null
 
 include "ProofDependencies.dfy"
diff --git a/docs/HowToFAQ/Errors-Compiler.md b/docs/HowToFAQ/Errors-Compiler.md
index 4203dd1e349..da243df24e4 100644
--- a/docs/HowToFAQ/Errors-Compiler.md
+++ b/docs/HowToFAQ/Errors-Compiler.md
@@ -74,7 +74,7 @@ For example, [`type T(00)` indicates that the type `T` is non-empty](../DafnyRef
 
 ## **Error: since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option** {#c_iterators_are_not_deterministic}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 iterator Gen(start: int) yields (x: int)
   yield ensures |xs| <= 10 && x == start + |xs| - 1
@@ -110,7 +110,7 @@ Furthermore, if the iterator is non-ghost, it cannot be compiled if it does not
 
 ## **Error: since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option** {#c_constructorless_class_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 class A { var j: int }
 ```
@@ -298,7 +298,7 @@ Body-less loops in ghost methods are similar to unchecked assumptions.
 
 ## **Error: nondeterministic assignment forbidden by the --enforce-determinism option** {#c_nondeterminism_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m() {
   var x: int;
@@ -319,7 +319,7 @@ There are a few different forms of this kind of assignment:
 
 ## **Error: assign-such-that statement forbidden by the --enforce-determinism option** {#c_assign_such_that_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m() {
   var x: int;
@@ -342,7 +342,7 @@ However, in this case the expression is too complex for Dafny's heuristics.
 
 ## **Error: nondeterministic if statement forbidden by the --enforce-determinism option** {#c_nondeterministic_if_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m() {
 var y: int;
@@ -379,7 +379,7 @@ whether there is a reasonable way to compute a value.)
 
 ## **Error: case-based if statement forbidden by the --enforce-determinism option** {#c_case_based_if_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m(k: int) {
   var i := k;
@@ -401,7 +401,7 @@ To enforce a deterministic order to the evaluation, use a chain of if-then-else
 
 ## **Error: nondeterministic loop forbidden by the --enforce-determinism option** {#c_non_deterministic_loop_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m(b: bool) decreases * {
   while * 
@@ -416,7 +416,7 @@ Hence this 'non-deterministic while' (`while *`) statement is not permitted with
 
 ## **Error: case-based loop forbidden by the --enforce-determinism option** {#c_case_based_loop_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m(k: int) {
   var i := k;
@@ -445,7 +445,7 @@ _The documentation of this problem is in progress._
 
 ## **Error: modify statement without a body forbidden by the --enforce-determinism option** {#c_bodyless_modify_statement_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 class A { constructor A(){}}
 
diff --git a/docs/HowToFAQ/Errors-Compiler.template b/docs/HowToFAQ/Errors-Compiler.template
index 93e5e82df8e..c6591bd1bce 100644
--- a/docs/HowToFAQ/Errors-Compiler.template
+++ b/docs/HowToFAQ/Errors-Compiler.template
@@ -44,7 +44,7 @@ type T
 
 ## **Error: since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option** {#c_iterators_are_not_deterministic}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 iterator Gen(start: int) yields (x: int)
   yield ensures |xs| <= 10 && x == start + |xs| - 1
@@ -72,7 +72,7 @@ iterator Gen(start: int) yields (x: int)
 
 ## **Error: since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option** {#c_constructorless_class_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 class A { var j: int }
 ```
@@ -208,7 +208,7 @@ ghost method m(i: int) {
 
 ## **Error: nondeterministic assignment forbidden by the --enforce-determinism option** {#c_nondeterminism_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m() {
   var x: int;
@@ -222,7 +222,7 @@ method m() {
 
 ## **Error: assign-such-that statement forbidden by the --enforce-determinism option** {#c_assign_such_that_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m() {
   var x: int;
@@ -239,7 +239,7 @@ method m() {
 
 ## **Error: nondeterministic if statement forbidden by the --enforce-determinism option** {#c_nondeterministic_if_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m() {
 var y: int;
@@ -266,7 +266,7 @@ method m(k: int) {
 
 ## **Error: case-based if statement forbidden by the --enforce-determinism option** {#c_case_based_if_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m(k: int) {
   var i := k;
@@ -282,7 +282,7 @@ method m(k: int) {
 
 ## **Error: nondeterministic loop forbidden by the --enforce-determinism option** {#c_non_deterministic_loop_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m(b: bool) decreases * {
   while * 
@@ -295,7 +295,7 @@ method m(b: bool) decreases * {
 
 ## **Error: case-based loop forbidden by the --enforce-determinism option** {#c_case_based_loop_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 method m(k: int) {
   var i := k;
@@ -317,7 +317,7 @@ method m(k: int) {
 
 ## **Error: modify statement without a body forbidden by the --enforce-determinism option** {#c_bodyless_modify_statement_forbidden}
 
-<!-- %check-run %options --enforce-determinism -->
+<!-- %check-resolve %options --enforce-determinism -->
 ```dafny
 class A { constructor A(){}}
 
diff --git a/docs/check-examples b/docs/check-examples
index 5096728128d..58264f735bc 100755
--- a/docs/check-examples
+++ b/docs/check-examples
@@ -423,7 +423,7 @@ do
                  FAIL=1
               fi
               if [ "$actualExit" != "$expectedExit" ]; then
-                echo EXPECTED EXIT CODE $expectedExit, got $actualec
+                echo EXPECTED EXIT CODE $expectedExit, got $actualExit
                 FAIL=1
               fi
             else 
diff --git a/docs/dev/news/5632.feat b/docs/dev/news/5632.feat
new file mode 100644
index 00000000000..344a92fc603
--- /dev/null
+++ b/docs/dev/news/5632.feat
@@ -0,0 +1 @@
+Enable the option `--enforce-determinism` for the commands `resolve` and `verify` 
\ No newline at end of file