blob: 907568d73d947f323435113b0236627cc8e98190 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(set-logic QF_AUFNIA)
(set-info :status unsat)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun a () (Array Int (Array Int Int)))
(declare-fun b () (Array Int (Array Int Int)))
(declare-fun c () (Array Int (Array Int Int)))
(declare-fun d () (Array Int (Array Int Int)))
(declare-fun e () (Array Int (Array Int Int)))
(declare-fun f () (Array Int (Array Int Int)))
(declare-fun g () (Array Int (Array Int Int)))
(declare-fun h () (Array Int (Array Int Int)))
(assert (not (= k 0)))
(assert (<= j k))
(assert (>= j k))
(assert (= b (store a j (store (select a j) 0 0))))
(assert (= d (store b 0 (store (select b 0) 0 (select (select d 0) 0)))))
(assert (<= i 0))
(assert (>= i (select (store (select d j) m 0) 0)))
(assert (not (= i 0)))
(check-sat)
(exit)
|
