(rewriter.expand_nested_stores) assertion violation at ../src/smt/smt_internalizer.cpp:378

[rainoftime]

Hi, for the following formula,

(set-option :rewriter.expand_nested_stores true)
(declare-datatypes ((x5 0)) (((x3) (x4))))
(declare-sort x31)
(declare-datatypes ((x36 0)) (((x35))))
(declare-sort x6)
(declare-datatypes ((x29 0)) (((x28 (x23 x5)))))
(declare-sort x30)
(declare-datatypes ((x45 0)) (((x44 (x38 x5) (x39 x6) (x40 x6) (x41 x6) (x42 x36) (x43 x31)))))
(declare-fun x63 () x30)
(declare-fun x70 () (Array x30 x45))
(declare-fun x68 () (Array x30 x45))
(declare-fun z3name!0 (x30) x29)
(declare-fun l51 () Bool)
(assert (= l51 (forall ((x73 x30)) (or (= x3 (x23 (z3name!0 x73))) (= x3 (x38 (select x70 x73)))))))
(assert (not (= x70 (store x70 x63 (x44 x4 (x39 (select x70 x63)) (x40 (select x70 x63)) (x41 (select x70 x63)) (x42 (select x70 x63)) (x43 (select x70 x63)))))))
(assert (not (= x70 x68)))
(check-sat-assuming (l51))

z3 4f6fcf8

ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 378
!gate_ctx
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB