Soundness bugs in arrays + reals/ints (no option)

[rainoftime]

Hi,
For this formula:
137.txt

CVC4 throws out a fatal failure:

Fatal failure within void CVC4::theory::arrays::ArrayInfo::addIndex(CVC4::Node, CVC4::TNode) at /home/CVC4/src/theory/arrays/array_info.cpp:137
Check failure

 !i.getType().isArray()

OS: Ubuntu 16.04
Commit: 2f8caab

[nafur]

A smaller example:

(declare-const a (Array Bool Bool))
(declare-const b (Array (Array Bool Bool) Int))
(assert (= b (store b a 0)))
(check-sat)

Note the comment after the assertion:

Assert(!i.getType().isArray());  // temporary for flat arrays

[rainoftime]

(set-logic QF_AUFLIRA)
(declare-fun _substvar_191_ () (Array (Array Bool Bool) (Array Bool Bool)))
(declare-const v2 Bool)
(declare-const arr0 (Array Bool Bool))
(declare-const arr1 (Array (Array Bool Bool) (Array Bool Bool)))
(assert (= arr1 (store arr1 (store arr0 false v2) arr0) _substvar_191_ arr1))
(push 1)
(assert v2)
(assert (= false false false false (= arr1 arr1 (store arr1 (store arr0 false v2) arr0) arr1) false))
(check-sat)