test/regress/regress0/auflia/a17.smt


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

(benchmark fuzzsmt
:logic QF_AUFLIA
:extrafuns ((a Array))
:extrafuns ((x1 Int))
:extrafuns ((y1 Int))
:extrafuns ((z0 Int))
:extrapreds ((p Array))
:status sat
:formula
(and
     (>= (select (store a (+ x1 z0) 1) x1) 1)
     (p a)
     (p (store a (+ x1 z0) 1))
     (p (store (store a (+ x1 z0) 1) y1 1))
     (>= x1 1)
     (>= z0 0)
     (<= z0 0)
     (<= y1 1)
     (>= y1 1)
)
)