blob: bbf37517ecb348b14e51f2800a50ad79743146f5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
// RUN: %boogie -noVerify %s > %t
// RUN: %diff %s.expect %t
// 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);
|