output

λ> main
Sat
SMTModel {modelObjectives = [], modelAssocs = [("arg1",5 :: Integer),("arg2",True :: Bool)]}

sbv-array-tup.hs

type STupArray a b c = (SArray a b, SArray a c)

newArrayTup
  :: (HasKind a, HasKind b, HasKind c) => String -> Symbolic (STupArray a b c)
newArrayTup str = (,) <$> newArray (str ++ "1") <*> newArray (str ++ "2")

writeArrayTup
  :: (SymWord b, SymWord c)
  => STupArray a b c
  -> SBV a
  -> (SBV b, SBV c)
  -> STupArray a b c
writeArrayTup (arr1, arr2) k (v1, v2)
  = (writeArray arr1 k v1, writeArray arr2 k v2)

readArrayTup :: STupArray a b c -> SBV a -> (SBV b, SBV c)
readArrayTup (arr1, arr2) k = (readArray arr1 k, readArray arr2 k)

main :: IO ()
main = runSMT $ do
  arr <- newArrayTup @Integer @Integer @Bool "arr"
  t <- (,) <$> sInteger "arg1" <*> sBool "arg2"
  let arr' = writeArrayTup arr 1 t

  constrain $ readArrayTup arr' 1 .== (5, true)
  constrain $ readArrayTup arr' 2 .== (6, false)

  query $ do
    cs <- checkSat
    mod <- getModel

    io $ do
      print cs
      print mod