** 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
[VALIDATE] NB. The following variable(s) are universally quantified: y
[VALIDATE]     We will assume that they are essentially zero for the purposes of validation.
[VALIDATE]     Note that this is a gross simplification of the model validation with universals!
[VALIDATE] There are no constraints to check.
[VALIDATE] Validating outputs.
[VALIDATE] All outputs are satisfied. Validation complete.

FINAL OUTPUT:
Satisfiable. Model:
  x = -Infinity :: Float