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