diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
index 49ee3003c..43f0a7922 100644
--- a/Source/Concurrency/CivlUtil.cs
+++ b/Source/Concurrency/CivlUtil.cs
@@ -133,7 +133,6 @@ public static int ResolveAndTypecheck(CoreOptions options, Absy absy, Resolution
       }
 
       var tc = new TypecheckingContext(null, options);
-      tc.CheckModifies = false; // to prevent access to tc.Proc which is null
       absy.Typecheck(tc);
       return tc.ErrorCount;
     }
diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
index c5a2c181b..266d93287 100644
--- a/Source/Concurrency/LinearRewriter.cs
+++ b/Source/Concurrency/LinearRewriter.cs
@@ -530,10 +530,7 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable<Absy> absys)
       return;
     }
     var tc = new TypecheckingContext(null, options);
-    var oldCheckModifies = tc.CheckModifies;
-    tc.CheckModifies = false;
     absys.ForEach(absy => absy.Typecheck(tc));
-    tc.CheckModifies = oldCheckModifies;
   }
 
   private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index ee240bde7..7783dde5c 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -751,13 +751,12 @@ public class TypecheckingContext : CheckingContext
     public LayerRange ExpectedLayerRange;
     public bool GlobalAccessOnlyInOld;
     public int InsideOld;
-    public bool CheckModifies;
+    public bool CheckModifies => Proc != null && (Proc.IsPure || (!Options?.DoModSetAnalysis ?? true));
 
     public TypecheckingContext(IErrorSink errorSink, CoreOptions options)
       : base(errorSink)
     {
       this.Options = options;
-      this.CheckModifies = !options?.DoModSetAnalysis ?? true;
     }
 
     public bool InFrame(Variable v)