Arrays and structs appear to be working.  But ACL2 struggles with two array loops in one function.