diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-24 17:01:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-24 17:01:38 -0500 |
| commit | 22916321f5c26fdc632df24f3c1fef45beaeb918 (patch) | |
| tree | a8a43b5aea9b8a4efbe5069eacb720e5506fc423 /test/regress/regress1/fmf | |
| parent | 25d3eea9614a0882a5c18c455e5a14d118a78dce (diff) | |
Improvements to sets + cardinality + quantifiers (#2200)
Diffstat (limited to 'test/regress/regress1/fmf')
| -rw-r--r-- | test/regress/regress1/fmf/radu-quant-set.smt2 | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/radu-quant-set.smt2 b/test/regress/regress1/fmf/radu-quant-set.smt2 new file mode 100644 index 000000000..09d5cc706 --- /dev/null +++ b/test/regress/regress1/fmf/radu-quant-set.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: unsat +(set-logic ALL_SUPPORTED) + +(declare-const A (Set Int)) +(declare-const B (Set Int)) + +(define-fun F () Bool + (exists ((i Int) (j Int)) (and (distinct i j) (member i A) (member j B))) +) + +(define-fun G () Bool + (and (>= (card (union A B)) 2) (>= (card A) 1) (>= (card B) 1)) +) + +(assert (and G (not F))) + +(check-sat) |