Initial set of files.

1 files changed, 15 insertions, 0 deletions

diff --git a/Test/test0/Triggers0.bpl b/Test/test0/Triggers0.bpl
new file mode 100644
index 00000000..6750d77d
--- /dev/null
+++ b/Test/test0/Triggers0.bpl
@@ -0,0 +1,15 @@
+// Trigger errors

+

+function f(int, int) returns (int);

+function P(int, int) returns (bool);

+

+// -------------- tests specific to pattern exclusions

+

+axiom (forall x: int ::

+       {:nopats f(x,10) }

+       { :   nopats   f(x,10) }

+       f(x,10) == 3);

+

+axiom (forall x: int ::

+       {:nopats f(x,10), f(x,x) }  // error: a pattern exclusion can only mention one expression

+       f(x,10) == 3);