simplification

shazqadeer · shazqadeer · commit 312b39d5335f · 2026-01-20T23:01:16.000-08:00
diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs
@@ -282,8 +282,7 @@ cmd is AssertCmd assertCmd && makeAssume
           }
           else
           {
-            var dropRequires = layerNum == enclosingYieldingProc.Layer && doRefinementCheck;
-            DesugarPureCall(newCall, dropRequires);
+            DesugarPureCall(newCall);
           }
         }
         return;
@@ -548,9 +547,9 @@ private void DesugarAsyncCall(CallCmd newCall)
       newCmdSeq.Add(newCall);
     }
 
-    private void DesugarPureCall(CallCmd newCall, bool dropRequires)
+    private void DesugarPureCall(CallCmd newCall)
     {
-      if (dropRequires)
+      if (doRefinementCheck)
       {
         if (!noRequiresPureProcedures.TryGetValue(newCall.Proc.Name, out Procedure checker))
         {

Original file line number	Diff line number	Diff line change
`@@ -282,8 +282,7 @@ cmd is AssertCmd assertCmd && makeAssume`
`282`	`282`	`}`
`283`	`283`	`else`
`284`	`284`	`{`
`285`		`- var dropRequires = layerNum == enclosingYieldingProc.Layer && doRefinementCheck;`
`286`		`- DesugarPureCall(newCall, dropRequires);`
	`285`	`+ DesugarPureCall(newCall);`
`287`	`286`	`}`
`288`	`287`	`}`
`289`	`288`	`return;`
`@@ -548,9 +547,9 @@ private void DesugarAsyncCall(CallCmd newCall)`
`548`	`547`	`newCmdSeq.Add(newCall);`
`549`	`548`	`}`
`550`	`549`
`551`		`- private void DesugarPureCall(CallCmd newCall, bool dropRequires)`
	`550`	`+ private void DesugarPureCall(CallCmd newCall)`
`552`	`551`	`{`
`553`		`- if (dropRequires)`
	`552`	`+ if (doRefinementCheck)`
`554`	`553`	`{`
`555`	`554`	`if (!noRequiresPureProcedures.TryGetValue(newCall.Proc.Name, out Procedure checker))`
`556`	`555`	`{`