test/regress/regress0/nl/issue3971.smt2


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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
(set-logic QF_NIA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const i12 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const v4 Bool)
(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))))
(declare-const v5 Bool)
(assert v1)
(declare-const i15 Int)
(declare-const v6 Bool)
(assert (distinct v5 (<= i8 i15)))
(declare-const i16 Int)
(assert v0)
(declare-const i17 Int)
(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)))
(declare-const i18 Int)
(declare-const v7 Bool)
(assert (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6))
(declare-const v8 Bool)
(declare-const v9 Bool)
(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)))
(assert (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))
(assert (=> v4 (<= i13 i6)))
(declare-const v10 Bool)
(declare-const v11 Bool)
(assert v9)
(check-sat)
(assert (> (abs i7) i4))
(assert v2)
(declare-const v12 Bool)
(assert (distinct v5 (<= i8 i15)))
(declare-const i19 Int)
(assert (xor (not (< (div i4 i8) 79)) (> (- 888) i15) (distinct i6 i12) (distinct i6 i12) (= (or v1 v3 v2) v1) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v10))
(check-sat)
(declare-const v13 Bool)
(push 1)
(assert (< i9 i8))
(assert (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8))
(push 1)
(push 1)
(declare-const v14 Bool)
(assert v7)
(assert v10)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const i20 Int)
(assert (or v1 v3 v2))
(declare-const i21 Int)
(declare-const v17 Bool)
(assert (=> (> i6 (abs 79)) (or (= (- i8) 36) v6 v1)))
(declare-const v18 Bool)
(assert (distinct i6 i12))
(declare-const v19 Bool)
(assert (< i9 i8))
(declare-const v20 Bool)
(assert (= v16 (>= i19 (abs i14)) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (<= i13 i6)))
(declare-const v21 Bool)
(declare-const v22 Bool)
(assert (> 79 34))
(declare-const i22 Int)
(assert v9)
(declare-const i23 Int)
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const i24 Int)
(pop 1)
(declare-const i25 Int)
(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))))
(declare-const v25 Bool)
(pop 1)
(declare-const v26 Bool)
(declare-const i26 Int)
(declare-const i27 Int)
(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1))
(push 1)
(assert (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4)))
(declare-const v27 Bool)
(declare-const v28 Bool)
(declare-const v29 Bool)
(declare-const i28 Int)
(assert (distinct v5 (<= i8 i15)))
(assert (xor (> (- 888) i15) v3 (< i9 i8) (=> v4 (<= i13 i6)) (>= 162 43) (and (>= 162 43) (distinct 623 752) (= i15 960)) (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4))))
(assert (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)))
(declare-const v30 Bool)
(assert (or (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v6 (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (>= 162 43) v30 (< (div i4 i8) 79) v2 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6)))
(assert (= (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) v28 v28))
(declare-const v31 Bool)
(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1))
(declare-const v32 Bool)
(pop 1)
(declare-const i29 Int)
(assert (xor v2 v2 v3 v0 v0 v2 v3 v1 v2))
(declare-const v33 Bool)
(assert v9)
(push 1)
(declare-const v34 Bool)
(assert (or (>= 162 43) (>= i14 i19) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79) (< i6 (div i4 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (or (not (< (div i4 i8) 79)) (> (abs i7) i4) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i9 i8) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v5))
(declare-const i30 Int)
(declare-const v35 Bool)
(push 1)
(assert (and (>= 162 43) (distinct 623 752) (= i15 960)))
(declare-const v36 Bool)
(assert (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))))
(push 1)
(declare-const v37 Bool)
(declare-const v38 Bool)
(assert (distinct (= v3 v4 (<= i13 i6) v0 v10 v6) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (> 546 i8) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i6 (div i4 i8)) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79)))
(assert (and (= v3 v4 (<= i13 i6) v0 v10 v6) (>= (abs 969) (* i6 162 i4 i4))))
(assert v0)
(assert (<= 12 i4))
(check-sat)
(assert (distinct (>= (abs 969) (* i6 162 i4 i4)) (xor (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (< (div i4 i8) 79) v11 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v4 (> 546 i8) (> i6 (abs 79)))))
(assert (=> (or (= (- i8) 36) v6 v1) (distinct v5 (<= i8 i15))))
(declare-const v39 Bool)
(push 1)
(declare-const v40 Bool)
(declare-const v41 Bool)
(declare-const v42 Bool)
(check-sat)
(assert (or (= (- i8) 36) v6 v1))
(assert (=> (=> v4 (<= i13 i6)) (< i6 (div i4 i8))))
(pop 1)
(declare-const v43 Bool)
(pop 1)
(assert (or v1 v3 v2))
(push 1)
(assert (not (> (abs i7) i4)))
(check-sat)
(exit)