Newer
Older
(set-info :smt-lib-version 2.6)
(set-logic QF_NRA)
(set-info :category |Crafted from GATeL POs|)
(set-info :status unsat)
(declare-fun x () Real)
(declare-fun y () Real)
(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)