blob: cf5c3bc7ed45a8e79b6c8258b72d4c3d061c0fbc (
plain)
1
2
3
4
5
6
7
8
9
|
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic LRA)
(declare-fun y1 () Real)
(declare-fun y2 () Real)
(declare-fun x1 () Real)
(assert (forall ((?y1 Real)) (exists ((?y2 Real)) (or (and (>= (+ (+ (* 69 ?y2) (* (- 80) ?y1)) (* 48 x1)) (- 77)) (and (not (= (+ (* (- 1) ?y2) (* (- 48) x1)) 0)) (not (= (+ (* 14 ?y1) (* (- 98) x1)) 83)))) (and (and (<= (+ (+ (* (- 95) ?y2) (* 34 ?y1)) (* (- 54) x1)) 51) (= (+ (+ (* 27 ?y2) (* (- 17) ?y1)) (* 75 x1)) 24)) (not (= (+ (* (- 96) ?y1) (* 90 x1)) (- 39))))))))
(check-sat)
(exit)
|
