5 files changed, 27 insertions, 10 deletions
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index c8cb1844..8408bf83 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -72,6 +72,7 @@ namespace Microsoft.Boogie
                 HashSet<Variable> vars = new HashSet<Variable>();
                 foreach (Variable var in this.availableLinearVars[absy])
                 {
+                    if (var is GlobalVariable) continue;
                     string domainName = FindDomainName(var);
                     if (this.linearDomains.ContainsKey(domainName))
                     {
diff --git a/Test/linear/Answer b/Test/linear/Answer
index 9219497b..9fabc440 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -45,3 +45,10 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- f3.bpl --------------------
 
 Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- bug.bpl --------------------
+bug.bpl(13,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    bug.bpl(12,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/linear/bug.bpl b/Test/linear/bug.bpl
new file mode 100644
index 00000000..b7a6a238
--- /dev/null
+++ b/Test/linear/bug.bpl
@@ -0,0 +1,14 @@
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }
+
+var {:linear ""} g:int;
+
+procedure A()
+{
+}
+
+procedure B()
+{
+  call A();
+  assert false;
+}
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
index c8d3dc62..bd32d250 100644
--- a/Test/linear/runtest.bat
+++ b/Test/linear/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (typecheck.bpl) do (
   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
 )
 
-for %%f in (list.bpl allocator.bpl f1.bpl f2.bpl f3.bpl) do (
+for %%f in (list.bpl allocator.bpl f1.bpl f2.bpl f3.bpl bug.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 64144ae9..3ba0840d 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -7,13 +7,9 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
   x
 }
 
-
-var {:linear "Perm"} Permissions: [int]bool;
-
-procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);
-modifies Permissions;
+procedure Allocate_Perm({:linear "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool);
 requires Permissions == mapconstbool(true);
-ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);
+ensures xls == mapconstbool(true);
 
 procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)
 requires permVar_in[0] && g == 0;
@@ -32,13 +28,12 @@ requires permVar_in[0] && g == 0;
   assert g == 1;
 }
 
-procedure{:entrypoint} {:yields} Main()
-modifies g, Permissions;
+procedure{:entrypoint} {:yields} Main({:linear "Perm"} Permissions: [int]bool)
 requires Permissions == mapconstbool(true);
 {
   var {:linear "Perm"} permVar_out: [int]bool;
 
-  call permVar_out := Allocate_Perm();
+  call permVar_out := Allocate_Perm(Permissions);
 
   g := 0;
   async call PB(permVar_out);