1 files changed, 11 insertions, 1 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 75a42200..b3107bcb 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -190,7 +190,7 @@ class AllocatedTests {
   {
     var n := new Node;
     var t := S + {n};
-    
+
     if (*) {
       assert !fresh(n);  // error: n was not allocated in the initial state
     } else {
@@ -498,6 +498,16 @@ class AttributeTests {
   }
 }
 
+// ----------------------- test attributes on variable declarations --------
+
+static method TestAttributesVarDecls()
+{
+  var {:foo} foo;
+  var {:bar} bar := 0;
+  var {:foo} {:bar} foobar := {};
+  var {:baz} baz, {:foobaz} foobaz := true, false;
+}
+
 // ----------------------- Pretty printing of !(!expr) --------
 
 static method TestNotNot()