Z3 adding assertion with recursive function call cause an infinite number of instance creation

[duncan020313]

I'm trying to model a recursive function with sequence access.

(declare-const seq_case (Seq Int))

(define-fun-rec seq_rec_func ((input_arg Int)) Int
  (ite (<= input_arg (seq.len seq_case))
       0
       (seq_rec_func (+ input_arg 1))))

(assert (= (seq.len seq_case) 10))
(assert (= (seq_rec_func 0) 0)) ;; table overflow!!

If I execute this, the solver begins to generate an infinite number of instances that are internally relevant to seq_rec_func.
How can I prevent this? Is there any option to avoid the infinite unrolling of the recursive function?

Here are the last 20 lines of the log

[instance] 0x0 #275030
[attach-enode] #275030 0
[end-of-instance]
[mk-app] #275031 Int
[attach-meaning] #275031 arith 21154
[inst-discovered] theory-solving 0x0 arith# ; #275021
[mk-app] #275032 = #275021 #275031
[instance] 0x0 #275032
[attach-enode] #275032 0
[end-of-instance]
[mk-app] #275033 <= #275031 #24
[mk-app] #275034 + #275031 #27
[mk-app] #275035 seq_rec_func #275034
[mk-app] #275036 if #275033 #26 #275035
[mk-app] #275037 seq_rec_func #275031
[inst-discovered] theory-solving 0x0 recfun# ; #275037
[mk-app] #275038 = #275037 #275036
[instance] 0x0 #275038
[attach-enode] #275038 0
[end-of-instance]

[hailinzeng]

Got the same "table overflow" z3::exception. The exception seems throw in https://github.com/Z3Prover/z3/blob/master/src/util/chashtable.h#L164