third commit

Author: shazqadeer

Source/Concurrency/YieldingProcDuplicator.cs

@@ -181,13 +181,14 @@ public override Block VisitBlock(Block node)
     public override Cmd VisitAssertCmd(AssertCmd node)
     {
       var assertCmd = (AssertCmd)base.VisitAssertCmd(node);
-      if (doRefinementCheck && node.Layers.Contains(layerNum))
-      {
-        return new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes);
-      }
       if (!node.Layers.Contains(layerNum))
       {
         assertCmd.Expr = Expr.True;
+        return assertCmd;
+      }
+      if (!doRefinementCheck)
+      {
+        return new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes);
       }
       return assertCmd;
     }
@@ -245,12 +246,17 @@ private void ProcessCallCmd(CallCmd newCall)
           {
             var pureAction = civlTypeChecker.Action(actionDecl);
             newCall.Proc = pureAction.Impl.Proc;
-            InjectGate(pureAction, newCall);
+            InjectGate(pureAction, newCall, !doRefinementCheck);
             newCmdSeq.Add(newCall);
           }
           else if (CivlPrimitives.IsPrimitive(newCall.Proc))
           {
-            newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall));
+            var cmds = linearRewriter.RewriteCallCmd(newCall).Select(cmd =>
+              cmd is AssertCmd assertCmd && !doRefinementCheck
+              ? new AssumeCmd(assertCmd.tok, assertCmd.Expr, assertCmd.Attributes)
+              : cmd
+            );
+            newCmdSeq.AddRange(cmds);
           }
           else
           {
@@ -464,7 +470,7 @@ private void InjectPreconditions(Action action, CallCmd callCmd)
       newCmdSeq.AddRange(action.Preconditions(layerNum, subst));
     }
 
-    private void InjectGate(Action action, CallCmd callCmd, bool assume = false)
+    private void InjectGate(Action action, CallCmd callCmd, bool assume)
     {
       if (action.Gate.Count == 0)
       {

Test/civl/samples/bluetooth.bpl

@@ -91,6 +91,7 @@ modifies usersInDriver;
 yield procedure {:layer 1}
 Exit(i: int, {:layer 1} {:linear_out} l: Set Perm, {:layer 1} {:linear} r: Set Perm)
 refines AtomicExit;
+requires {:layer 1} l->val == MapOne(Left(i)) && r->val == MapOne(Right(i));
 preserves call Inv1();
 {
     call DeleteReference();