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