diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/seu169+1.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/seu169+1.smt2 | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/seu169+1.smt2 b/test/regress/regress1/quantifiers/seu169+1.smt2 new file mode 100644 index 000000000..08fd6025b --- /dev/null +++ b/test/regress/regress1/quantifiers/seu169+1.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic UF) +(declare-sort $$unsorted 0) +(declare-fun in ($$unsorted $$unsorted) Bool) +(declare-fun powerset ($$unsorted) $$unsorted) +(declare-fun subset ($$unsorted $$unsorted) Bool) +(declare-fun empty ($$unsorted) Bool) +(declare-fun element ($$unsorted $$unsorted) Bool) +(declare-fun empty_set () $$unsorted) +(set-info :filename "SEU169+1") +(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (in B A))) )) +(assert (forall ((A $$unsorted) (B $$unsorted)) (= (= B (powerset A)) (forall ((C $$unsorted)) (= (in C B) (subset C A)) )) )) +(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) ))) +(assert (forall ((A $$unsorted) (B $$unsorted)) (= (subset A B) (forall ((C $$unsorted)) (or (not (in C A)) (in C B)) )) )) +(assert (forall ((A $$unsorted)) (not (forall ((B $$unsorted)) (not (element B A)) )) )) +(assert (forall ((A $$unsorted)) (not (empty (powerset A))) )) +(assert (empty empty_set)) +(assert (not (forall ((A $$unsorted) (B $$unsorted) (BOUND_VARIABLE_423 $$unsorted)) (or (not (element B (powerset A))) (not (in BOUND_VARIABLE_423 B)) (in BOUND_VARIABLE_423 A)) ))) +(assert (forall ((A $$unsorted)) (or (empty A) (not (forall ((B $$unsorted)) (or (not (element B (powerset A))) (empty B)) ))) )) +(assert (not (forall ((A $$unsorted)) (not (empty A)) ))) +(assert (not (forall ((A $$unsorted)) (empty A) ))) +(assert (forall ((A $$unsorted)) (subset A A) )) +(assert (forall ((A $$unsorted)) (or (not (empty A)) (= empty_set A)) )) +(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (empty B))) )) +(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= A B) (not (empty B))) )) +(assert true) +(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) ))) +(check-sat) |