Exercise 7 -- LraTest.smt2
LraEx1aTest.smt2 — Plain Text, 196 bytes
File contents
(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)