test/regress/regress1/sygus/interpol_dt.smt2


1
2
3
4
5
6
7
8
9
10
11
12

; COMMAND-LINE: --produce-interpols=default
; 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)
(declare-fun y () List)
(assert ((_ is cons) x))
(assert ((_ is nil) (tail x)))
(assert (= (head x) 0))
(assert (= x y))
(get-interpol A (distinct y nil))