Error: block size must be a multiple of size

[yuzeng2333]

I am doing a simple experiment with arrays in c. The c code is:

`int vec0[5];

int vec_func(int num) { vec0[0] = 1; vec0[1] = 2; vec0[2] = 3; vec0[3] = 4; vec0[4] = 5;

return vec0[num]; }`

And here is the partial code for checking:

`(define (check-vec) (parameterize ([llvm:current-machine (llvm:make-machine cpp:symbols cpp:globals)])

; symbolic inputs
(define-symbolic num (bitvector 32))

; symbolic result
(define r (cpp:@vec_func num))

(define sol
  (solve
   (begin
     (assume (bvsle num 5))
     (assert (not equal? r 3))
    )
  )
)
sol

))

` But when I ran the checking, an error is reported:

[assert] ~/serval/serval/lib/memory/mblock.rkt:254 mcell-path: block size (bv #x0000000000000001 64) must be a multiple of size (bv #x0000000000000004 64)

I am writing and reading int from the array, so the block size should be 4 byte. why the error says block size is #x0000000000000001? It seems the "element-size" in mblock.rkt has some problem: it always returns 1 for the integer array, even though its element type is int.

Update: I just find the same error happens for provided array.c in the test folder.