CVC4 backend fails to parse `groundEval` of `Int`-indexed array (`array select not indexed with correct type for array`)

This program, when run with what4 at commit 629f9f1:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Main where

import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Nonce as N
import qualified Data.Parameterized.Some as Some
import qualified System.IO as IO
import qualified What4.Config as WC
import qualified What4.Expr as WE
import qualified What4.Expr.Builder as WEB
import qualified What4.Expr.GroundEval as WEG
import qualified What4.Interface as WI
import qualified What4.Solver as WS

opts :: [WC.ConfigDesc]
opts = WS.cvc4Options

adapter :: WS.SolverAdapter st
adapter = WS.cvc4Adapter

main :: IO ()
main = do
  Some.Some ng <- N.newIONonceGenerator
  sym <- WEB.newExprBuilder WEB.FloatIEEERepr WE.EmptyExprBuilderState ng
  WC.extendConfig opts (WI.getConfiguration sym)

  let w = WI.knownNat @64
  arr <- WI.freshConstant sym (WI.safeSymbol "arr")
           (WI.BaseArrayRepr (Ctx.Empty Ctx.:> WI.BaseIntegerRepr)
                             (WI.BaseBVRepr w))
  idxInt <- WI.intLit sym 0
  let idx = Ctx.Empty Ctx.:> idxInt
  elt <- WI.arrayLookup sym arr idx
  p <- WI.bvIsNonzero sym elt
  WS.solver_adapter_check_sat adapter sym
    WS.defaultLogData{WS.logHandle = Just IO.stdout} [p] $ \_result ->
    case _result of
      WS.Sat (ge, _) -> do
        putStrLn "Satisfiable, with model:"
        v <- WEG.groundEval ge =<< WI.arrayLookup sym arr idx
        print v
      WS.Unsat _ -> putStrLn "Unsatisfiable."
      WS.Unknown -> putStrLn "Solver failed to find a solution."

Will fail with the following error message:

(set-logic ALL_SUPPORTED)
(set-option :produce-models true)
; :1:0
(declare-fun arr () (Array Int (_ BitVec 64)))
(define-fun x!0 () (_ BitVec 64) (select arr 0))
(define-fun x!1 () Bool (= (_ bv0 64) x!0))
(define-fun x!2 () Bool (not x!1))
(assert x!2)
(check-sat)
; sat
Satisfiable, with model:
(get-value ((select arr 0.0)))
; (error "Parse Error: <stdin>:9.28: array select not indexed with correct type for array")
*** Exception: Solver reported an error:
  Parse Error: <stdin>:9.28: array select not indexed with correct type for array
in response to command:
  (get-value ((select arr 0.0)))

What's more, this error message appears to be exclusive to the CVC4 backend. If I run this with the Z3 backend or Yices backend (by changing the values of opts and adapter accordingly), then it succeeds. For example, here is the output with the Z3 backend:

(set-option :produce-models true)
(set-option :pp.decimal true)
; :1:0
(declare-datatypes (T0) ((Struct1 (mk-struct1 (struct1-proj0 T0)))))
(declare-fun arr () (Array Int (_ BitVec 64)))
(define-fun x!0 () (_ BitVec 64) (select arr 0))
(define-fun x!1 () Bool (= (_ bv0 64) x!0))
(define-fun x!2 () Bool (not x!1))
(assert x!2)
(check-sat)
; sat
Satisfiable, with model:
(get-value ((select arr 0.0)))
; (((select arr 0.0) #xffffffffffffffff))
BV 18446744073709551615
(exit)

I suspect the issue is this line:

what4/what4/src/What4/Protocol/SMTWriter.hs

Line 3003 in 537b609

IntegerTypeMap -> rationalTerm (fromInteger v)

This is converting an Integer to a rationalTerm, and the SMTLib writer renders rational literals with decimals, causing intLit sym 0 to be rendered as 0.0. If I change that line to the following:

diff --git a/what4/src/What4/Protocol/SMTWriter.hs b/what4/src/What4/Protocol/SMTWriter.hs
index 3168a750..c9c5462c 100644
--- a/what4/src/What4/Protocol/SMTWriter.hs
+++ b/what4/src/What4/Protocol/SMTWriter.hs
@@ -3000,7 +3000,7 @@ smtIndicesTerms tps vals = Ctx.forIndexRange 0 sz f []
         f i l = (r:l)
          where GVW v = vals Ctx.! i
                r = case tps Ctx.! i of
-                      IntegerTypeMap -> rationalTerm (fromInteger v)
+                      IntegerTypeMap -> integerTerm v
                       BVTypeMap w -> bvTerm w v
                       _ -> error "Do not yet support other index types."

Then the 0.0 is rendered as 0, causing the issue to go away. I'm not sure if this has any other adverse consequences, however. All of the what4 test suites continue to pass with this change, at the very least.

Yeah, weird that it was ever rendered as a rational term. That seems like the right fix to me.