Issue with recursive function definition when ite uses a recursive call

[jorgelopezcoronado]

Hi,

I'm experiencing some issues with recent versions of z3. I have a very basic example:

(define-fun-rec max_array ( (arr (Array Int Real)) (size Int) ) Real
	(ite (<= size 0) 
		(select arr size)
		(ite (< (select arr size) (max_array arr (- size 1)))
			(max_array arr (- size 1))
			(select arr size)
		)
	)
)

(declare-const A (Array Int Real))
(assert (= (select A 0) 3.0))
(assert (= (select A 1) 1.1))
(assert (= (select A 2) 6.02))
(assert (= (select A 3) 2.2))
(assert (= (select A 4) 5.2))
(assert (= (select A 5) 5.5))
(assert (= (select A 6) 4.1))
(assert (= (select A 7) 0.3))
(assert (= (select A 8) 1.8))
(assert (= (select A 9) 4.7))

(assert (>= (max_array A 9) 6))

(check-sat)

When executing this on recent versions z3 it'll consume all available memory (it seems very much like an unbounded recursive call). This behavior only occurs when the ite condition contains a recursive call. I didn't look up the potential issue in the code. However, this issue started to appear in version 4.8.11; executing this code in version 4.8.10 yields a sat result, as expected.

Could you kindly help? Sorry, for not helping a bit more with the debugging.

Thank you very much,

Jorge