added test

Source/Concurrency/CivlCoreTypes.cs

@@ -68,6 +68,8 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
       DeclareTriggerFunctions();
     }
 
+    public IEnumerable<Variable> UsedGlobalVars => UsedGlobalVarsInGate.Union(UsedGlobalVarsInAction);
+
     public IToken tok => ActionDecl.tok;
 
     public string Name => ActionDecl.Name;

Source/Concurrency/InductiveSequentialization.cs

@@ -331,7 +331,7 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target
     private IEnumerable<Expr> InputDisjointnessExprs()
     {
       return civlTypeChecker.linearTypeChecker.DisjointnessExprForEachDomain(
-        invariantAction.Impl.InParams.Union(invariantAction.ModifiedGlobalVars)
+        invariantAction.Impl.InParams.Union(invariantAction.UsedGlobalVars)
         .Where(x => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(x))));
     }
 

Test/civl/regression-tests/rec-IS1.bpl

@@ -1,29 +1,30 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-async left action {:layer 1} main_f''()
+var {:linear} g: One int;
+
+async left action {:layer 1} main_f''({:linear_in} l: One int)
 refines final using Inv;
 creates main_f'';
 {
-    if(*){
-    }
-    else{
-      call create_async(main_f''());
-    }
+  if (*) {
+  } else{
+    call create_async(main_f''(l));
+  }
 }
 
-action {:layer 2} final()
+action {:layer 2} final({:linear_in} l: One int)
 {
-
+  // conclusion check succeeds due to disjointness assumption
 }
 
-action {:layer 1} Inv()
+action {:layer 1} Inv({:linear_in} l: One int)
 creates main_f'';
 {
-    if(*){
-    }
-    else{
-      call create_async(main_f''());
-      call set_choice(main_f''());
-    }
+  assert l != g;
+  if (*) {
+  } else {
+    call create_async(main_f''(l));
+    call set_choice(main_f''(l));
+  }
 }

Test/civl/regression-tests/rec-IS1.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 5 verified, 0 errors