1 2 3 4 5 6 7 8 9 10 11
; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-sort elem 0) (declare-datatypes () ((list (Nil) (Cons (hd elem) (tl list))))) (define-fun-rec f ((x list)) elem (ite (is-Nil x) (f x) (hd x)) ) (declare-fun t () elem) (assert (= t (f Nil))) (check-sat)