diff options
Diffstat (limited to 'test/regress/regress0/sets')
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sets/nonvar-univ.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/sets/pre-proc-univ.smt2 | 9 |
3 files changed, 23 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index c2e3546d9..9413dfba3 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -79,7 +79,9 @@ TESTS = \ complement.cvc \ complement2.cvc \ complement3.cvc \ - sharing-simp.smt2 + sharing-simp.smt2 \ + pre-proc-univ.smt2 \ + nonvar-univ.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2 new file mode 100644 index 000000000..c71c984a2 --- /dev/null +++ b/test/regress/regress0/sets/nonvar-univ.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun x () (Set Int)) +(declare-fun P ((Set Int)) Bool) + +(assert (P x)) +(assert (not (P (singleton 0)))) +(assert (member 1 x)) +(assert (not (member 0 (as univset (Set Int))))) + +(check-sat) diff --git a/test/regress/regress0/sets/pre-proc-univ.smt2 b/test/regress/regress0/sets/pre-proc-univ.smt2 new file mode 100644 index 000000000..1b4bf8b41 --- /dev/null +++ b/test/regress/regress0/sets/pre-proc-univ.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () (Set Int)) + +(assert (= x (union (singleton 0) (singleton 1)))) + +(assert (not (member 0 (as univset (Set Int))))) + +(check-sat) |