z3 returning unknown when using Floats and Reals together?

Question

As I was using Floats and Reals in the same .smt2 file, I noticed that this would often lead to the result being "unknown". I have seen this mentioned here but as some time has passed since this answer I wanted to ask if maybe I'm simply not using the correct settings (e.g. Should I maybe be passing a tactic as parameter in the check-sat line? Or narrowing down set-logic?)

Here is an example that exhibits the behavior:

(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.6)

(set-info :status unknown)
(define-sort FPN () (_ FloatingPoint  8  24))

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)

(declare-fun x0 () FPN)
(declare-fun y0 () FPN)
(declare-fun z0 () FPN)

(declare-fun x1 () FPN)
(declare-fun y1 () FPN)
(declare-fun z1 () FPN)

(define-fun fun ( (x FPN) (y FPN) (z FPN) (arg0 Real) (arg1 Real) (arg2 Real)) FPN (fp.add RNE 
                                                                                           (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE arg0) x)
                                                                                                       (fp.mul RNE ((_ to_fp 8 24) RNE arg1) y))
                                                                                           (fp.mul RNE ((_ to_fp 8 24) RNE arg2) z)) )

(assert (fp.eq x0 ((_ to_fp 8 24) RNE 1)))
(assert (fp.eq y0 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq z0 ((_ to_fp 8 24) RNE 0)))

(assert (fp.eq x1 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq y1 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq z1 ((_ to_fp 8 24) RNE 0)))

(assert
  (fp.gt (fun x0 y0 z0 a b c) (fun x1 y1 z1 a b c))
)


(check-sat)
(get-info :reason-unknown)
(get-model)
(exit)

Thank you so much for any responses!