Unexpected performance difference between define-fun and define-funcs-rec in smt

[pjljvandelaar]

When I run z3 with the following model in smt2.5

(set-info :smt-lib-version 2.5)
(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes () ((a0(c0$0(c0$0$0 Bool))(c0$1)(c0$2(c0$2$0 a6)(c0$2$1 a6)(c0$2$2 a8)(c0$2$3 a9)(c0$2$4 a6)(c0$2$5 Bool)(c0$2$6 a9)(c0$2$7 a2)(c0$2$8 a7)(c0$2$9 Int)(c0$2$a a6)(c0$2$b Int)(c0$2$c a8))(c0$3)(c0$4)(c0$5)(c0$6)(c0$7(c0$7$0 aa)(c0$7$1 a9)))(a1(c1$0(c1$0$0 String)(c1$0$1 Int)(c1$0$2 Int)(c1$0$3 String)(c1$0$4 Bool)(c1$0$5 String)(c1$0$6 String)(c1$0$7 Int)(c1$0$8 Bool))(c1$1(c1$1$0 a0)(c1$1$1 a9)(c1$1$2 a2)(c1$1$3 Int)))(a2(c2$0)(c2$1)(c2$2(c2$2$0 a0)(c2$2$1 String))(c2$3)(c2$4(c2$4$0 a2)(c2$4$1 a8)(c2$4$2 a6))(c2$5)(c2$6)(c2$7(c2$7$0 String)(c2$7$1 a5)(c2$7$2 a9)(c2$7$3 Bool)(c2$7$4 a0)(c2$7$5 String))(c2$8)(c2$9)(c2$a)(c2$b)(c2$c)(c2$d)(c2$e)(c2$f)(c2$10))(a3(c3$0)(c3$1)(c3$2)(c3$3)(c3$4(c3$4$0 a3)(c3$4$1 a5)(c3$4$2 Int)(c3$4$3 a1)(c3$4$4 a5)(c3$4$5 a6)(c3$4$6 a4))(c3$5)(c3$6(c3$6$0 a8))(c3$7)(c3$8)(c3$9(c3$9$0 Int)(c3$9$1 a4))(c3$a)(c3$b)(c3$c)(c3$d)(c3$e)(c3$f(c3$f$0 a5)(c3$f$1 a0)(c3$f$2 a8))(c3$10)(c3$11)(c3$12))(a4(c4$0)(c4$1(c4$1$0 a8)(c4$1$1 a3))(c4$2)(c4$3)(c4$4)(c4$5)(c4$6)(c4$7)(c4$8)(c4$9))(a5(c5$0(c5$0$0 Bool)(c5$0$1 Int)(c5$0$2 a1)(c5$0$3 a8)(c5$0$4 a8)(c5$0$5 a7)(c5$0$6 a1))(c5$1(c5$1$0 a8)(c5$1$1 a1)))(a6(c6$0)(c6$1(c6$1$0 a4)(c6$1$1 a6)(c6$1$2 a8)(c6$1$3 a3)(c6$1$4 aa)(c6$1$5 a4)(c6$1$6 a5))(c6$2)(c6$3(c6$3$0 a0)(c6$3$1 aa)(c6$3$2 a1)(c6$3$3 a2)(c6$3$4 Bool))(c6$4)(c6$5)(c6$6)(c6$7(c6$7$0 aa)))(a7(c7$0)(c7$1)(c7$2(c7$2$0 a3)(c7$2$1 a4)(c7$2$2 a7)(c7$2$3 a4)(c7$2$4 a9)(c7$2$5 a8))(c7$3)(c7$4(c7$4$0 a8))(c7$5(c7$5$0 a9))(c7$6))(a8(c8$0(c8$0$0 String))(c8$1)(c8$2)(c8$3(c8$3$0 a2)(c8$3$1 a7)(c8$3$2 a1))(c8$4)(c8$5)(c8$6)(c8$7(c8$7$0 a4)(c8$7$1 aa)(c8$7$2 a4))(c8$8(c8$8$0 a4)(c8$8$1 a2))(c8$9)(c8$a)(c8$b))(a9(c9$0(c9$0$0 a5)(c9$0$1 a7)(c9$0$2 String))(c9$1)(c9$2)(c9$3)(c9$4)(c9$5)(c9$6(c9$6$0 a4)(c9$6$1 a5)(c9$6$2 a7)(c9$6$3 a1)(c9$6$4 a5)(c9$6$5 a3))(c9$7)(c9$8))(aa(ca$0(ca$0$0 a0)(ca$0$1 a9)(ca$0$2 a1)(ca$0$3 a7))(ca$1)(ca$2(ca$2$0 a8)(ca$2$1 a8)(ca$2$2 a9))(ca$3)(ca$4(ca$4$0 a4)(ca$4$1 a9)(ca$4$2 a3))(ca$5))))
(define-fun f3 ((v29 a5)) String
            (ite (is-c1$0 (ite (is-c8$3 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) (c8$3$2 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) (c1$1 c0$5 c9$4 c2$1 (- 1)))) (c1$0$5 (ite (is-c8$3 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) 
                 (c8$3$2 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) (c1$1 c0$5 c9$4 c2$1 (- 1)))) "x~\x06\xef\x8aA\x92"
            )
)
(push 1)
(declare-fun v2a() a1)
(declare-fun v2b() aa)
(declare-fun v2c() a7)
(declare-fun v2d() String)
(declare-fun v2e() a0)
(declare-fun v2f() Int)
(declare-fun v30() a7)
(declare-fun v31() a5)
(declare-fun v32() String)
(declare-fun v33() a8)
(declare-fun v34() a9)
(declare-fun v35() a6)
(assert (= (c1$0 "" (- 2) 0 "" false "\xf0t\x9e" """" (- 1) false) v2a))
(assert (= ca$1 v2b))
(assert (= c7$3 v2c))
(assert (= "\x8e\x10\xa8=Y\xca)~" v2d))
(assert (= (c0$2 c6$4 c6$0 c8$4 c9$1 (c6$7 ca$3) false c9$2 c2$6 c7$0 1 c6$4 0 (c8$7 c4$8 ca$3 c4$2)) v2e))
(assert (= (- 18) v2f))
(assert (= c7$3 v30))
(assert (= (c5$1 c8$a (c1$1 c0$3 c9$1 c2$a (- 2))) v31))
(assert (= "\x8e\x10\xa8=Y\xca)~" v32))
(assert (= c8$2 v33))
(assert (= c9$8 v34))
(assert (= (c6$7 ca$1) v35))
(check-sat)
(exit)

I almost immediately get sat (as expected).
When I use the define-funcs-rec instead of define-fun, hence

(set-info :smt-lib-version 2.5)
(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes () ((a0(c0$0(c0$0$0 Bool))(c0$1)(c0$2(c0$2$0 a6)(c0$2$1 a6)(c0$2$2 a8)(c0$2$3 a9)(c0$2$4 a6)(c0$2$5 Bool)(c0$2$6 a9)(c0$2$7 a2)(c0$2$8 a7)(c0$2$9 Int)(c0$2$a a6)(c0$2$b Int)(c0$2$c a8))(c0$3)(c0$4)(c0$5)(c0$6)(c0$7(c0$7$0 aa)(c0$7$1 a9)))(a1(c1$0(c1$0$0 String)(c1$0$1 Int)(c1$0$2 Int)(c1$0$3 String)(c1$0$4 Bool)(c1$0$5 String)(c1$0$6 String)(c1$0$7 Int)(c1$0$8 Bool))(c1$1(c1$1$0 a0)(c1$1$1 a9)(c1$1$2 a2)(c1$1$3 Int)))(a2(c2$0)(c2$1)(c2$2(c2$2$0 a0)(c2$2$1 String))(c2$3)(c2$4(c2$4$0 a2)(c2$4$1 a8)(c2$4$2 a6))(c2$5)(c2$6)(c2$7(c2$7$0 String)(c2$7$1 a5)(c2$7$2 a9)(c2$7$3 Bool)(c2$7$4 a0)(c2$7$5 String))(c2$8)(c2$9)(c2$a)(c2$b)(c2$c)(c2$d)(c2$e)(c2$f)(c2$10))(a3(c3$0)(c3$1)(c3$2)(c3$3)(c3$4(c3$4$0 a3)(c3$4$1 a5)(c3$4$2 Int)(c3$4$3 a1)(c3$4$4 a5)(c3$4$5 a6)(c3$4$6 a4))(c3$5)(c3$6(c3$6$0 a8))(c3$7)(c3$8)(c3$9(c3$9$0 Int)(c3$9$1 a4))(c3$a)(c3$b)(c3$c)(c3$d)(c3$e)(c3$f(c3$f$0 a5)(c3$f$1 a0)(c3$f$2 a8))(c3$10)(c3$11)(c3$12))(a4(c4$0)(c4$1(c4$1$0 a8)(c4$1$1 a3))(c4$2)(c4$3)(c4$4)(c4$5)(c4$6)(c4$7)(c4$8)(c4$9))(a5(c5$0(c5$0$0 Bool)(c5$0$1 Int)(c5$0$2 a1)(c5$0$3 a8)(c5$0$4 a8)(c5$0$5 a7)(c5$0$6 a1))(c5$1(c5$1$0 a8)(c5$1$1 a1)))(a6(c6$0)(c6$1(c6$1$0 a4)(c6$1$1 a6)(c6$1$2 a8)(c6$1$3 a3)(c6$1$4 aa)(c6$1$5 a4)(c6$1$6 a5))(c6$2)(c6$3(c6$3$0 a0)(c6$3$1 aa)(c6$3$2 a1)(c6$3$3 a2)(c6$3$4 Bool))(c6$4)(c6$5)(c6$6)(c6$7(c6$7$0 aa)))(a7(c7$0)(c7$1)(c7$2(c7$2$0 a3)(c7$2$1 a4)(c7$2$2 a7)(c7$2$3 a4)(c7$2$4 a9)(c7$2$5 a8))(c7$3)(c7$4(c7$4$0 a8))(c7$5(c7$5$0 a9))(c7$6))(a8(c8$0(c8$0$0 String))(c8$1)(c8$2)(c8$3(c8$3$0 a2)(c8$3$1 a7)(c8$3$2 a1))(c8$4)(c8$5)(c8$6)(c8$7(c8$7$0 a4)(c8$7$1 aa)(c8$7$2 a4))(c8$8(c8$8$0 a4)(c8$8$1 a2))(c8$9)(c8$a)(c8$b))(a9(c9$0(c9$0$0 a5)(c9$0$1 a7)(c9$0$2 String))(c9$1)(c9$2)(c9$3)(c9$4)(c9$5)(c9$6(c9$6$0 a4)(c9$6$1 a5)(c9$6$2 a7)(c9$6$3 a1)(c9$6$4 a5)(c9$6$5 a3))(c9$7)(c9$8))(aa(ca$0(ca$0$0 a0)(ca$0$1 a9)(ca$0$2 a1)(ca$0$3 a7))(ca$1)(ca$2(ca$2$0 a8)(ca$2$1 a8)(ca$2$2 a9))(ca$3)(ca$4(ca$4$0 a4)(ca$4$1 a9)(ca$4$2 a3))(ca$5))))
(define-funs-rec ((f3((v29 a5))String))
                 ((ite (is-c1$0 (ite (is-c8$3 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) (c8$3$2 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) (c1$1 c0$5 c9$4 c2$1 (- 1)))) (c1$0$5 (ite (is-c8$3 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) 
                       (c8$3$2 (ite (is-c3$6 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) (c3$6$0 (ite (is-c7$2 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) (c7$2$0 (ite (is-c8$3 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) (c8$3$1 (ite (is-c7$2 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) (c7$2$5 (ite (is-c5$0 v29) (c5$0$5 v29) c7$1)) c8$5)) c7$3)) c3$3)) c8$6)) (c1$1 c0$5 c9$4 c2$1 (- 1)))) "x~\x06\xef\x8aA\x92"
                  ))
)
(push 1)
(declare-fun v2a() a1)
(declare-fun v2b() aa)
(declare-fun v2c() a7)
(declare-fun v2d() String)
(declare-fun v2e() a0)
(declare-fun v2f() Int)
(declare-fun v30() a7)
(declare-fun v31() a5)
(declare-fun v32() String)
(declare-fun v33() a8)
(declare-fun v34() a9)
(declare-fun v35() a6)
(assert (= (c1$0 "" (- 2) 0 "" false "\xf0t\x9e" """" (- 1) false) v2a))
(assert (= ca$1 v2b))
(assert (= c7$3 v2c))
(assert (= "\x8e\x10\xa8=Y\xca)~" v2d))
(assert (= (c0$2 c6$4 c6$0 c8$4 c9$1 (c6$7 ca$3) false c9$2 c2$6 c7$0 1 c6$4 0 (c8$7 c4$8 ca$3 c4$2)) v2e))
(assert (= (- 18) v2f))
(assert (= c7$3 v30))
(assert (= (c5$1 c8$a (c1$1 c0$3 c9$1 c2$a (- 2))) v31))
(assert (= "\x8e\x10\xa8=Y\xca)~" v32))
(assert (= c8$2 v33))
(assert (= c9$8 v34))
(assert (= (c6$7 ca$1) v35))
(check-sat)
(exit)

I don't get an answer within 20 minutes and z3 consumes over 10 Gigabytes of data.
I understand the concepts are slightly different, yet f3 isn't used and is not recursive so I didn't expect such a hugh change in performance.
Can you please look at it to investigate this unexpected change in performance?

[pjljvandelaar]

For this case problem is indeed solved.
However, for a similar case
z3UnexpectedlySlow.smt2.txt
the same slow performance is still observed.

[NikolajBjorner]

@c-cube: what do you think? the bottleneck is the unfolding of ite expressions as they are assumed (pessimistically) to be guards for recursive function definitions. The ite expressions occur deeply nested and the unfolding multiplies.

[c-cube]

I imagine there are two possible workarounds here:

• detecting if functions are actually recursive before translating them (otherwise it's just a normal if)
• only unfolding if in cases one of its subterms contains a recursive call (to a function in the same mutually recursive block); that's more precise but probably more work to implement.

[NikolajBjorner]

The parser issues the main calls to setting definitions after each body is parsed.
The relevant function call is m_ctx.insert_rec_fun. The bodies of other recursive functions have not been parsed at that point. The parser would need to be changed.

I only unfold a term if it contains an if, which contains a potentially recursive function.
The function may or may not be recursive, of course.

Note that the normalization to cases doesn't do well with shared subterms eitther.
Perhaps there is one version where it handles shared subterms well.

[pjljvandelaar]

Run our unit tests with the latest nightly build today.
After 3498 tests, quickCheck generate once more a file which Z3 can't handle.
z3Slow.txt
The large number of test cases hint that it might be a corner case...

All data types in this example have multiple constructors, which invalidate my hypotheses that it might be related to data types with a single constructor.
Accessors of data types with a single constructor don't need to check that the right constructor is used in advance. So these accessors do not need to be encapsolated in ITEs which might force Z3 to unfold more than for accessors of data types with multiple constructors.
Yet, no such data type is present in the example, so I can't help you ;-(

[NikolajBjorner]

It is hitting the same bottleneck that causes the recursive function compiler to create large ite unfoldings. It would require a re-do of how recursive functions are pre-processed to make this scalable.
The scalable approach is probably to push the unfolding of ite over recursive functions into the module that is responsible for unfolding recursive function definitions. It will not require the same up-front unfolding but would be able to afford an incremental unfolding.

[NikolajBjorner]

See duplicate #2985