diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/test1/StatementIds0.bpl | 15 | ||||
-rw-r--r-- | Test/test1/StatementIds0.bpl.expect | 4 |
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 |