; COMMAND-LINE: --fmf-fun-rlv --no-check-models
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(define-fun $$isTrue$$ ((b Bool)) Bool b)
(define-fun $$isFalse$$ ((b Bool)) Bool (not b))
(define-fun $$toString$$ ((b Bool)) String (ite b "true" "false"))
(define-fun $$fromString$$ ((s String)) Bool (= s "true"))
(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (str.from_int (- i))) (str.from_int i)))
(declare-fun $$takeWhile$$ (String String) String)
(declare-fun $$takeWhileNot$$ (String String) String)
(declare-fun $$dropWhile$$ (String String) String)
(declare-fun $$dropWhileNot$$ (String String) String)
(declare-datatypes ((AddressType 0) (Conditional_Int 0) (Conditional_dateTime 0) (Conditional_string 0) (CustomerType 0) (List_CustomerType 0) (List_OrderType 0) (OrderType 0) (RootType 0) (ShipInfoType 0)) (
((AddressType$C_AddressType (AddressType$C_AddressType$address String) (AddressType$C_AddressType$city String) (AddressType$C_AddressType$region String) (AddressType$C_AddressType$postalCode String) (AddressType$C_AddressType$country String)))
((Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int)))
((Conditional_dateTime$CAbsent_dateTime) (Conditional_dateTime$CPresent_dateTime (Conditional_dateTime$CPresent_dateTime$value Int)))
((Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String)))
((CustomerType$C_CustomerType (CustomerType$C_CustomerType$companyName String) (CustomerType$C_CustomerType$contactName String) (CustomerType$C_CustomerType$contactTitle String) (CustomerType$C_CustomerType$phone String) (CustomerType$C_CustomerType$fax Conditional_string) (CustomerType$C_CustomerType$fullAddress AddressType) (CustomerType$C_CustomerType$customerID Int)))
((List_CustomerType$CNil_CustomerType) (List_CustomerType$Cstr_CustomerType (List_CustomerType$Cstr_CustomerType$head CustomerType) (List_CustomerType$Cstr_CustomerType$tail List_CustomerType)))
((List_OrderType$CNil_OrderType) (List_OrderType$Cstr_OrderType (List_OrderType$Cstr_OrderType$head OrderType) (List_OrderType$Cstr_OrderType$tail List_OrderType)))
((OrderType$C_OrderType (OrderType$C_OrderType$customerID Int) (OrderType$C_OrderType$employeeID Int) (OrderType$C_OrderType$orderDate Int) (OrderType$C_OrderType$requiredDate Int) (OrderType$C_OrderType$shipInfo ShipInfoType)))
((RootType$C_RootType (RootType$C_RootType$customers List_CustomerType) (RootType$C_RootType$orders List_OrderType)))
((ShipInfoType$C_ShipInfoType (ShipInfoType$C_ShipInfoType$shipVia Int) (ShipInfoType$C_ShipInfoType$freight Int) (ShipInfoType$C_ShipInfoType$shipName String) (ShipInfoType$C_ShipInfoType$shipAddress String) (ShipInfoType$C_ShipInfoType$shipCity String) (ShipInfoType$C_ShipInfoType$shipRegion String) (ShipInfoType$C_ShipInfoType$shipPostalCode String) (ShipInfoType$C_ShipInfoType$shipCountry String) (ShipInfoType$C_ShipInfoType$shippedDate Conditional_dateTime)))
))
(define-fun f2866$toXml((a$$2869 AddressType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "" "") (AddressType$C_AddressType$address a$$2869)) "") "") (AddressType$C_AddressType$city a$$2869)) "") "") (AddressType$C_AddressType$region a$$2869)) "") "") (AddressType$C_AddressType$postalCode a$$2869)) "") "") (AddressType$C_AddressType$country a$$2869)) "") ""))
(define-fun f2656$toXml((c$$2659 CustomerType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "") "") (CustomerType$C_CustomerType$companyName c$$2659)) "") "") (CustomerType$C_CustomerType$contactName c$$2659)) "") "") (CustomerType$C_CustomerType$contactTitle c$$2659)) "") "") (CustomerType$C_CustomerType$phone c$$2659)) "") (ite ((_ is Conditional_string$CPresent_string) (CustomerType$C_CustomerType$fax c$$2659)) (str.++ (str.++ "" (Conditional_string$CPresent_string$value (CustomerType$C_CustomerType$fax c$$2659))) "") "")) (f2866$toXml (CustomerType$C_CustomerType$fullAddress c$$2659))) ""))
(define-funs-rec
(
(f2574$toXml((lc$$2577 List_CustomerType)) String)
)
(
(ite ((_ is List_CustomerType$CNil_CustomerType) lc$$2577) "" (str.++ (f2656$toXml (List_CustomerType$Cstr_CustomerType$head lc$$2577)) (f2574$toXml (List_CustomerType$Cstr_CustomerType$tail lc$$2577))))
)
)
(define-fun f2942$toXml((s$$2945 ShipInfoType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "") ">")) "") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$shipVia s$$2945))) "") "") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$freight s$$2945))) "") "") (ShipInfoType$C_ShipInfoType$shipName s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipAddress s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipCity s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipRegion s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipPostalCode s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipCountry s$$2945)) "") ""))
(define-fun f2776$toXml((o$$2779 OrderType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "" "") ($$inttostr$$ (OrderType$C_OrderType$customerID o$$2779))) "") "") ($$inttostr$$ (OrderType$C_OrderType$employeeID o$$2779))) "") "") ($$inttostr$$ (OrderType$C_OrderType$orderDate o$$2779))) "") "") ($$inttostr$$ (OrderType$C_OrderType$requiredDate o$$2779))) "") (f2942$toXml (OrderType$C_OrderType$shipInfo o$$2779))) ""))
(define-funs-rec
(
(f2615$toXml((lo$$2618 List_OrderType)) String)
)
(
(ite ((_ is List_OrderType$CNil_OrderType) lo$$2618) "" (str.++ (f2776$toXml (List_OrderType$Cstr_OrderType$head lo$$2618)) (f2615$toXml (List_OrderType$Cstr_OrderType$tail lo$$2618))))
)
)
(define-fun f2526$toXml((r$$2529 RootType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "" "") (f2574$toXml (RootType$C_RootType$customers r$$2529))) "") "") (f2615$toXml (RootType$C_RootType$orders r$$2529))) "") ""))
(declare-fun $Report$3105$0$1$() String)
(assert (= $Report$3105$0$1$ ""))
; should be fast since functions introduced by define-fun-rec do not appear in the ground assertion
(check-sat)