Multiple dynamic array parameters

Hi, I'm having difficulty verifying this program using the following eDSL:

pragma solidity 0.4.24;

contract simple15 {

    function getLength(uint[] xarr, uint[] zarr) pure external returns (uint) {
        return zarr.length;
    }
}

[getLength]
k: (#execute => #halt) ~> _
statusCode: _ => EVMC_SUCCESS
output: _ => #encodeArgs(#uint256(Z_LEN))
log: _
callStack: _
this: #CONTRACT_ID
msg_sender: MSG_SENDER
callData:  #abiCallData("getLength", (#array(#uint256(_), X_LEN, _), #array(#uint256(_), Z_LEN, _)))
callValue: 0
wordStack: .WordStack => _
localMem: .Map => _
pc: 0 => _
gas: #gas(INITGAS, 0, 0) => _
memoryUsed: 0 => _
refund: _
coinbase: _ => _
+requires:  andBool #range(0 <= CD < 1024)
            andBool #rangeAddress(MSG_SENDER)
            andBool #rangeUInt(256, X_LEN)
            andBool #rangeUInt(256, Z_LEN)

Interestingly, if I modify the code to return xarr.length instead of zarr.length (i.e. the length of the first dynamic array parameter instead of the second dynamic array parameter), the spec actually passes successfully (once the output cell is updated to output: _ => #encodeArgs(#uint256(X_LEN)). This seems to suggest that something may be missing from the spec or rewrite rules to handle extracting the length of a dynamic array parameter which is preceded by another dynamically-size array.
I looked at the edsl.k file, and I couldn't figure out how the following rewrite rule would work:

rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) ++ #encodeArgs(DATA)

especially when compared to the similar rule for #enc(#bytes(WS)) which seems to "bottom-out" rather than recursively encoding WS via #encodeArgs:

rule #enc(#bytes(WS)) => #encBytes(#sizeWordStack(WS), WS)
rule #encBytes(N, WS) => #enc(#uint256(N)) ++ WS ++ #buf(#ceil32(N) -Int N, 0) 

Is there something missing from my spec?

Reproduce the Solidity example and its eDSL specification, then inspect edsl.k, especially the #enc rule for #array and the related #bytes rules. Determine why zarr.length is not verified when another dynamic array precedes it; done means the specification verifies the second array's length or the missing rewrite behavior is clearly resolved.