smt-lib compliance turns `unsat` to `unknown` (with a bizarre unknown message)

[LeventErkok]

Given:

(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))

(define-fun sbv.rat.eq ((x SBVRational) (y SBVRational)) Bool
   (= (* (sbv.rat.numerator   x) (sbv.rat.denominator y))
      (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))
)

(define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool
   (not (sbv.rat.eq x y))
)
(define-fun s4 () Real 0.0)
(declare-fun s0 () SBVRational)
(assert (< 0 (sbv.rat.denominator s0)))
(declare-fun s1 () SBVRational) ; tracks user variable "__internal_sbv_s1"
(assert (< 0 (sbv.rat.denominator s1)))
(define-fun s2 () Int (sbv.rat.denominator s1))
(define-fun s3 () Real (to_real s2))
(define-fun s5 () Bool (= s3 s4))
(define-fun s6 () Int (sbv.rat.numerator s1))
(define-fun s7 () Real (to_real s6))
(define-fun s8 () Real (/ s7 s3))
(define-fun s9 () Real (ite s5 s4 s8))
(define-fun s10 () Int (sbv.rat.denominator s0))
(define-fun s11 () Real (to_real s10))
(define-fun s12 () Bool (= s4 s11))
(define-fun s13 () Int (sbv.rat.numerator s0))
(define-fun s14 () Real (to_real s13))
(define-fun s15 () Real (/ s14 s11))
(define-fun s16 () Real (ite s12 s4 s15))
(define-fun s17 () Bool (= s9 s16))
(define-fun s18 () Bool (sbv.rat.eq s0 s1))
(assert s17)
(assert (not s18))
(check-sat)
(get-info :reason-unknown)

z3 says:

unknown
(:reason-unknown "Sort mismatch at argument #2 for function (declare-fun * (Real Real) Real) supplied sort is Int")

That unknown reason is really confusing to me; but maybe it's indicative of a deeper problem. Indeed, if you comment out the line:

; (set-option :smtlib2_compliant true)

You get:

unsat

which is the correct answer.