blob: 549624f8b20147339909e561d8ba1ca5ad72634e (
plain)
1
2
3
4
5
6
7
8
9
10
|
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun v4 () Index)
(declare-fun v3 () Index)
(declare-fun v5 () Element)
(declare-fun v1 () (Array Index Element))
(check-sat-assuming ( (let ((_let_0 (store v1 v4 v5))) (let ((_let_1 (select _let_0 v3))) (distinct (ite (distinct _let_1 (select v1 v3)) v4 v3) (ite (= _let_1 (select (store _let_0 v4 v5) v3)) v3 v4)))) ))
|
