summaryrefslogtreecommitdiff
path: root/test/regress/regress0/issue2832-qualId.smt2
blob: ff6e6e8818d2e2fd4b51936509909c37300904a3 (plain)
1
2
3
4
5
6
7
8
9
(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((D 2)) ((par (T1 T2)
                                    ((CL  (get_CL  T1))
                                     (CR (get_CR T2))))))
(declare-sort U 0)
(declare-fun s0 () U)
(define-fun s1 () (D U U) ((as CL (D U U)) s0))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback