mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
37 lines
990 B
Text
37 lines
990 B
Text
(set-logic QF_UFDT)
|
|
(declare-datatypes ((t 0))
|
|
(((T0) (T1 (prev1 t)) (T2 (prev2 t)))))
|
|
|
|
(declare-const c1 t)
|
|
(declare-const c2 t)
|
|
(declare-const c3 t)
|
|
(declare-const c4 t)
|
|
(declare-const c5 t)
|
|
(declare-const c6 t)
|
|
(declare-const c7 t)
|
|
(declare-const c8 t)
|
|
(declare-const c9 t)
|
|
(declare-const c10 t)
|
|
(assert (= c1 c10))
|
|
(assert (not (= c1 T0)))
|
|
(assert (not (= c2 T0)))
|
|
(assert (not (= c3 T0)))
|
|
(assert (not (= c4 T0)))
|
|
(assert (not (= c5 T0)))
|
|
(assert (not (= c6 T0)))
|
|
(assert (not (= c7 T0)))
|
|
(assert (not (= c8 T0)))
|
|
(assert (not (= c9 T0)))
|
|
(assert (not (= c10 T0)))
|
|
(assert (or (= c1 (T1 c2)) (= c1 (T2 c2))))
|
|
(assert (or (= c2 (T1 c3)) (= c2 (T2 c3))))
|
|
(assert (or (= c3 (T1 c4)) (= c3 (T2 c4))))
|
|
(assert (or (= c4 (T1 c5)) (= c4 (T2 c5))))
|
|
(assert (or (= c5 (T1 c6)) (= c5 (T2 c6))))
|
|
(assert (or (= c6 (T1 c7)) (= c6 (T2 c7))))
|
|
(assert (or (= c7 (T1 c8)) (= c7 (T2 c8))))
|
|
(assert (or (= c8 (T1 c9)) (= c8 (T2 c9))))
|
|
(assert (or (= c9 (T1 c10)) (= c9 (T2 c10))))
|
|
(check-sat)
|
|
(exit)
|
|
|