diff options
Diffstat (limited to 'Test/test21/Keywords.bpl')
| -rw-r--r-- | Test/test21/Keywords.bpl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Test/test21/Keywords.bpl b/Test/test21/Keywords.bpl new file mode 100644 index 00000000..daf38b45 --- /dev/null +++ b/Test/test21/Keywords.bpl @@ -0,0 +1,9 @@ +
+
+function NOT(x:int) returns(int);
+
+axiom (forall x:int :: NOT(x) == 1 - x);
+
+procedure P() returns () {
+ assert NOT(5) == -4;
+}
\ No newline at end of file |