Avoiding `unknown` for *, / over Reals?

I'm trying find a solution to a problem of dividing elements from a Sequence into N groups that are roughly evenly distributed. I thought I was making good progress by using a "G-Test" and setting a goal of it being under some maximum value, but I keep getting "unknown" and I think I narrowed it down to this (ln-approx x) function. Since z3 can't do (ln x) I am hoping to use this approximation, but even when avoiding x = -1 I don't see success. I get unknown and a reason of canceled.

Is there a way to avoid this unknown?

Is there a better technique for evaluating a solutions "cardinal balance" among partitions, I might call it?

; approximation that looks close enough for me on the graph for [0 .. 1]
(define-fun ln-approx ((x Real)) Real (ite (<= 0.0 x 1.0) (* 2.0 (/ (- x 1.0) (+ x 1.0))) 1000.0))

By the way, is there a way to write in native z3 to (get-model) only if (check-sat) sat and ask for reasons and other diagnostics if unsat?

Here is the function I'm using instead of ln compared to ln which I assume will be close enough for a useful g-test calculation. Since 0 < O < E, then 0.0 < O/E <= 1.0. The E = 0 case is ited in my g-test implementation.

https://www.desmos.com/calculator/1wh6g3glkx

For background, here's my current g-test implementation, (missing some of the supporting types):

; g-test of an attribute
(define-fun attr-g-test ((attr-count-accessor (Array AttrCounts Int))) Real
    (* 2.0
    (seq.foldli
        (lambda ((group_0_based Int) (half-score Real) (ignored Bool))
            (let 
                ((O (attr-count-accessor (attr-counts students (+ group_0_based 1))))
                (E (attr-count-accessor G_COUNTS)))
                (+ half-score (ite (< 0 O E) (* O (ln-approx (/ O E))) 0.0)))
                ;(+ half-score (* O 1.2))) ;; something like this instead is `sat` (but otherwise useless)
        )
        0 ; offset
        0.0 ; null-hypothesis initial value
        group-iterable-range))
)

I'm not surprised you're getting unknown. You are using foldli (a higher-order function), you have non-linear terms ((x - 1) / (x + 1)), and you're using sequences. You're pushing what theory-combination can get you, at least for the current state of the art.

Without seeing your entire input, it's hard to opine further. But you might want to try the nra tactic (non-linear real arithmetic), and simplify so you don't need foldi (by using a constant length list of booleans, instead of a symbolic sequence.)

Regarding your question By the way, is there a way to write in native z3 to (get-model) only if (check-sat) sat and ask for reasons and other diagnostics if unsat?. The short answer is no. SMTLib doesn't have any control-structures. You typically use a higher-level binding (from Haskell/Python/C etc.) to do this sort of processing.