path: root/test/regress/regress1/abduct-dt.smt2

; COMMAND-LINE: --produce-abducts
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
(set-logic ALL)
(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
(declare-fun x () List)
(assert (distinct x nil))
(get-abduct A (= x (cons (head x) (tail x))))