(set-option :rewriter.expand_nested_stores true)
(declare-fun a (Int Int Int Int Int Int (Array Int (Array Int Int))
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int (Array Int Int) (Array Int
Int) Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int (Array Int Int) (Array Int Int) (Array Int (Array
Int Int)) Int Int Int Int Int Int Int Int (Array Int (Array Int Int))
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int (Array Int Int) Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int (Array Int Int) Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
Int Int Int Int Bool) Bool)
(assert (forall ((c Int) (d Int) (aa Int) (e Int) (f Int) (ab Int) (ac
(Array Int (Array Int Int))) (g Int) (h Int) (i Int) (j Int) (k Int)
(l Int) (m Int) (n Int) (o Int) (p Int) (q Int) (r Int) (s Int) (t
Int) (u Int) (v Int) (w Int) (x Int) (y Int) (z Int) (ad Int) (ae Int)
(af (Array Int Int)) (ag (Array Int Int)) (ah Int) (ai Int) (aj Int)
(ak Int) (al Int) (am Int) (an Int) (ao Int) (ap Int) (aq Int) (ar
Int) (as Int) (ay Int) (at Int) (au Int) (av Int) (aw Int) (ax (Array
Int Int)) (bi (Array Int Int)) (az (Array Int (Array Int Int))) (ba
Int) (bb Int) (bc Int) (bd Int) (be Int) (bf Int) (bg (Array Int
(Array Int Int))) (bh Int) (bn Int) (bj Int) (bk Int) (bl Int) (bm
Int) (bs Int) (bo Int) (bp Int) (bq Int) (br Int) (bx Int) (bt Int)
(bu Int) (bv Int) (bw Int) (cg Int) (by Int) (bz Int) (ca Int) (cb
Int) (cc Int) (cd Int) (ce Int) (cf Int) (cq (Array Int Int)) (ch Int)
(ci Int) (cj Int) (ck Int) (cl Int) (cm Int) (do Int) (cn Int) (co
Int) (cp Int) (db Int) (cr Int) (cs Int) (ct Int) (cu Int) (cv Int)
(cw Int) (cx Int) (cy Int) (cz Int) (da Int) (dr Int) (dc Int) (dd
Int) (de Int) (dw Int) (df Int) (dg Int) (dh Int) (di Int) (dj Int)
(dk Int) (dl Int) (dm Int) (dn Int) (dp Int) (dq Int) (en Int) (ds
Int) (dt Int) (du Int) (dv Int) (es Int) (dx Int) (dy Int) (dz Int)
(ea Int) (eb Int) (ec Int) (ed Int) (ee Int) (ef Int) (eg Int) (eh
Int) (ei Int) (ej Int) (ek Int) (el Int) (em Int) (gr Int) (eo Int)
(ep Int) (eq Int) (er Int) (ft Int) (et Int) (eu Int) (ev Int) (ew
Int) (ex Int) (ey Int) (ez Int) (fa Int) (fb Int) (fc Int) (fd Int)
(fe Int) (ff Int) (fg Int) (fh Int) (fi Int) (fj Int) (fk Int) (fl
Int) (fm Int) (fn Int) (fo Int) (gq Int) (fp Int) (fq Int) (fr Int)
(fs Int) (gv Int) (fu Int) (gx Int) (fv Int) (fw Int) (fx Int) (if
(Array Int Int)) (fy Int) (fz Int) (ga Int) (gb Int) (gc Int) (gd Int)
(ge Int) (gf Int) (gg Int) (gh Int) (gi Int) (gj Int) (gk Int) (gl
Int) (gm Int) (gn Int) (go Int) (gp Int) (ht Int) (hu Int) (gs Int)
(gt Int) (gu Int) (hy Int) (gw Int) (ia Int) (gy Int) (gz Int) (ha
Int) (hb Int) (hc Int) (hd Int) (he Int) (hf Int) (hg Int) (hh Int)
(hi Int) (hj Int) (hk Int) (hl Int) (hm Int) (hn Int) (ho Int) (hp
Int) (hq Int) (hr Int) (hs Int) (ip Int) (iq Int) (hv Int) (hw Int)
(hx Int) (ir Int) (hz Int) (is Int) (ib Int) (ic Int) (id Int) (ie
Int) (ig Int) (ih Int) (ii Int) (ij Int) (ik Int) (il Bool) (im (Array
Int Int))) (and (or (let ((in 0)) (= cq (let ((io (bg gq))) (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
im 0 0) 1 0) 2 0) 3 0) 4 0) 5 0) 6 0) 7 0) 8 0) 9 0) 0 0) 1 0) 2 0) 3
0) 4 0) 5 0) 6 0) 7 0) 8 0) 9 0) 0 0) 1 0) 2 0) 3 0) 4 0) 5 0) 6 0) 7
0) 8 0) 9 0) 0 0) 1 0) 2 0) 3 0) 4 0) 5 0) 6 0) 7 0) 8 0) 9 0) 0 (io
in)))))) (a c d aa e f ab ac g h i j k l m n o d p q r e s f t d u v w
x y z e f ad ae af ag ah ai aj ak al am an ao ap aq ar as ay at au av
c d e f aw ax bi az ba e f bb bc bd be bf bg bh bn bj bk bl bm bs bo
bp c d e f bq br bx bt bu c bv bw c d e f cg by c bz ca cb c cc cd ce
c d e cf cq ch ci cj c ck d cl cm do cn co cp db c d d e cr f cs ct cu
c d e f cv cw d cx cy e cz da dr dc dd d de dw e df dg dh di dj c d c
d e f e f dk dl dm f dn dp e dq en ds dt du dv f es dx e dy dz ea eb
ec ed ee c d e f ef eg eh ei ej f ek el em gr eo ep eq er ft f et eu
ev ew ex ey ez fa fb fc fd fe ff fg fh fi fj fk fl fm fn fo gq fp fq
fr fs gv fu gx fv fw fx if fy fz ga gb gc gd ge gf gg gh gi gj gk gl
gm gn go gp ht hu gs gt gu hy gw ia gy gz ha hb hc hd he hf hg hh hi
hj hk hl hm hn ho hp hq hr hs ip iq hv hw hx ir hz is ib ic id ie ig
ih ii ij ik il)))
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 49
v->get_sort() == m().get_sort(r)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB