multi-dimensional array type mismatch for CVC4 backend

The short program below, which simply creates a fresh array and indexes into it, crashes. The error message from CVC4 is:

  Parse Error: <stdin>:4.47: array select not indexed with correct type for array

Here's the program:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
import qualified Data.Parameterized.Nonce as N
import qualified Data.Parameterized.Context as C
import qualified Lang.Crucible.Backend.Simple as CB
import qualified Lang.Crucible.CFG.Core as CC
import qualified What4.Config as WC
import qualified What4.Expr.Builder as W4B
import qualified What4.Interface as W4
import qualified What4.Solver as WS

main :: IO ()
main = do
    CC.Some gen <- N.newIONonceGenerator
    sym <- CB.newSimpleBackend W4B.FloatRealRepr gen
    WC.extendConfig WS.cvc4Options (W4.getConfiguration sym)
    f <- W4.freshConstant sym (W4.safeSymbol "x")
        (W4.BaseArrayRepr
            (C.Empty C.:> W4.BaseBoolRepr C.:> W4.BaseBoolRepr)
            W4.BaseBoolRepr
        )
    p <- W4.arrayLookup sym f (C.Empty C.:> W4.truePred sym C.:> W4.truePred sym)
    WS.solver_adapter_check_sat WS.cvc4Adapter sym WS.defaultLogData [p] (\_ -> return ())

The SMTlib that it produces and passes on to CVC4 looks like this:

(set-logic ALL_SUPPORTED)
(set-option :produce-models true)
; :1:0
(declare-fun x () (Array (Tuple Bool Bool) Bool))
(define-fun x!0 () Bool (select (select x true) true))
(assert x!0)
(check-sat)

It looks like the array declaration code is thinking of multi-dimensional arrays as arrays indexed by a tuple, while the indexing code is thinking of them as nested arrays.

GaloisInc / what4

multi-dimensional array type mismatch for CVC4 backend #138