diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:25:31 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:25:31 +0000 |
| commit | 16ed35436d4e4914a2dc601947fcc9c184b264a7 (patch) | |
| tree | 2e98c5c78f32d3a6c93106cd4ad1a079c24dd2eb /test/regress/regress0/uf/simple.04.cvc | |
| parent | 04fd25e4201130776015fd3179631a97f27da12a (diff) | |
one more simple test for uf
Diffstat (limited to 'test/regress/regress0/uf/simple.04.cvc')
| -rw-r--r-- | test/regress/regress0/uf/simple.04.cvc | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc new file mode 100644 index 000000000..58bb6fef1 --- /dev/null +++ b/test/regress/regress0/uf/simple.04.cvc @@ -0,0 +1,11 @@ +% EXPECT: INVALID +A: TYPE; +B: TYPE; +x, y: A; +a, b: A; + +f: A -> B; + +ASSERT (x = a OR x = b) AND (y = b OR y = a); +QUERY (f(x) = f(y)); + |