** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (_ FloatingPoint  8 24)) ; tracks user variable "x"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (assert (forall ((s1 (_ FloatingPoint  8 24)))
                   (let ((s2 (fp.isNaN s1)))
                   (let ((s3 (fp.isInfinite s1)))
                   (let ((s4 (or s2 s3)))
                   (let ((s5 (not s4)))
                   (let ((s6 (not s5)))
                   (let ((s7 (fp.leq s0 s1)))
                   (let ((s8 (or s6 s7)))
                   s8)))))))))
[SEND] (check-sat)
[RECV] sat
*** In a quantified context, obvservables will not be printed.
[SEND] (get-value (s0))
[RECV] ((s0 (_ -oo 8 24)))
*** Solver   : Z3
*** Exit code: ExitSuccess
[VALIDATE] Validating the model. Assignment:
[VALIDATE]       x =                -Infinity :: Float
[VALIDATE]       y = <universally quantified> :: Float

EXCEPTION RAISED:
*** Data.SBV: Cannot validate models in the presence of universally quantified variable "y"
***
***   To turn validation off, use `cfg{validateModel = False}`
***
*** Validation engine is not capable of handling this case. Failed to validate.