I'm trying to put a limit on the size of elements of a datatype generated by Z3.

Concretely, let's say I have the following functions and constraints:

(define-fun-rec length ((l (List Int))) Int
   (if ((_ is nil) l) 0 (+ 1 (length (tail l)))))

; (all-two l) means that every element of l is 2
(define-fun-rec all-two ((l (List Int))) Bool 
   (if ((_ is nil) l)
       true
       (and (= (head l) 2) (all-two (tail l)))))

(define-fun-rec sum ((l (List Int))) Int 
   (if ((_ is nil) l)
       0
       (+ (head l) (sum (tail l)))))

(define-fun N () Int 6)
(declare-const l (List Int))
(assert (all-two l))
(assert (= (sum l) N))
(check-sat)
(get-model)

If N is 6, Z3 quickly returns a model where l is [2,2,2] as expected. If N is much larger (say 100), it takes more time to find the model, which is expected, but it eventually does.

However, if N is odd, say 1, then I never get the answer that my constraints are unsat, because Z3 seems to just try longer and longer lists indefinitely. I don't expect that it would actually answer unsat because I understand it really just "unfolds" the recursive definitions when encountered. However, I would like to be able to control when to stop searching. Adding an assertion that bounds length l does not help since length itself is a recursive function that will be unrolled. I could put a timeout or maybe set the r-limit, but these are global metrics that are also influenced by the rest of my constraints, so I'm looking for something more fine-grained.

Is there a way to tell Z3 to stop searching (and possibly return unknown) at a certain datatype size?

I've tried looking into the parameters but I did not find my answer there.