diff options
Diffstat (limited to 'test/regress/regress1/fmf/ko-bound-set.cvc')
| -rw-r--r-- | test/regress/regress1/fmf/ko-bound-set.cvc | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/test/regress/regress1/fmf/ko-bound-set.cvc b/test/regress/regress1/fmf/ko-bound-set.cvc deleted file mode 100644 index 5306a1513..000000000 --- a/test/regress/regress1/fmf/ko-bound-set.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: not_entailed -OPTION "finite-model-find"; -OPTION "fmf-bound-int"; -OPTION "produce-models"; - -X, Y : SET OF INT; - -ASSERT FORALL(x : INT): x IS_IN X => x > 0; -QUERY ||X|| = 5 AND Y = X | {9} => ||Y|| <= 4; - |