added assert

shazqadeer · shazqadeer · commit 6af7d1671f6e · 2025-11-25T21:01:00.000-08:00
diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs
@@ -1,4 +1,5 @@
 ﻿using System.Collections.Generic;
+using System.Diagnostics;
 using System.Linq;
 
 namespace Microsoft.Boogie
@@ -699,6 +700,7 @@ public override Variable VisitVariable(Variable node)
     
     public static LinearKind FindLinearKind(Variable v)
     {
+      Debug.Assert(v is GlobalVariable || v is Formal);
       if (QKeyValue.FindAttribute(v.Attributes, x => x.Key == CivlAttributes.LINEAR) != null)
       {
         return LinearKind.LINEAR;

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,5 @@`
`1`	`1`	`using System.Collections.Generic;`
	`2`	`+using System.Diagnostics;`
`2`	`3`	`using System.Linq;`
`3`	`4`
`4`	`5`	`namespace Microsoft.Boogie`
`@@ -699,6 +700,7 @@ public override Variable VisitVariable(Variable node)`
`699`	`700`
`700`	`701`	`public static LinearKind FindLinearKind(Variable v)`
`701`	`702`	`{`
	`703`	`+ Debug.Assert(v is GlobalVariable \|\| v is Formal);`
`702`	`704`	`if (QKeyValue.FindAttribute(v.Attributes, x => x.Key == CivlAttributes.LINEAR) != null)`
`703`	`705`	`{`
`704`	`706`	`return LinearKind.LINEAR;`