Add a test.

2 files changed, 15 insertions, 4 deletions

diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl
index 85b9cd36..abf26159 100644
--- a/Test/test1/StatementIds0.bpl
+++ b/Test/test1/StatementIds0.bpl
@@ -3,13 +3,22 @@
 
 procedure test0(n: int)
 {
-    assume {:id "s0"} 0 < n;
-    assert {:id "s0"} 0 < n;
+    assume {:id "s0"} true;
+    assert {:id "s0"} true;
 }
 
-procedure test1(n: int)
+procedure test1()
 {
     call {:id "s0"} P();
 }
 
+procedure test2(n: int)
+{
+    while (*)
+      invariant {:id "s0"} true;
+      invariant {:id "s0"} true;
+    {
+    }
+}
+
 procedure P();
diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect
index 944c3257..4783d912 100644
--- a/Test/test1/StatementIds0.bpl.expect
+++ b/Test/test1/StatementIds0.bpl.expect
@@ -1,3 +1,5 @@
 StatementIds0.bpl(7,4): Error: more than one statement with same id: s0
 StatementIds0.bpl(12,4): Error: more than one statement with same id: s0
-2 name resolution errors detected in StatementIds0.bpl
+StatementIds0.bpl(18,6): Error: more than one statement with same id: s0
+StatementIds0.bpl(19,6): Error: more than one statement with same id: s0
+4 name resolution errors detected in StatementIds0.bpl