diff options
Diffstat (limited to 'test/regress/regress0/sets/union-1b-flip.smt2')
| -rw-r--r-- | test/regress/regress0/sets/union-1b-flip.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 new file mode 100644 index 000000000..86fed459b --- /dev/null +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --incremental --no-check-models +; EXPECT: unsat +; EXPECT: sat + +; x not in A U B => x not in A +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(assert (in x B)) +(push 1) +(assert (not (in x (union A B)))) +(check-sat) +(pop 1) +(check-sat) |