diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs
index 182c494db..995b04e01 100644
--- a/Source/Concurrency/YieldingProcDuplicator.cs
+++ b/Source/Concurrency/YieldingProcDuplicator.cs
@@ -297,15 +297,7 @@ private void ProcessCallCmd(CallCmd newCall)
           }
           else if (IsRefinementLayer)
           {
-            if (newCall.HasAttribute(CivlAttributes.SKIP))
-            {
-              var calleeRefinedAction = PrepareNewCall(newCall, yieldingProc);
-              InjectGate(calleeRefinedAction, newCall);
-            }
-            else
-            {
-              AddPendingAsync(newCall, yieldingProc);
-            }
+            AddPendingAsync(newCall, yieldingProc);
           }
         }
         else
diff --git a/Source/Core/AST/Commands/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs
index 48a6208d0..ea04875b1 100644
--- a/Source/Core/AST/Commands/CallCmd.cs
+++ b/Source/Core/AST/Commands/CallCmd.cs
@@ -301,7 +301,6 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
     if (Proc is YieldProcedureDecl calleeDecl)
     {
       var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
-      var isSkipped = this.HasAttribute(CivlAttributes.SKIP);
       if (calleeDecl.Layer > callerDecl.Layer)
       {
         tc.Error(this, "layer of callee must not be more than layer of caller");
@@ -320,12 +319,12 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
             else
             {
               CheckModifies(highestRefinedActionDecl.ModifiedVars);
+              if (callerDecl.HasMoverType && highestRefinedActionDecl.Creates.Any())
+              {
+                tc.Error(this, "caller must not be a mover procedure");
+              }
               if (!IsAsync)
               {
-                if (highestRefinedActionDecl.Creates.Any() && callerDecl.HasMoverType)
-                {
-                  tc.Error(this, "caller must not be a mover procedure");
-                }
                 // check there is no application of IS_RIGHT in the entire chain of refined actions
                 var calleeRefinedAction = calleeDecl.RefinedAction;
                 while (calleeRefinedAction != null)
@@ -363,16 +362,9 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
                   calleeRefinedAction = calleeActionDecl.RefinedAction;
                 }
               }
-              else if (isSkipped)
+              else if (callerDecl.HasMoverType)
               {
-                if (highestRefinedActionDecl.LayerRange.UpperLayer != callerDecl.Layer)
-                {
-                  tc.Error(this, $"upper layer of action {highestRefinedActionDecl.Name} must be same as layer of caller");
-                }
-                else if (!highestRefinedActionDecl.IsSkippable())
-                {
-                  tc.Error(this, $"action {highestRefinedActionDecl.Name} must be skippable");
-                }
+                tc.Error(this, "async call must be synchronized");
               }
             }
           }
diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
index 425d70be4..06d6835b7 100644
--- a/Source/Core/CivlAttributes.cs
+++ b/Source/Core/CivlAttributes.cs
@@ -86,7 +86,6 @@ public static class CivlAttributes
     public const string HIDE = "hide";
     public const string PENDING_ASYNC = "pending_async";
     public const string SYNC = "sync";
-    public const string SKIP = "skip";
     public const string IS_RIGHT = "IS_right";
     public const string IS_LEFT = "IS_left";
 
diff --git a/Test/civl/regression-tests/issue-1005.bpl b/Test/civl/regression-tests/issue-1005.bpl
new file mode 100644
index 000000000..7e7c03f61
--- /dev/null
+++ b/Test/civl/regression-tests/issue-1005.bpl
@@ -0,0 +1,15 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+left action {:layer 1, 100} voting_action ()
+{
+}
+
+yield procedure {:layer 0} voting_procedure ();
+refines voting_action;
+
+
+yield left procedure {:layer 100} voting_loop_yield_procedure()
+{
+    async call voting_procedure();
+}
diff --git a/Test/civl/regression-tests/issue-1005.bpl.expect b/Test/civl/regression-tests/issue-1005.bpl.expect
new file mode 100644
index 000000000..192505590
--- /dev/null
+++ b/Test/civl/regression-tests/issue-1005.bpl.expect
@@ -0,0 +1,2 @@
+issue-1005.bpl(14,10): Error: async call must be synchronized
+1 type checking errors detected in issue-1005.bpl
diff --git a/Test/civl/regression-tests/refinement3.bpl b/Test/civl/regression-tests/refinement3.bpl
deleted file mode 100644
index 3de8708c6..000000000
--- a/Test/civl/regression-tests/refinement3.bpl
+++ /dev/null
@@ -1,26 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-yield procedure {:layer 1} Good()
-{
-    async call {:skip} P_A();
-}
-
-atomic action {:layer 1} A()
-asserts true;
-{}
-
-yield procedure {:layer 0} P_A();
-refines A;
-
-yield procedure {:layer 1} Bad()
-{
-    async call {:skip} P_B();
-}
-
-atomic action {:layer 1} B()
-asserts false;
-{}
-
-yield procedure {:layer 0} P_B();
-refines B;
\ No newline at end of file
diff --git a/Test/civl/regression-tests/refinement3.bpl.expect b/Test/civl/regression-tests/refinement3.bpl.expect
deleted file mode 100644
index 3cee83cf8..000000000
--- a/Test/civl/regression-tests/refinement3.bpl.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-refinement3.bpl(22,1): Error: this gate of B could not be proved
-Execution trace:
-    refinement3.bpl(18,11): anon0
-
-Boogie program verifier finished with 3 verified, 1 error