sq_id_fp_nra_3_unsat.smt2

(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 s2 () Real
  (+ (+ (+ (- (* (* 1.9 x) x)
	      (* y y))
	   (* (* 2.0 x) y))
	(* (* 1.1 x) x))
     (* (* 4.0 y) y)))

(define-fun s2r () Real
  (+ (* (+ x y) (+ x y))
     (* 2.0 x x)
     (* 2.0 y y)))

(assert (not
	(= s2 s2r)
	))
(check-sat)