blob: d8252e3e44208530b8c66c653d18afbbb043b6ca (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun v0 () (Array Index Element))
(declare-fun v1 () (Array Index Element))
(declare-fun v2 () Index)
(declare-fun v3 () Element)
(declare-fun v4 () Element)
(check-sat-assuming ( (let ((_let_0 (distinct v0 v0))) (let ((_let_1 (distinct v0 v1))) (let ((_let_2 (distinct v2 v2))) (let ((_let_3 (distinct v3 v4))) (let ((_let_4 (ite _let_1 (ite _let_2 (ite _let_0 v1 v1) v0) v0))) (let ((_let_5 (ite _let_3 v1 v0))) (let ((_let_6 (ite _let_0 (ite _let_3 v2 v2) (ite _let_2 (ite _let_3 v2 v2) (ite _let_3 v2 v2))))) (let ((_let_7 (ite _let_3 (ite _let_2 v3 v4) v3))) (let ((_let_8 (ite _let_1 v3 v4))) (let ((_let_9 (ite _let_3 _let_7 v4))) (let ((_let_10 (ite _let_0 (ite _let_1 _let_8 (ite _let_2 v3 v4)) _let_9))) (let ((_let_11 (or (ite (= _let_5 (store (ite _let_0 v1 v1) (ite _let_1 v2 (ite _let_3 v2 v2)) _let_10)) (= _let_4 _let_5) (or (= (= (ite _let_3 v2 v2) v2) (= (ite _let_1 _let_8 (ite _let_2 v3 v4)) _let_10)) (= v4 (ite _let_1 _let_8 (ite _let_2 v3 v4))))) (= (= (=> (= (ite _let_1 _let_8 (ite _let_2 v3 v4)) (ite _let_1 _let_8 (ite _let_2 v3 v4))) (distinct _let_6 (ite _let_2 v2 (ite _let_3 v2 v2)))) (= (= _let_9 _let_7) (= (distinct _let_8 (select _let_4 _let_6)) _let_3))) _let_1)))) (and (and (or (and (distinct v2 (ite _let_1 v2 (ite _let_3 v2 v2))) (or (xor (distinct (ite _let_2 (ite _let_0 v1 v1) v0) v1) (distinct v4 (ite _let_2 v3 v4))) _let_0)) (ite (= (ite _let_0 v1 v1) v1) (=> (xor (xor (= _let_5 _let_4) (= _let_9 _let_10)) (= (distinct _let_9 (ite _let_1 _let_8 (ite _let_2 v3 v4))) (= v0 (ite _let_0 v1 v1)))) (not (distinct (ite _let_1 v2 (ite _let_3 v2 v2)) (ite _let_2 (ite _let_3 v2 v2) (ite _let_3 v2 v2))))) (ite (=> (not _let_2) (distinct v4 v3)) (= _let_10 _let_8) (= _let_4 _let_4)))) (distinct _let_10 v4)) (= _let_11 _let_11)))))))))))))) ))
|
