diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-29 08:38:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-29 08:38:30 -0500 |
| commit | c59aefd26d391cb01f0e27b050e553afe49a69d8 (patch) | |
| tree | 5da0ac0bd5814ec93f3fde9ffed99046cd4d75c5 /test/regress/regress1 | |
| parent | 327fe83f2e0533d53902645364180bc51ff20dcc (diff) | |
Apply empty splits more aggressively in sets+cardinality (#2907)
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/sets/issue2904.smt2 | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 new file mode 100644 index 000000000..13ca789f6 --- /dev/null +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -0,0 +1,27 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+; conjecture set nonempty(~b & ~c)
+
+(declare-fun n () Int)
+(declare-fun f () Int)
+(declare-fun m () Int)
+
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun UNIVERALSET () (Set Int))
+(assert (subset b UNIVERALSET))
+(assert (subset c UNIVERALSET))
+
+(assert (> n 0))
+(assert (= (card UNIVERALSET) n))
+(assert (= (card b) m))
+(assert (= (card c) (- f m)))
+(assert (>= m 0))
+(assert (>= f m))
+(assert (> n (+ (* 2 f) m)))
+
+
+(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n))
+
+(check-sat)
|