diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index c109aacbb..b9e1e36db 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -2867,6 +2867,7 @@ public class ActionDecl : Procedure
     public List<CallCmd> YieldRequires;
     public List<AssertCmd> Asserts;
     public DatatypeTypeCtorDecl PendingAsyncCtorDecl;
+    public bool IsAnonymous;
 
     public Implementation Impl; // set when the implementation of this action is resolved
     public LayerRange LayerRange; // set during registration
@@ -2886,6 +2887,11 @@ public ActionDecl(IToken tok, string name, MoverType moverType,
       this.YieldRequires = yieldRequires;
       this.Asserts = asserts;
       this.PendingAsyncCtorDecl = pendingAsyncCtorDecl;
+      this.IsAnonymous = name == null;
+      if (IsAnonymous)
+      {
+        this.Name = $"AnonymousAction_{this.UniqueId}";
+      }
     }
 
     public override void Register(ResolutionContext rc)
@@ -2949,6 +2955,12 @@ public override void Resolve(ResolutionContext rc)
 
     public override void Typecheck(TypecheckingContext tc)
     {
+      if (IsAnonymous)
+      {
+        var modSetCollector = new ModSetCollector(tc.Options);
+        modSetCollector.DoModSetAnalysis(this.Impl);
+      }
+
       var oldProc = tc.Proc;
       tc.Proc = this;
       base.Typecheck(tc);
diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs
index 336781057..f7e0f0a4f 100644
--- a/Source/Core/Analysis/ModSetCollector.cs
+++ b/Source/Core/Analysis/ModSetCollector.cs
@@ -25,6 +25,17 @@ public ModSetCollector(CoreOptions options)
 
   private bool moreProcessingRequired;
 
+  public void DoModSetAnalysis(Implementation impl)
+  {
+    this.VisitImplementation(impl);
+    var proc = impl.Proc;
+    proc.Modifies = new List<IdentifierExpr>();
+    foreach (Variable v in modSets[proc])
+    {
+      proc.Modifies.Add(new IdentifierExpr(v.tok, v));
+    }
+  }
+
   public void DoModSetAnalysis(Program program)
   {
     Contract.Requires(program != null);
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index e020af43f..fe5b791c2 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -701,7 +701,7 @@ ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out
     ImplBody<out locals, out stmtList>
     (.
        impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
-                                      locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
+                                      locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone());
     .)
   )
   (.
@@ -742,25 +742,63 @@ SpecCreates<.List<ActionDeclRef> creates.>
   ";"
   .
 
-SpecRefinedAction<ref ActionDeclRef refinedAction>
+SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>
 =
   (. IToken m; QKeyValue kv = null; .) 
   "refines"
-  { Attribute<ref kv> } 
+  { Attribute<ref kv> }
   Ident<out m>
   (.
      if (refinedAction == null) {
-       refinedAction = new ActionDeclRef(m, m.val, kv);
+        refinedAction = new ActionDeclRef(m, m.val, kv);
      } else {
-       this.SemErr("a refines specification already exists");
+        this.SemErr("a refines specification already exists");
      }
   .)
   .
 
+SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs.>
+=
+  (. IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
+  "refines"
+  { Attribute<ref kv> }
+  (
+    MoverQualifier<ref moverType>
+    "action" (. tok = t; .)
+    { Attribute<ref akv> }
+    Ident<out unused>
+    ImplBody<out locals, out stmtList>
+    (.
+      if (refinedAction == null) {
+        var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+                                      false, new List<ActionDeclRef>(), null, null,
+                                      new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
+        Pgm.AddTopLevelDeclaration(actionDecl);
+        var impl = new Implementation(tok, actionDecl.Name, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+                                      locals, stmtList, akv == null ? null : (QKeyValue)akv.Clone());
+        Pgm.AddTopLevelDeclaration(impl);
+        refinedAction = new ActionDeclRef(tok, actionDecl.Name);
+      } else {
+        this.SemErr("a refines specification already exists");
+      }
+    .)
+  |
+    Ident<out tok>
+    (.
+     if (refinedAction == null) {
+        refinedAction = new ActionDeclRef(tok, tok.val, kv);
+     } else {
+        this.SemErr("a refines specification already exists");
+     }
+    .)
+    ";"
+  )
+  .
+
 SpecAction<.ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<Requires> requires, List<CallCmd> yieldRequires, List<AssertCmd> asserts.>
 =
   (
-    SpecRefinedAction<ref refinedAction>
+    SpecRefinedActionForAtomicAction<ref refinedAction>
     (. IToken m; .)
     ["using" Ident<out m> (. invariantAction = new ActionDeclRef(m, m.val); .)]
     ";"
@@ -803,8 +841,8 @@ YieldProcedureDecl<out YieldProcedureDecl ypDecl, out Implementation impl>
     ProcFormals<true, true, out ins>
       [ "returns" ProcFormals<false, true, out outs> ]
     ( ";"
-      { SpecYieldPrePost<ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
-    | { SpecYieldPrePost<ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
+      { SpecYieldPrePost<ref refinedAction, name, ins, outs, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
+    | { SpecYieldPrePost<ref refinedAction, name, ins, outs, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
       ImplBody<out locals, out stmtList>
       (.
          impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
@@ -855,11 +893,10 @@ SpecYieldPreserves<. List<CallCmd> yieldPreserves .>
   ";"
   .
 
-SpecYieldPrePost<. ref ActionDeclRef refinedAction, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods.>
+SpecYieldPrePost<. ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods.>
 =
   (  
-    SpecRefinedAction<ref refinedAction>
-    ";"
+    SpecRefinedActionForYieldProcedure<ref refinedAction, name, ins, outs>
   | SpecYieldRequires<pre, yieldRequires>
   | SpecYieldEnsures<post, yieldEnsures>
   | SpecYieldPreserves<yieldPreserves>
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 68966a376..86678cf34 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -628,11 +628,11 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 		if (la.kind == 10) {
 			Get();
 			while (StartOf(6)) {
-				SpecYieldPrePost(ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods);
+				SpecYieldPrePost(ref refinedAction, name, ins, outs, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods);
 			}
 		} else if (StartOf(7)) {
 			while (StartOf(6)) {
-				SpecYieldPrePost(ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods);
+				SpecYieldPrePost(ref refinedAction, name, ins, outs, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods);
 			}
 			ImplBody(out locals, out stmtList);
 			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
@@ -726,7 +726,7 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
 			}
 			ImplBody(out locals, out stmtList);
 			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
-			                              locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
+			                              locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone());
 			
 		} else SynErr(133);
 		if (isPure) {
@@ -1167,7 +1167,7 @@ void MoverQualifier(ref MoverType moverType) {
 
 	void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<Requires> requires, List<CallCmd> yieldRequires, List<AssertCmd> asserts) {
 		if (la.kind == 41) {
-			SpecRefinedAction(ref refinedAction);
+			SpecRefinedActionForAtomicAction(ref refinedAction);
 			IToken m; 
 			if (la.kind == 42) {
 				Get();
@@ -1203,7 +1203,7 @@ void SpecCreates(List<ActionDeclRef> creates) {
 		Expect(10);
 	}
 
-	void SpecRefinedAction(ref ActionDeclRef refinedAction) {
+	void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) {
 		IToken m; QKeyValue kv = null; 
 		Expect(41);
 		while (la.kind == 26) {
@@ -1211,13 +1211,53 @@ void SpecRefinedAction(ref ActionDeclRef refinedAction) {
 		}
 		Ident(out m);
 		if (refinedAction == null) {
-		 refinedAction = new ActionDeclRef(m, m.val, kv);
+		  refinedAction = new ActionDeclRef(m, m.val, kv);
 		} else {
-		 this.SemErr("a refines specification already exists");
+		  this.SemErr("a refines specification already exists");
 		}
 		
 	}
 
+	void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs) {
+		IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; 
+		Expect(41);
+		while (la.kind == 26) {
+			Attribute(ref kv);
+		}
+		if (StartOf(5)) {
+			MoverQualifier(ref moverType);
+			Expect(39);
+			tok = t; 
+			while (la.kind == 26) {
+				Attribute(ref akv);
+			}
+			Ident(out unused);
+			ImplBody(out locals, out stmtList);
+			if (refinedAction == null) {
+			 var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+			                               false, new List<ActionDeclRef>(), null, null,
+			                               new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
+			 Pgm.AddTopLevelDeclaration(actionDecl);
+			 var impl = new Implementation(tok, actionDecl.Name, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+			                               locals, stmtList, akv == null ? null : (QKeyValue)akv.Clone());
+			 Pgm.AddTopLevelDeclaration(impl);
+			 refinedAction = new ActionDeclRef(tok, actionDecl.Name);
+			} else {
+			 this.SemErr("a refines specification already exists");
+			}
+			
+		} else if (StartOf(14)) {
+			Ident(out tok);
+			if (refinedAction == null) {
+			  refinedAction = new ActionDeclRef(tok, tok.val, kv);
+			} else {
+			  this.SemErr("a refines specification already exists");
+			}
+			
+			Expect(10);
+		} else SynErr(140);
+	}
+
 	void SpecModifies(List<IdentifierExpr> mods) {
 		List<IToken> ms; 
 		Expect(54);
@@ -1241,7 +1281,7 @@ void SpecYieldRequires(List<Requires> pre, List<CallCmd> yieldRequires ) {
 		} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 			CallCmd(out cmd);
 			yieldRequires.Add((CallCmd)cmd); 
-		} else SynErr(140);
+		} else SynErr(141);
 		Expect(10);
 	}
 
@@ -1257,10 +1297,9 @@ void SpecAsserts(List<AssertCmd> asserts ) {
 		Expect(10);
 	}
 
-	void SpecYieldPrePost(ref ActionDeclRef refinedAction, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods) {
+	void SpecYieldPrePost(ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods) {
 		if (la.kind == 41) {
-			SpecRefinedAction(ref refinedAction);
-			Expect(10);
+			SpecRefinedActionForYieldProcedure(ref refinedAction, name, ins, outs);
 		} else if (la.kind == 49) {
 			SpecYieldRequires(pre, yieldRequires);
 		} else if (la.kind == 50) {
@@ -1269,7 +1308,7 @@ void SpecYieldPrePost(ref ActionDeclRef refinedAction, List<Requires> pre, List<
 			SpecYieldPreserves(yieldPreserves);
 		} else if (la.kind == 54) {
 			SpecModifies(mods);
-		} else SynErr(141);
+		} else SynErr(142);
 	}
 
 	void CallCmd(out Cmd c) {
@@ -1306,7 +1345,7 @@ void SpecYieldEnsures(List<Ensures> post, List<CallCmd> yieldEnsures ) {
 		} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 			CallCmd(out cmd);
 			yieldEnsures.Add((CallCmd)cmd); 
-		} else SynErr(142);
+		} else SynErr(143);
 		Expect(10);
 	}
 
@@ -1346,7 +1385,7 @@ void Spec(List<Requires> pre, List<IdentifierExpr> mods, List<Ensures> post) {
 			SpecPrePost(true, pre, post);
 		} else if (la.kind == 49 || la.kind == 50) {
 			SpecPrePost(false, pre, post);
-		} else SynErr(143);
+		} else SynErr(144);
 	}
 
 	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
@@ -1369,7 +1408,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			post.Add(new Ensures(tok, free, e, null, kv)); 
-		} else SynErr(144);
+		} else SynErr(145);
 	}
 
 	void StmtList(out StmtList/*!*/ stmtList) {
@@ -1463,7 +1502,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 				hideRevealId = new IdentifierExpr(t, t.val); 
 			} else if (la.kind == 60) {
 				Get();
-			} else SynErr(145);
+			} else SynErr(146);
 			c = hideRevealId == null ? new HideRevealCmd(t, mode) : new HideRevealCmd(hideRevealId, mode); 
 			Expect(10);
 		} else if (la.kind == 64) {
@@ -1513,7 +1552,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 		} else if (la.kind == 72) {
 			ParCallCmd(out cn);
 			c = cn; 
-		} else SynErr(146);
+		} else SynErr(147);
 	}
 
 	void StructuredCmd(out StructuredCmd/*!*/ ec) {
@@ -1529,7 +1568,7 @@ void StructuredCmd(out StructuredCmd/*!*/ ec) {
 		} else if (la.kind == 61) {
 			BreakCmd(out bcmd);
 			ec = bcmd; 
-		} else SynErr(147);
+		} else SynErr(148);
 	}
 
 	void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1553,7 +1592,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 				Attribute(ref kv);
 			}
 			tc = new ReturnCmd(t) { Attributes = kv }; 
-		} else SynErr(148);
+		} else SynErr(149);
 		Expect(10);
 	}
 
@@ -1578,7 +1617,7 @@ void IfCmd(out IfCmd/*!*/ ifcmd) {
 				Get();
 				StmtList(out els);
 				elseOption = els; 
-			} else SynErr(149);
+			} else SynErr(150);
 		}
 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 
 	}
@@ -1617,7 +1656,7 @@ void WhileCmd(out WhileCmd wcmd) {
 			} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 				CallCmd(out cmd);
 				yields.Add((CallCmd)cmd); 
-			} else SynErr(150);
+			} else SynErr(151);
 			Expect(10);
 		}
 		Expect(26);
@@ -1648,7 +1687,7 @@ void Guard(out Expr e) {
 		} else if (StartOf(19)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(151);
+		} else SynErr(152);
 		Expect(12);
 	}
 
@@ -1726,7 +1765,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			}
 			Expect(10);
 			c = new AssignCmd(x, lhss, rhss, kv); 
-		} else SynErr(152);
+		} else SynErr(153);
 	}
 
 	void ParCallCmd(out Cmd d) {
@@ -1826,7 +1865,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			}
 			Expect(12);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else SynErr(153);
+		} else SynErr(154);
 	}
 
 	void Expressions(out List<Expr>/*!*/ es) {
@@ -1871,7 +1910,7 @@ void EquivOp() {
 			Get();
 		} else if (la.kind == 75) {
 			Get();
-		} else SynErr(154);
+		} else SynErr(155);
 	}
 
 	void LogicalExpression(out Expr/*!*/ e0) {
@@ -1909,7 +1948,7 @@ void ImpliesOp() {
 			Get();
 		} else if (la.kind == 77) {
 			Get();
-		} else SynErr(155);
+		} else SynErr(156);
 	}
 
 	void ExpliesOp() {
@@ -1917,7 +1956,7 @@ void ExpliesOp() {
 			Get();
 		} else if (la.kind == 79) {
 			Get();
-		} else SynErr(156);
+		} else SynErr(157);
 	}
 
 	void RelationalExpression(out Expr/*!*/ e0) {
@@ -1935,7 +1974,7 @@ void AndOp() {
 			Get();
 		} else if (la.kind == 81) {
 			Get();
-		} else SynErr(157);
+		} else SynErr(158);
 	}
 
 	void OrOp() {
@@ -1943,7 +1982,7 @@ void OrOp() {
 			Get();
 		} else if (la.kind == 83) {
 			Get();
-		} else SynErr(158);
+		} else SynErr(159);
 	}
 
 	void BvTerm(out Expr/*!*/ e0) {
@@ -2005,7 +2044,7 @@ void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(159); break;
+		default: SynErr(160); break;
 		}
 	}
 
@@ -2037,7 +2076,7 @@ void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		} else if (la.kind == 93) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Sub; 
-		} else SynErr(160);
+		} else SynErr(161);
 	}
 
 	void Power(out Expr/*!*/ e0) {
@@ -2065,7 +2104,7 @@ void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		} else if (la.kind == 96) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.RealDiv; 
-		} else SynErr(161);
+		} else SynErr(162);
 	}
 
 	void IsConstructor(out Expr/*!*/ e0) {
@@ -2097,7 +2136,7 @@ void UnaryExpression(out Expr/*!*/ e) {
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 
 		} else if (StartOf(25)) {
 			CoercionExpression(out e);
-		} else SynErr(162);
+		} else SynErr(163);
 	}
 
 	void NegOp() {
@@ -2105,7 +2144,7 @@ void NegOp() {
 			Get();
 		} else if (la.kind == 100) {
 			Get();
-		} else SynErr(163);
+		} else SynErr(164);
 	}
 
 	void CoercionExpression(out Expr/*!*/ e) {
@@ -2129,7 +2168,7 @@ void CoercionExpression(out Expr/*!*/ e) {
 				 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
 				}
 				
-			} else SynErr(164);
+			} else SynErr(165);
 		}
 	}
 
@@ -2201,7 +2240,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 					Expression(out e1);
 					Expect(12);
 					e = new NAryExpr(x, new FieldUpdate(id, id.val), new List<Expr> { e, e1 }); 
-				} else SynErr(165);
+				} else SynErr(166);
 			}
 		}
 	}
@@ -2318,7 +2357,7 @@ void AtomExpression(out Expr/*!*/ e) {
 					e = new NAryExpr(x, new FunctionCall(id), es); 
 				} else if (la.kind == 12) {
 					e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); 
-				} else SynErr(166);
+				} else SynErr(167);
 				Expect(12);
 			}
 			break;
@@ -2378,7 +2417,7 @@ void AtomExpression(out Expr/*!*/ e) {
 				 e = new LambdaExpr(x, typeParams, ds, kv, e); 
 			} else if (la.kind == 9) {
 				LetExpr(out e);
-			} else SynErr(167);
+			} else SynErr(168);
 			Expect(12);
 			break;
 		}
@@ -2391,7 +2430,7 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new CodeExpr(locals, blocks); 
 			break;
 		}
-		default: SynErr(168); break;
+		default: SynErr(169); break;
 		}
 	}
 
@@ -2403,7 +2442,7 @@ void Dec(out BigDec n) {
 		} else if (la.kind == 6) {
 			Get();
 			s = t.val; 
-		} else SynErr(169);
+		} else SynErr(170);
 		try {
 		 n = BigDec.FromString(s);
 		} catch (FormatException) {
@@ -2447,7 +2486,7 @@ void Forall() {
 			Get();
 		} else if (la.kind == 118) {
 			Get();
-		} else SynErr(170);
+		} else SynErr(171);
 	}
 
 	void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -2465,7 +2504,7 @@ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out L
 			}
 		} else if (StartOf(12)) {
 			BoundVars(out ds);
-		} else SynErr(171);
+		} else SynErr(172);
 		QSep();
 		while (la.kind == 26) {
 			AttributeOrTrigger(ref kv, ref trig);
@@ -2478,7 +2517,7 @@ void Exists() {
 			Get();
 		} else if (la.kind == 120) {
 			Get();
-		} else SynErr(172);
+		} else SynErr(173);
 	}
 
 	void Lambda() {
@@ -2486,7 +2525,7 @@ void Lambda() {
 			Get();
 		} else if (la.kind == 122) {
 			Get();
-		} else SynErr(173);
+		} else SynErr(174);
 	}
 
 	void LetExpr(out Expr/*!*/ letexpr) {
@@ -2596,7 +2635,7 @@ void SpecBlock(out Block/*!*/ b) {
 			 Attributes = kv
 			}); 
 			
-		} else SynErr(174);
+		} else SynErr(175);
 		Expect(10);
 	}
 
@@ -2653,7 +2692,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			 trig.AddLast(new Trigger(tok, true, es, null));
 			}
 			
-		} else SynErr(175);
+		} else SynErr(176);
 		Expect(27);
 	}
 
@@ -2668,7 +2707,7 @@ void AttributeParameter(out object/*!*/ o) {
 		} else if (StartOf(19)) {
 			Expression(out e);
 			o = e; 
-		} else SynErr(176);
+		} else SynErr(177);
 	}
 
 	void QSep() {
@@ -2676,7 +2715,7 @@ void QSep() {
 			Get();
 		} else if (la.kind == 124) {
 			Get();
-		} else SynErr(177);
+		} else SynErr(178);
 	}
 
 	void LetVar(out Variable/*!*/ v) {
@@ -2896,44 +2935,45 @@ string GetSyntaxErrorString(int n) {
 			case 137: s = "invalid TypeArgs"; break;
 			case 138: s = "invalid MoverQualifier"; break;
 			case 139: s = "invalid SpecAction"; break;
-			case 140: s = "invalid SpecYieldRequires"; break;
-			case 141: s = "invalid SpecYieldPrePost"; break;
-			case 142: s = "invalid SpecYieldEnsures"; break;
-			case 143: s = "invalid Spec"; break;
-			case 144: s = "invalid SpecPrePost"; break;
-			case 145: s = "invalid LabelOrCmd"; break;
+			case 140: s = "invalid SpecRefinedActionForYieldProcedure"; break;
+			case 141: s = "invalid SpecYieldRequires"; break;
+			case 142: s = "invalid SpecYieldPrePost"; break;
+			case 143: s = "invalid SpecYieldEnsures"; break;
+			case 144: s = "invalid Spec"; break;
+			case 145: s = "invalid SpecPrePost"; break;
 			case 146: s = "invalid LabelOrCmd"; break;
-			case 147: s = "invalid StructuredCmd"; break;
-			case 148: s = "invalid TransferCmd"; break;
-			case 149: s = "invalid IfCmd"; break;
-			case 150: s = "invalid WhileCmd"; break;
-			case 151: s = "invalid Guard"; break;
-			case 152: s = "invalid LabelOrAssign"; break;
-			case 153: s = "invalid CallParams"; break;
-			case 154: s = "invalid EquivOp"; break;
-			case 155: s = "invalid ImpliesOp"; break;
-			case 156: s = "invalid ExpliesOp"; break;
-			case 157: s = "invalid AndOp"; break;
-			case 158: s = "invalid OrOp"; break;
-			case 159: s = "invalid RelOp"; break;
-			case 160: s = "invalid AddOp"; break;
-			case 161: s = "invalid MulOp"; break;
-			case 162: s = "invalid UnaryExpression"; break;
-			case 163: s = "invalid NegOp"; break;
-			case 164: s = "invalid CoercionExpression"; break;
-			case 165: s = "invalid ArrayExpression"; break;
-			case 166: s = "invalid AtomExpression"; break;
+			case 147: s = "invalid LabelOrCmd"; break;
+			case 148: s = "invalid StructuredCmd"; break;
+			case 149: s = "invalid TransferCmd"; break;
+			case 150: s = "invalid IfCmd"; break;
+			case 151: s = "invalid WhileCmd"; break;
+			case 152: s = "invalid Guard"; break;
+			case 153: s = "invalid LabelOrAssign"; break;
+			case 154: s = "invalid CallParams"; break;
+			case 155: s = "invalid EquivOp"; break;
+			case 156: s = "invalid ImpliesOp"; break;
+			case 157: s = "invalid ExpliesOp"; break;
+			case 158: s = "invalid AndOp"; break;
+			case 159: s = "invalid OrOp"; break;
+			case 160: s = "invalid RelOp"; break;
+			case 161: s = "invalid AddOp"; break;
+			case 162: s = "invalid MulOp"; break;
+			case 163: s = "invalid UnaryExpression"; break;
+			case 164: s = "invalid NegOp"; break;
+			case 165: s = "invalid CoercionExpression"; break;
+			case 166: s = "invalid ArrayExpression"; break;
 			case 167: s = "invalid AtomExpression"; break;
 			case 168: s = "invalid AtomExpression"; break;
-			case 169: s = "invalid Dec"; break;
-			case 170: s = "invalid Forall"; break;
-			case 171: s = "invalid QuantifierBody"; break;
-			case 172: s = "invalid Exists"; break;
-			case 173: s = "invalid Lambda"; break;
-			case 174: s = "invalid SpecBlock"; break;
-			case 175: s = "invalid AttributeOrTrigger"; break;
-			case 176: s = "invalid AttributeParameter"; break;
-			case 177: s = "invalid QSep"; break;
+			case 169: s = "invalid AtomExpression"; break;
+			case 170: s = "invalid Dec"; break;
+			case 171: s = "invalid Forall"; break;
+			case 172: s = "invalid QuantifierBody"; break;
+			case 173: s = "invalid Exists"; break;
+			case 174: s = "invalid Lambda"; break;
+			case 175: s = "invalid SpecBlock"; break;
+			case 176: s = "invalid AttributeOrTrigger"; break;
+			case 177: s = "invalid AttributeParameter"; break;
+			case 178: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Test/civl/large-samples/shared-vector.bpl b/Test/civl/large-samples/shared-vector.bpl
index 1c9e2cb6b..08e859471 100644
--- a/Test/civl/large-samples/shared-vector.bpl
+++ b/Test/civl/large-samples/shared-vector.bpl
@@ -305,32 +305,26 @@ type Tid;
 type Mutex = Option Tid;
 var {:layer 0, 9} MutexPool: Map Loc Mutex;
 
-right action {:layer 1, 9} Atomic_Mutex_Alloc() returns ({:linear} one_loc_l: One Loc)
-modifies MutexPool;
+yield procedure {:layer 0} Mutex_Alloc() returns ({:linear} one_loc_l: One Loc);
+refines right action {:layer 1, 9} _
 {
   call one_loc_l := Loc_New();
   assume !Map_Contains(MutexPool, one_loc_l->val);
   MutexPool := Map_Update(MutexPool, one_loc_l->val, None());
 }
-yield procedure {:layer 0} Mutex_Alloc() returns ({:linear} one_loc_l: One Loc);
-refines Atomic_Mutex_Alloc;
 
-right action {:layer 1, 9} Atomic_Mutex_Acquire({:linear} tid: One Tid, loc_l: Loc)
-modifies MutexPool;
+yield procedure {:layer 0} Mutex_Acquire({:linear} tid: One Tid, loc_l: Loc);
+refines right action {:layer 1, 9} _
 {
   assert Map_Contains(MutexPool, loc_l);
   assume Map_At(MutexPool, loc_l) == None();
   MutexPool := Map_Update(MutexPool, loc_l, Some(tid->val));
 }
-yield procedure {:layer 0} Mutex_Acquire({:linear} tid: One Tid, loc_l: Loc);
-refines Atomic_Mutex_Acquire;
 
-left action {:layer 1, 9} Atomic_Mutex_Release({:linear} tid: One Tid, loc_l: Loc)
-modifies MutexPool;
+yield procedure {:layer 0} Mutex_Release({:linear} tid: One Tid, loc_l: Loc);
+refines left action {:layer 1, 9} _
 {
   assert Map_Contains(MutexPool, loc_l);
   assert Map_At(MutexPool, loc_l) == Some(tid->val);
   MutexPool := Map_Update(MutexPool, loc_l, None());
 }
-yield procedure {:layer 0} Mutex_Release({:linear} tid: One Tid, loc_l: Loc);
-refines Atomic_Mutex_Release;
diff --git a/Test/civl/regression-tests/anonymous-action.bpl b/Test/civl/regression-tests/anonymous-action.bpl
new file mode 100644
index 000000000..8e9aa05bd
--- /dev/null
+++ b/Test/civl/regression-tests/anonymous-action.bpl
@@ -0,0 +1,17 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0,2} x: int;
+
+yield procedure {:layer 0} A(i: int) returns (j: int);
+refines both action {:layer 1} _ {
+    x := x + 1;
+}
+
+yield procedure {:layer 1} B(i: int) returns (j: int)
+refines both action {:layer 2} _ {
+    x := x + 1;
+}
+{
+    call j := A(i);
+}
\ No newline at end of file
diff --git a/Test/civl/regression-tests/anonymous-action.bpl.expect b/Test/civl/regression-tests/anonymous-action.bpl.expect
new file mode 100644
index 000000000..a9949f2e7
--- /dev/null
+++ b/Test/civl/regression-tests/anonymous-action.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 3 verified, 0 errors