Newer
Older
(set-info :smt-lib-version 2.6)
(set-logic QF_FPNRA)
(set-info :category |Crafted from GATeL POs|)
(set-info :status unsat)
(declare-fun dx () Float64)
(declare-fun dy () Float64)
(define-fun x () Real
(fp.to_real dx))
(define-fun y () Real
(fp.to_real dy))
(define-fun isFinite ((F Float64)) Bool
(and (not (fp.isInfinite F))
(not (fp.isNaN F))))
(assert (and (isFinite dx) (isFinite dy)))
(define-fun s2r () Real
(+ (* (+ x y) (+ x y))
(* 2.0 x x)
(* 2.0 y y)))
(assert (not
(=> (and (<= (- 2.0) x 2.0) (<= (- 2.0) y 2.0)) (<= 0.0 s2r 32.0))
))
(check-sat)