mirror of
https://github.com/Z3Prover/z3
synced 2026-02-22 00:07:36 +00:00
Delete examples/SMT-LIB2/finite-sets/cycle.smt2
This commit is contained in:
parent
7fe9b1f873
commit
24f36c2498
1 changed files with 0 additions and 67 deletions
|
|
@ -1,67 +0,0 @@
|
|||
(declare-const s1 (FiniteSet Int))
|
||||
(declare-const s2 (FiniteSet Int))
|
||||
(declare-const s3 (FiniteSet Int))
|
||||
(declare-const s4 (FiniteSet Int))
|
||||
(declare-const s5 (FiniteSet Int))
|
||||
(declare-const s6 (FiniteSet Int))
|
||||
(declare-const s7 (FiniteSet Int))
|
||||
(declare-const s8 (FiniteSet Int))
|
||||
(declare-const s9 (FiniteSet Int))
|
||||
(declare-const s10 (FiniteSet Int))
|
||||
|
||||
(declare-const s11 (FiniteSet Int))
|
||||
(declare-const s12 (FiniteSet Int))
|
||||
(declare-const s13 (FiniteSet Int))
|
||||
(declare-const s14 (FiniteSet Int))
|
||||
(declare-const s15 (FiniteSet Int))
|
||||
(declare-const s16 (FiniteSet Int))
|
||||
(declare-const s17 (FiniteSet Int))
|
||||
(declare-const s18 (FiniteSet Int))
|
||||
(declare-const s19 (FiniteSet Int))
|
||||
(declare-const s20 (FiniteSet Int))
|
||||
|
||||
(declare-const s21 (FiniteSet Int))
|
||||
(declare-const s22 (FiniteSet Int))
|
||||
(declare-const s23 (FiniteSet Int))
|
||||
(declare-const s24 (FiniteSet Int))
|
||||
(declare-const s25 (FiniteSet Int))
|
||||
(declare-const s26 (FiniteSet Int))
|
||||
(declare-const s27 (FiniteSet Int))
|
||||
(declare-const s28 (FiniteSet Int))
|
||||
(declare-const s29 (FiniteSet Int))
|
||||
(declare-const s30 (FiniteSet Int))
|
||||
|
||||
(assert (set.subset s1 s2))
|
||||
(assert (set.subset s2 s3))
|
||||
(assert (set.subset s3 s4))
|
||||
(assert (set.subset s4 s5))
|
||||
(assert (set.subset s5 s6))
|
||||
(assert (set.subset s6 s7))
|
||||
(assert (set.subset s7 s8))
|
||||
(assert (set.subset s8 s9))
|
||||
(assert (set.subset s9 s10))
|
||||
(assert (set.subset s10 s11))
|
||||
(assert (set.subset s11 s12))
|
||||
(assert (set.subset s12 s13))
|
||||
(assert (set.subset s13 s14))
|
||||
(assert (set.subset s14 s15))
|
||||
(assert (set.subset s15 s16))
|
||||
(assert (set.subset s16 s17))
|
||||
(assert (set.subset s17 s18))
|
||||
(assert (set.subset s18 s19))
|
||||
(assert (set.subset s19 s20))
|
||||
(assert (set.subset s20 s21))
|
||||
(assert (set.subset s21 s22))
|
||||
(assert (set.subset s22 s23))
|
||||
(assert (set.subset s23 s24))
|
||||
(assert (set.subset s24 s25))
|
||||
(assert (set.subset s25 s26))
|
||||
(assert (set.subset s26 s27))
|
||||
(assert (set.subset s27 s28))
|
||||
(assert (set.subset s28 s29))
|
||||
(assert (set.subset s29 s30))
|
||||
(assert (set.subset s30 s1))
|
||||
|
||||
(assert (or (not (= s1 s10)) (not (= s1 s11)) (not (= s1 s12)) (not (= s1 s13)) (not (= s1 s14)) (not (= s1 s15))))
|
||||
|
||||
(check-sat)
|
||||
Loading…
Add table
Add a link
Reference in a new issue