rewriter.expand_nested_stores Assertion violation at ../src/ast/rewriter/rewriter_def.h Line: 49

[muchang]

Hi,
For this formula:

(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)

Z3 throws out an assertion violation:

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

OS: Ubuntu 18.04
Commit: 5c9fd90