test/regress/regress1/fmf/dt-proper-model.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-sort U 0)
(declare-datatypes ((D 0)) (((cons (x Int) (y U)))))
(declare-fun d1 () D)
(declare-fun d2 () D)
(declare-fun d3 () D)
(declare-fun d4 () D)
(assert (distinct d1 d2 d3 d4))
(assert (forall ((x U) (y U)) (= x y)))
(declare-fun a () U)
(declare-fun P (U) Bool)
(assert (P a))
(check-sat)