diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 64767c8933c..b11464f8071 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -478,12 +478,12 @@ public virtual Expression CloneExpr(Expression expr) {
     public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) {
       Contract.Requires(c != null);
       Contract.Requires(c.Arguments != null);
-      return new MatchCaseExpr(Tok(c.tok), c.Ctor, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body));
+      return new MatchCaseExpr(Tok(c.tok), c.Ctor, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body), CloneAttributes(c.Attributes));
     }
 
     public NestedMatchCaseExpr CloneNestedMatchCaseExpr(NestedMatchCaseExpr c) {
       Contract.Requires(c != null);
-      return new NestedMatchCaseExpr(Tok(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body));
+      return new NestedMatchCaseExpr(Tok(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body), CloneAttributes(c.Attributes));
     }
 
     public virtual Expression CloneApplySuffix(ApplySuffix e) {
@@ -902,7 +902,7 @@ public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, strin
         if (def == null) {
           continue;
         }
-        
+
         if (!declmap.ContainsKey(def)) {
           declmap.Add(def, new List<AliasModuleDecl>());
           sigmap.Add(def, new ModuleSignature());
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 5ea6138e4dd..313dbc681ea 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -4113,11 +4113,13 @@ CaseExpression<out NestedMatchCaseExpr c, bool allowLemma, bool allowLambda, boo
 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x;
      ExtendedPattern/*!*/ pat = null;
      Expression/*!*/ body;
+     Attributes attrs = null;
   .)
   "case"                      (. x = t; .)
+  { Attribute<ref attrs> }
   ExtendedPattern<out pat>             (. .)
   "=>"
-  Expression<out body, allowLemma, allowLambda, allowBitwiseOps>    (. c = new NestedMatchCaseExpr(x, pat, body); .)
+  Expression<out body, allowLemma, allowLambda, allowBitwiseOps>    (. c = new NestedMatchCaseExpr(x, pat, body, attrs); .)
 .
 
 /*------------------------------------------------------------------------*/
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 8cfc6ec69a9..0d2c75046e3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -9558,7 +9558,7 @@ public static MatchCaseExpr CreateMatchCase(MatchCaseExpr old_case, Expression n
       var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);
       new_body = VarSubstituter(old_case.Arguments.ConvertAll<NonglobalVariable>(x=>(NonglobalVariable)x), newVars, new_body);
 
-      var new_case = new MatchCaseExpr(old_case.tok, old_case.Ctor, newVars, new_body);
+      var new_case = new MatchCaseExpr(old_case.tok, old_case.Ctor, newVars, new_body, old_case.Attributes);
 
       new_case.Ctor = old_case.Ctor; // resolve here
       return new_case;
@@ -12132,18 +12132,20 @@ public MatchCase(IToken tok, DatatypeCtor ctor, [Captured] List<BoundVar> argume
   public class MatchCaseExpr : MatchCase
   {
     private Expression body;
+    public Attributes Attributes;
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(body != null);
     }
 
-    public MatchCaseExpr(IToken tok, DatatypeCtor ctor, [Captured] List<BoundVar> arguments, Expression body)
+    public MatchCaseExpr(IToken tok, DatatypeCtor ctor, [Captured] List<BoundVar> arguments, Expression body, Attributes attrs = null)
       : base(tok, ctor, arguments) {
       Contract.Requires(tok != null);
       Contract.Requires(ctor != null);
       Contract.Requires(cce.NonNullElements(arguments));
       Contract.Requires(body != null);
       this.body = body;
+      this.Attributes = attrs;
     }
 
     public Expression Body {
@@ -12428,10 +12430,12 @@ public NestedMatchCase(IToken tok, ExtendedPattern pat) {
   public class NestedMatchCaseExpr : NestedMatchCase
   {
     public readonly Expression Body;
+    public Attributes Attributes;
 
-    public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body): base(tok, pat) {
+    public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs): base(tok, pat) {
       Contract.Requires(body != null);
       this.Body = body;
+      this.Attributes = attrs;
     }
   }
 
@@ -12496,13 +12500,15 @@ public class NestedMatchExpr : ConcreteSyntaxExpression
     public readonly Expression Source;
     public readonly List<NestedMatchCaseExpr> Cases;
     public readonly bool UsesOptionalBraces;
+    public Attributes Attributes;
 
-    public NestedMatchExpr(IToken tok, Expression source, [Captured] List<NestedMatchCaseExpr> cases, bool usesOptionalBraces): base(tok) {
+    public NestedMatchExpr(IToken tok, Expression source, [Captured] List<NestedMatchCaseExpr> cases, bool usesOptionalBraces, Attributes attrs = null): base(tok) {
       Contract.Requires(source != null);
       Contract.Requires(cce.NonNullElements(cases));
       this.Source = source;
       this.Cases = cases;
       this.UsesOptionalBraces = usesOptionalBraces;
+      this.Attributes = attrs;
     }
   }
 
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7febeabfe95..3e37adb0e20 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1892,7 +1892,9 @@ public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, boo
           foreach (var mc in e.Cases) {
             bool isLastCase = i == e.Cases.Count - 1;
             Indent(ind);
-            wr.Write("case ");
+            wr.Write("case");
+            PrintAttributes(mc.Attributes);
+            wr.Write(" ");
             PrintExtendedPattern(mc.Pat);
             wr.WriteLine(" =>");
             PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
@@ -1919,7 +1921,10 @@ public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, boo
           foreach (var mc in e.Cases) {
             bool isLastCase = i == e.Cases.Count - 1;
             Indent(ind);
-            wr.Write("case {0}", mc.Ctor.Name);
+            wr.Write("case");
+            PrintAttributes(mc.Attributes);
+            wr.Write(" ");
+            wr.Write(mc.Ctor.Name);
             PrintMatchCaseArgument(mc);
             wr.WriteLine(" =>");
             PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1bf89ccf307..827705b3328 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -13,6 +13,7 @@
 using System.Diagnostics.Contracts;
 using Microsoft.BaseTypes;
 using Microsoft.Boogie;
+using Microsoft.CodeAnalysis.CSharp.Syntax;
 
 namespace Microsoft.Dafny
 {
@@ -11580,9 +11581,11 @@ public SyntaxContainer(IToken tok) {
     private class CExpr : SyntaxContainer
     {
       public readonly Expression Body;
+      public Attributes Attributes;
 
-      public CExpr(IToken tok, Expression body) : base(tok) {
+      public CExpr(IToken tok, Expression body, Attributes attrs = null) : base(tok) {
         this.Body = body;
+        this.Attributes = attrs;
       }
     }
 
@@ -11652,14 +11655,17 @@ public override string ToString() {
     private class RBranchExpr : RBranch {
 
       public Expression Body;
+      public Attributes Attributes;
 
-      public RBranchExpr(IToken tok, int branchid, List<ExtendedPattern> patterns,  Expression body) : base(tok, branchid, patterns) {
+      public RBranchExpr(IToken tok, int branchid, List<ExtendedPattern> patterns,  Expression body, Attributes attrs = null) : base(tok, branchid, patterns) {
         this.Body = body;
+        this.Attributes = attrs;
       }
 
-      public RBranchExpr(int branchid, NestedMatchCaseExpr x) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
+      public RBranchExpr(int branchid, NestedMatchCaseExpr x, Attributes attrs = null) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
         this.Body = x.Body;
         this.Patterns.Add(x.Pat);
+        this.Attributes = attrs;
       }
 
       public override string ToString() {
@@ -11675,7 +11681,7 @@ private static RBranchStmt CloneRBranchStmt(RBranchStmt branch) {
 
     private static RBranchExpr CloneRBranchExpr(RBranchExpr branch) {
       Cloner cloner = new Cloner();
-      return new RBranchExpr(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), cloner.CloneExpr(branch.Body));
+      return new RBranchExpr(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), cloner.CloneExpr(branch.Body), cloner.CloneAttributes((branch.Attributes)));
     }
 
     private static RBranch CloneRBranch(RBranch branch) {
@@ -11699,7 +11705,7 @@ private SyntaxContainer PackBody(IToken tok, RBranch branch) {
       if (branch is RBranchStmt br) {
         return new CStmt(tok, new BlockStmt(tok, tok, br.Body), br.Attributes);
       } else if (branch is RBranchExpr) {
-        return new CExpr(tok, ((RBranchExpr)branch).Body);
+        return new CExpr(tok, ((RBranchExpr)branch).Body, ((RBranchExpr)branch).Attributes);
       } else {
         Contract.Assert(false); throw new cce.UnreachableException(); // RBranch has only two implementations
       }
@@ -11817,7 +11823,8 @@ private MatchCase MakeMatchCaseFromContainer(IToken tok, KeyValuePair<string, Da
         newMatchCase = new MatchCaseStmt(tok, ctor.Value,  freshPatBV, insideBranch, c.Attributes);
       } else {
         var insideBranch = ((CExpr)insideContainer).Body;
-        newMatchCase = new MatchCaseExpr(tok, ctor.Value,  freshPatBV, insideBranch);
+        var attrs = ((CExpr)insideContainer).Attributes;
+        newMatchCase = new MatchCaseExpr(tok, ctor.Value,  freshPatBV, insideBranch, attrs);
       }
       newMatchCase.Ctor = ctor.Value;
       return newMatchCase;
@@ -12036,7 +12043,7 @@ private SyntaxContainer CompileRBranchConstructor(MatchTempInfo mti, MatchingCon
           c.Attributes = new Attributes("split", args, c.Attributes);
         }
         var newMatchStmt = new MatchStmt(mti.Tok, mti.EndTok, currMatchee, newMatchCaseStmts, true, mti.Attributes, context);
-        return new CStmt(null, newMatchStmt); //Wokring HERE
+        return new CStmt(null, newMatchStmt);
       } else {
         var newMatchExpr = new MatchExpr(mti.Tok, currMatchee, newMatchCases.ConvertAll(x => (MatchCaseExpr)x), true, context);
         return new CExpr(null, newMatchExpr);
@@ -12164,7 +12171,7 @@ private void CompileNestedMatchExpr(NestedMatchExpr e, ResolveOpts opts) {
       List<RBranch> branches = new List<RBranch>();
       for (int id = 0; id < e.Cases.Count(); id++) {
         var branch = e.Cases.ElementAt(id);
-        branches.Add(new RBranchExpr(id, branch));
+        branches.Add(new RBranchExpr(id, branch, branch.Attributes));
         mti.BranchTok[id] = branch.Tok;
       }
 
@@ -12410,6 +12417,7 @@ private void CheckLinearNestedMatchCase(Type type, NestedMatchCase mc, ResolveOp
     private void CheckLinearNestedMatchExpr(Type dtd, NestedMatchExpr me, ResolveOpts opts) {
       foreach(NestedMatchCaseExpr mc in me.Cases) {
         scope.PushMarker();
+        ResolveAttributes(mc.Attributes, null, opts);
         CheckLinearNestedMatchCase(dtd, mc, opts);
         scope.PopMarker();
       }
diff --git a/Source/Dafny/Verifier/Substituter.cs b/Source/Dafny/Verifier/Substituter.cs
index 18a33798e88..5cfdb818ec1 100644
--- a/Source/Dafny/Verifier/Substituter.cs
+++ b/Source/Dafny/Verifier/Substituter.cs
@@ -256,7 +256,7 @@ public virtual Expression Substitute(Expression expr) {
           if (newBoundVars != mc.Arguments || body != mc.Body) {
             anythingChanged = true;
           }
-          var newCaseExpr = new MatchCaseExpr(mc.tok, mc.Ctor, newBoundVars, body);
+          var newCaseExpr = new MatchCaseExpr(mc.tok, mc.Ctor, newBoundVars, body, mc.Attributes);
           newCaseExpr.Ctor = mc.Ctor;  // resolve here
           cases.Add(newCaseExpr);
         }
diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy
index 0bd1dac5f9c..ac015c04d21 100644
--- a/Test/dafny0/AttributeChecks.dfy
+++ b/Test/dafny0/AttributeChecks.dfy
@@ -53,6 +53,15 @@ method Match(xs: List<int>) returns (r: int)
   }
 }
 
+function method CaseExpr(r: List<int>): List<int>
+{
+  match r {
+    case Nil => Nil
+    case {:ignore 3 + true} Cons(h, Nil) => Nil // error:  3 + true is ill-typed
+    case {:ignore false} Cons(h, t) => CaseExpr(t)
+  }
+}
+
 method Calc(x: int, y: int)
 {
   calc {:split 1} {:split 1 + false} { // error:  1 + false is ill-typed
diff --git a/Test/dafny0/AttributeChecks.dfy.expect b/Test/dafny0/AttributeChecks.dfy.expect
index c2b5584fea8..295a7fb6afe 100644
--- a/Test/dafny0/AttributeChecks.dfy.expect
+++ b/Test/dafny0/AttributeChecks.dfy.expect
@@ -66,6 +66,18 @@ method Match(xs: List<int>) returns (r: int)
   }
 }
 
+function method CaseExpr(r: List<int>): List<int>
+{
+  match r {
+    case Nil =>
+      Nil
+    case {:ignore 3 + true} Cons(h, Nil) =>
+      Nil
+    case {:ignore false} Cons(h, t) =>
+      CaseExpr(t)
+  }
+}
+
 method Calc(x: int, y: int)
 {
   calc {:split 1} {:split 1 + false} {
@@ -104,12 +116,12 @@ method For(lo: int, hi: int) returns (k: int)
   }
   return 2;
 }
-AttributeChecks.dfy(94,7): Error: unresolved identifier: k
-AttributeChecks.dfy(93,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-AttributeChecks.dfy(93,28): Error: type of right argument to + (int) must agree with the result type (bool)
-AttributeChecks.dfy(97,25): Error: unresolved identifier: k
-AttributeChecks.dfy(96,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-AttributeChecks.dfy(96,28): Error: type of right argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(103,7): Error: unresolved identifier: k
+AttributeChecks.dfy(102,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+AttributeChecks.dfy(102,28): Error: type of right argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(106,25): Error: unresolved identifier: k
+AttributeChecks.dfy(105,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+AttributeChecks.dfy(105,28): Error: type of right argument to + (int) must agree with the result type (bool)
 AttributeChecks.dfy(18,17): Error: type of left argument to + (int) must agree with the result type (bool)
 AttributeChecks.dfy(18,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
 AttributeChecks.dfy(28,35): Error: type of right argument to + (int) must agree with the result type (bool)
@@ -118,12 +130,14 @@ AttributeChecks.dfy(42,19): Error: type of left argument to + (int) must agree w
 AttributeChecks.dfy(42,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
 AttributeChecks.dfy(52,19): Error: type of left argument to + (int) must agree with the result type (bool)
 AttributeChecks.dfy(52,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-AttributeChecks.dfy(58,28): Error: type of left argument to + (int) must agree with the result type (bool)
-AttributeChecks.dfy(58,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-AttributeChecks.dfy(68,25): Error: type of left argument to + (int) must agree with the result type (bool)
-AttributeChecks.dfy(68,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-AttributeChecks.dfy(75,23): Error: type of right argument to + (int) must agree with the result type (bool)
-AttributeChecks.dfy(75,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-AttributeChecks.dfy(86,30): Error: type of right argument to + (int) must agree with the result type (bool)
-AttributeChecks.dfy(86,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
-22 resolution/type errors detected in AttributeChecks.dfy
+AttributeChecks.dfy(60,20): Error: type of left argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(60,20): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+AttributeChecks.dfy(67,28): Error: type of left argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(67,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+AttributeChecks.dfy(77,25): Error: type of left argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(77,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+AttributeChecks.dfy(84,23): Error: type of right argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(84,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+AttributeChecks.dfy(95,30): Error: type of right argument to + (int) must agree with the result type (bool)
+AttributeChecks.dfy(95,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+24 resolution/type errors detected in AttributeChecks.dfy