Z3 Solver 오류: DataTypes

[hongjisung]

(declare-datatypes () (( LList nil (cons (head Int) (tail LList)))))
(define-fun f ((x LList)) Int (+ (+ 1 0) (head x)))
(assert (= (f (cons 4 nil)) 5) )
(assert (= (f (cons 0 nil)) 1) )
(assert (= (f nil) 0) )
(check-sat)

위와 같은 경우에 sat으로 처리되는 문제
(head nil)을 이상하게 처리