You are here: Home Decision Procedures Resources Lra test file

Lra test file

Plain Text icon 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)