Skip to content
Snippets Groups Projects
Normal view Permalink
sq_id_nra_5_unsat.smt2 248 B
Newer Older
Bruno Marre's avatar
encore des benchs
Bruno Marre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 

(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)

(assert (not
	(>= 0.0 (- (+ (* x x) (* y y) (* 2.0 x y))))
	))
(check-sat)