(set-option :produce-unsat-cores true)
(set-option :produce-models true)

(define-fun-rec size ((l (List Int))) Int
   (ite (= l nil) 0 (+ 1 (size (tail l)))))
   
(define-fun 
   isEmpty ((x (List Int))) Bool
   (= (size x) 0)
)

(define-fun 
   isNotEmpty ((x (List Int))) Bool
   (> (size x) 0)
)

(define-fun 
   safeAccess ((x (List Int)) (n (Int))) Bool
   (and (>= n 0) (< n (size x)))
)

(declare-const l2 (List Int))
(declare-const el Int)
(assert (! (= el (head l2)) :named l2_head_gets_el))
(assert (! (= (safeAccess l2 0) true) :named l2_head_is_safe))
(check-sat)
(get-model)

(declare-const l1 (List Int))
(assert (! (= nil l1) :named l1_is_nil))
(assert (! (= (safeAccess l1 0) true) :named l1_head_is_unsafe))
(check-sat)
(get-unsat-core)



(get-info :all-statistics)