Removed definite assignment change.

dafny-lang · Feb 10, 2025 · d928f2f · d928f2f
1 parent 384eae6
commit d928f2f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs
@@ -30,7 +30,7 @@ bool NeedsDefiniteAssignmentTracker(bool isGhost, Type type, bool isField) {
                  (options.DefiniteAssignmentLevel == 4 && isField && !options.ForbidNondeterminism)) {
         if (isGhost && type.IsNonempty) {
           return false;
-        } else if (!isGhost && type.HasCompilableValue && options.DefiniteAssignmentLevel == 1) {
+        } else if (!isGhost && type.HasCompilableValue) {
           return false;
         }
       }