(set-logic QF_LRA) (declare-fun x1 () Real) (declare-fun x2 () Real) (assert (<= (+ (- x1) (* (- 2) x2)) (- 1))) (assert (<= (+ (* (- 2) x1) (- x2)) (- 1))) (assert (<= (+ x1 x2) 0.5)) (check-sat)