first commit

Source/Concurrency/CivlCoreTypes.cs

@@ -190,7 +190,8 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh
             .Zip(Impl.InParams)
             .ToDictionary(x => x.Item1, x => (Expr)Expr.Ident(x.Item2)));
       Gate = ActionDecl.Requires.Select(
-        requires => new AssertCmd(requires.tok, Substituter.Apply(gateSubst, requires.Condition))).ToList();
+        requires => new AssertCmd(requires.tok, Substituter.Apply(gateSubst, requires.Condition),
+                                  CivlAttributes.ApplySubstitutionToPoolHints(gateSubst, requires.Attributes))).ToList();
     }
 
     private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Implementation impl)

Source/Concurrency/MoverCheck.cs

@@ -442,7 +442,7 @@ private void CreateCooperationChecker(Action action, MoverCheckContext moverChec
       List<Requires> requires =
         DisjointnessAndWellFormedRequires(impl.InParams.Where(v => LinearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_OUT),
           frame).ToList();
-      requires.AddRange(action.Gate.Select(assertCmd => new Requires(false, assertCmd.Expr)));
+      requires.AddRange(action.Gate.Select(assertCmd => new Requires(Token.NoToken, false, assertCmd.Expr, null, assertCmd.Attributes)));
       if (moverCheckContext != null)
       {
         checkerName = $"CooperationChecker_{action.Name}_{moverCheckContext.layer}";
@@ -454,9 +454,8 @@ private void CreateCooperationChecker(Action action, MoverCheckContext moverChec
         TransitionRelationComputation.Cooperation(civlTypeChecker, action, frame),
         $"Cooperation check for {action.Name} failed");
 
-      // call action after the cooperation check to exploit quantifier instantiation hints in the body
       AddChecker(checkerName, new List<Variable>(impl.InParams), new List<Variable>(impl.OutParams),
-        new List<Variable>(), requires, new List<Cmd> { cooperationCheck, ActionCallCmd(action, impl) });
+        new List<Variable>(), requires, new List<Cmd> { cooperationCheck });
     }
   }
 }

Source/Core/CivlAttributes.cs

@@ -177,6 +177,40 @@ public static bool IsCallMarked(CallCmd callCmd)
     {
       return callCmd.HasAttribute(MARK);
     }
+
+    public static QKeyValue ApplySubstitutionToPoolHints(Substitution incarnationSubst, QKeyValue attributes)
+    {
+      if (attributes == null)
+      {
+        return null;
+      }
+      attributes = (QKeyValue)new Duplicator().Visit(attributes);
+      var iter = attributes;
+      while (iter != null)
+      {
+        if (iter.Key == "add_to_pool" && iter.Params.Count > 1)
+        {
+          var label = iter.Params[0] as string;
+          if (label != null)
+          {
+            var newParams = new List<object> {label};
+            for (int i = 1; i < iter.Params.Count; i++)
+            {
+              var instance = iter.Params[i] as Expr;
+              if (instance != null)
+              {
+                instance = Substituter.Apply(incarnationSubst, instance);
+                newParams.Add(instance);
+              }
+            }
+            iter.ClearParams();
+            iter.AddParams(newParams);
+          }
+        }
+        iter = iter.Next;
+      }
+      return attributes;
+    }
   }
 
   public static class CivlPrimitives

Source/VCExpr/QuantifierInstantiationEngine.cs

@@ -78,41 +78,15 @@ private QuantifierInstantiationEngine(VCExpressionGenerator vcExprGen, Boogie2VC
       this.vcExprGen = vcExprGen;
       this.exprTranslator = exprTranslator;
     }
-    
+
     public static void SubstituteIncarnationInInstantiationSources(Cmd cmd, Substitution incarnationSubst)
     {
-      QKeyValue iter = null;
-      if (cmd is AssignCmd assignCmd)
-      {
-        iter = assignCmd.Attributes;
-      }
-      else if (cmd is PredicateCmd predicateCmd)
-      {
-        iter = predicateCmd.Attributes;
-      }
-      while (iter != null)
+      var attrCmd = cmd as ICarriesAttributes;
+      if (attrCmd == null)
       {
-        if (iter.Key == "add_to_pool" && iter.Params.Count > 1)
-        {
-          var label = iter.Params[0] as string;
-          if (label != null)
-          {
-            var newParams = new List<object> {label};
-            for (int i = 1; i < iter.Params.Count; i++)
-            {
-              var instance = iter.Params[i] as Expr;
-              if (instance != null)
-              {
-                instance = Substituter.Apply(incarnationSubst, instance);
-                newParams.Add(instance);
-              }
-            }
-            iter.ClearParams();
-            iter.AddParams(newParams);
-          }
-        }
-        iter = iter.Next;
+        return;
       }
+      attrCmd.Attributes = CivlAttributes.ApplySubstitutionToPoolHints(incarnationSubst, attrCmd.Attributes);
     }
 
     public VCExpr BindQuantifier(VCExprQuantifier node)

Source/VCGeneration/ConditionGeneration.cs

@@ -234,7 +234,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu
       {
         Contract.Assert(req != null);
         Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
-        AssumeCmd c = new AssumeCmd(req.tok, e);
+        AssumeCmd c = new AssumeCmd(req.tok, e, CivlAttributes.ApplySubstitutionToPoolHints(formalProcImplSubst, req.Attributes));
         // Copy any {:id ...} from the precondition to the assumption, so
         // we can track it while analyzing verification coverage.
         (c as ICarriesAttributes).CopyIdFrom(req.tok, req);

Test/civl/regression-tests/left-mover.bpl

@@ -27,7 +27,7 @@ left action {:layer 2} block ()
 { assume x >= 0; }
 
 pure action F (i: int) returns ({:pool "A"} j: int)
+requires {:add_to_pool "A", i+1} true;
 {
-  assume {:add_to_pool "A", i+1} true;
   assume j > i;
 }

Test/civl/regression-tests/left-mover.bpl.expect

@@ -12,4 +12,4 @@ left-mover.bpl(26,24): Error: Cooperation check for block failed
 Execution trace:
     (0,0): init
 
-Boogie program verifier finished with 2 verified, 3 errors
+Boogie program verifier finished with 3 verified, 3 errors