1 files changed, 127 insertions, 0 deletions
diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl
new file mode 100644
index 00000000..02c63406
--- /dev/null
+++ b/Test/test0/Triggers1.bpl
@@ -0,0 +1,127 @@
+// Trigger errors
+
+function f(int, int) returns (int);
+function P(int, int) returns (bool);
+
+axiom (forall x: int ::
+       { f(x,10) && f(x,9) }   // error: && not allowed
+       f(x,10) == 3);
+
+axiom (forall x: int ::
+       { ((((f(x,10) || f(x,9))))) }   // error: || not allowed
+       f(x,10) == 3);
+
+axiom (forall x: int ::
+       { !f(x,10) }   // error: ! not allowed
+       f(x,10) == 3);
+
+axiom (forall x: int ::
+       { (!f(x,10)) }   // error: ! not allowed
+       f(x,10) == 3);
+
+axiom (forall x: int ::
+       { P(x,10) ==> P(20,x) }   // error: ==> not allowed
+       f(x,10) == 3);
+
+axiom (forall x: int ::
+       { P(x,10) <==> P(20,x) }   // error: <==> not allowed
+       f(x,10) == 3);
+
+
+axiom (forall x: int ::
+       { f(x,10) == 3 }   // error: == not allowed
+       f(x,10) == 3);
+
+axiom (forall x: int ::
+       { f(x,10) < 3 }   // error: < not allowed
+       f(x,10) == 3);
+
+
+axiom (forall x: int ::
+       { f(x,10) + f(x,x) != 3 }   // yes, != is allowed
+       f(x,10) == 3);
+
+axiom (forall b: bool ::
+       { (forall y: int :: b) }   // error: quantifiers not allowed
+       b);
+
+// -------------- tests of free variables
+
+const g: int;
+
+axiom (forall x: int ::
+       { false, 6 }             // error: does not mention "x"
+       x < x + 1);
+
+axiom (forall x: int ::
+       { false, x+1, 6 }        // allowed
+       x < x + 1);
+
+axiom (forall x: int, y: int ::
+       { x+1 }                  // error: does not mention "y"
+       { y+1 }                  // error: does not mention "x"
+       x < y + 1);
+
+axiom (forall x: int ::
+       { g+x != 65 }            // allowed
+       x < x + 1);
+
+axiom (forall x: int ::
+       { x }                    // "x" by itself is not a good trigger
+       x < x + 1);
+
+//axiom (forall x: any ::  // PR: removed for the time being
+//       { cast(x,int) }          // can't fool me, still not allowed
+//       x == x );
+
+// --- multiple triggers
+
+axiom (forall x: int, y: int, z: int ::
+       { x+y+z }                // good
+       { x+y, y+z }             // also good
+       { f(f(x,y),y) }          // error: does not mention z
+       x == x );
+
+// --- multi-triggers
+
+axiom (forall x: int, y: int, z: int ::
+       { f(x,x), f(y,y), f(z,z) }  // good
+       f(x,y) < f(y,z) );
+
+// --- pattern exclusion
+
+axiom (forall x: int, y: int ::
+       {:nopats x }                   // error: "x" by itself is not allowed here either
+       {:nopats g }                   // error: "g" by itself is not allowed here either
+       x < y);
+
+axiom (forall x: int, y: int ::
+       {:nopats f(g,g) }              // but it is okay not to mention the bound variables (in a pattern exclusion)
+       x < y);
+
+// --- merging of nested quantifiers
+
+axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK
+axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error
+axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // error
+
+// three levels
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // error
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(y,z) } f(y,y) > 0))); // error
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK
+
+// --- no free variables
+
+var h0: int;
+var h1: [ref,ref]int;
+
+axiom (forall o: ref, f: ref  :: h1[o,f] // error: cannot mention free variable "h1"
+                               < h0);    // error: cannot mention free variable "h0"
+
+const c0: int;
+const c1: [ref,ref]int;
+
+axiom (forall o: ref, f: ref :: c1[o,f] < c0);
+
+type ref;