CVC4 type-error on array in nested struct

[nchong]

Checking the following program with --cvc4 results in an error: SMT2 solver returned error message: "expecting bit-vector terms". The program is verified (and fails, as expected) with MiniSat and Z3.

 struct S {
   char a[1];
 };
 struct {
   int i;
   struct S s;
 } x;
 int main() { __CPROVER_assert(0, ""); }

Looking at the smt2 file it seems the problem is the array a within the nested struct of x: it looks like concat is being applied to a function array.1.

 ; the following is a substitute for an array constructor
 (declare-fun array.1 () (Array (_ BitVec 64) (_ BitVec 8)))
 (assert (= (select array.1 (_ bv0 64)) (_ bv0 8)))
 ; set_to true (equal)
 (define-fun |x#1| () (_ BitVec 64) (concat (_ bv0 24) (concat array.1 (_ bv0 32))))

[TGWDB]

Fixed in #6205