blob: 6f0fb84f2b50bc0edd83558cb52e7e09d1309d09 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(set-logic UFDTLIA)
(set-info :status sat)
(set-option :finite-model-find true)
(declare-sort a 0)
(declare-sort b 0)
(declare-datatypes ((c 0)) (((d (m b)))))
(declare-sort d 0)
(declare-sort e 0)
(declare-datatypes ((f 0)) (((n))))
(declare-fun o (f e d c) a)
(declare-fun g (f) e)
(declare-fun h (f d) c)
(declare-fun i () f)
(declare-fun j (e) d)
(assert (forall ((k e)) (exists ((l c)) (= (o i k (j k) l) (o i (g i) (j k) (h i (j k)))))))
(check-sat)
|
