summaryrefslogtreecommitdiff
path: root/Test/test1/StatementIds0.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test1/StatementIds0.bpl')
-rw-r--r--Test/test1/StatementIds0.bpl15
1 files changed, 12 insertions, 3 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();