test/regress/regress0/arrays/x2.smtv1.smt2


1
2
3
4
5
6
7
8
9
10

(set-option :incremental false)
(set-info :status unsat)
(set-info :status unknown)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun a () Index)
(declare-fun S () (Array Index Element))
(declare-fun SS () (Array Index Element))
(check-sat-assuming ( (not (ite (= S SS) (= S (store SS a (select S a))) true)) ))