test/regress/regress0/bug639.smt2

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