1 files changed, 9 insertions, 0 deletions
diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl
index ec18dc3b..33e500d6 100644
--- a/Test/test0/WhereParsing.bpl
+++ b/Test/test0/WhereParsing.bpl
@@ -23,3 +23,12 @@ implementation P(xx: int where xx > 0)  // error: where not allowed in implement
     yy := b;
     return;
 }
+
+procedure {:myProcAttr} Attr(x: int, {:myParamAttr x, y} y: bool) returns (z: int, {:retAttr x} w: bool)
+{
+}
+
+procedure BadAttrs(x: int);
+implementation BadAttrs({:myParamAttr} x: int)  // error: attributes not allowed in implementation decl
+{
+}