blob: 3b7ddbcf3eb5a1d53d9f3b704b54ffd73c784805 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
; EXPECT: false
; EXIT: 0
(set-logic LIA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun v15 () Bool)
(declare-fun v16 () Bool)
(declare-fun i0 () Int)
(declare-fun i2 () Int)
(declare-fun i9 () Int)
(declare-fun v26 () Bool)
(declare-fun v33 () Bool)
(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0)))
|
