blob: 2e50030d1a5b7a15dd42045dc5c1082645e8f27d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
; COMMAND-LINE: --full-saturate-quant
; EXPECT: unsat
(set-logic LRA)
(set-info :status unsat)
(declare-fun x4 () Real)
(declare-fun x3 () Real)
(assert (forall ((?lambda Real))
(let ((?v_26 (* (- 1) x4)))
(let ((?v_28 (+ ?lambda (* (/ 3 40) x4))))
(and
(<= (+ ?lambda (* (/ 1 60) x4)) (/ 400 3))
(<= (+ (* (- 1) ?lambda) (* (/ (- 1) 60) x4)) (/ (- 731) 6))
(<= ?v_28 610)
(<= ?v_28 359)
(<= ?v_26 (- 4100))
(<= ?v_26 (- 4500))
(<= ?v_26 (- 4910))
))
)))
(check-sat)
(exit)
|
