diff options
Diffstat (limited to 'Test/inline/test7.bpl')
-rw-r--r-- | Test/inline/test7.bpl | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/Test/inline/test7.bpl b/Test/inline/test7.bpl deleted file mode 100644 index b5c6a4c6..00000000 --- a/Test/inline/test7.bpl +++ /dev/null @@ -1,15 +0,0 @@ -var g: int;
-
-procedure main()
-modifies g;
-{
- g := 0;
- call foo();
- assert g == 1;
-}
-
-procedure foo()
-modifies g;
-{
- g := g + 1;
-}
\ No newline at end of file |