blob: bf2d2a8c312413f8cb107f0a468a3c898a697da2 (
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
25
26
27
28
29
30
31
|
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(assert (or (not (<= (+ (* (- 24) x0 ) (* (- 15) x2 ) (* (- 18) x2 ) ) 2)) (not (< (+ (* (- 21) x2 ) (* 6 x2 ) ) (- 11))) (> (+ (* (- 3) x0 ) (* 8 x1 ) ) 11) ))
(assert (not (> (+ (* (- 4) x2 ) (* (- 23) x2 ) ) (- 26))) )
(assert (or (not (< (+ (* 35 x2 ) (* 40 x0 ) (* 38 x0 ) ) (- 4))) (not (<= (+ (* 46 x0 ) (* (- 16) x1 ) ) (- 44))) (> (+ (* 33 x2 ) (* (- 47) x2 ) (* (- 38) x0 ) ) 32) ))
(assert (or (<= (+ (* 49 x2 ) (* 42 x0 ) (* 36 x0 ) (* (- 15) x0 ) ) 41) (not (= (+ (* 5 x2 ) (* (- 2) x0 ) ) (- 23))) ))
(assert (or (< (+ (* 9 x1 ) (* (- 16) x1 ) (* 47 x2 ) (* 2 x0 ) ) (- 18)) (not (>= (+ (* 43 x0 ) (* (- 24) x1 ) ) (- 22))) (not (< (+ (* (- 37) x1 ) (* (- 27) x2 ) (* (- 40) x0 ) (* (- 34) x0 ) ) (- 42))) ))
(assert (or (not (<= (+ (* (- 26) x1 ) (* (- 20) x0 ) ) 26)) (<= (+ (* 24 x0 ) (* (- 40) x2 ) ) (- 50)) ))
(check-sat)
(push 1)
(assert (or (< (+ (* (- 23) x0 ) (* 25 x2 ) ) 47) (not (>= (+ (* (- 3) x0 ) (* 20 x1 ) (* (- 22) x0 ) ) 4)) (<= (+ (* (- 14) x0 ) (* 32 x2 ) (* 2 x0 ) (* 13 x1 ) ) (- 3)) ))
(assert (or (>= (+ (* (- 6) x0 ) (* (- 22) x2 ) ) (- 41)) (not (< (+ (* 26 x0 ) (* 15 x1 ) ) 6)) ))
(assert (<= (+ (* (- 14) x2 ) (* (- 39) x0 ) (* (- 31) x1 ) ) 24) )
(assert (or (> (+ (* (- 27) x2 ) (* (- 35) x1 ) ) (- 46)) (< (+ (* (- 41) x0 ) (* 46 x1 ) (* 16 x2 ) (* (- 31) x2 ) ) 29) (not (<= (+ (* (- 44) x2 ) (* 46 x0 ) (* (- 33) x1 ) ) (- 14))) ))
(check-sat)
(assert (not (>= (+ (* 23 x2 ) (* 5 x1 ) ) (- 16))) )
(assert (or (>= (+ (* (- 3) x0 ) (* 3 x1 ) (* 44 x0 ) ) (- 39)) (> (+ (* 28 x1 ) (* 26 x1 ) (* (- 22) x2 ) (* (- 36) x2 ) ) 27) (not (= (+ (* 16 x0 ) (* 41 x2 ) (* 16 x2 ) ) (- 47))) ))
(check-sat)
(pop 1)
(assert (not (<= (+ (* (- 28) x1 ) (* (- 11) x0 ) (* 9 x0 ) (* (- 4) x0 ) ) 23)) )
(assert (not (< (+ (* 16 x1 ) (* (- 18) x2 ) ) 34)) )
(assert (or (> (+ (* (- 41) x0 ) (* (- 12) x2 ) ) 11) (>= (+ (* 11 x1 ) (* 26 x0 ) (* 11 x1 ) (* 43 x1 ) ) 8) ))
(assert (or (> (+ (* 17 x2 ) (* (- 35) x2 ) ) 49) (not (= (+ (* 2 x0 ) (* 32 x1 ) (* 40 x1 ) (* 1 x0 ) ) (- 6))) (> (+ (* (- 18) x1 ) (* (- 40) x0 ) (* (- 40) x0 ) ) (- 36)) ))
(check-sat)
|
