content: -----------------------------------------------------------------------------
  -- |
  -- Module    : TestSuite.Queries.ArrayGetVal
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Making sure array get-value works, since we might send extra asserts after
  -- check-sat.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE ScopedTypeVariables #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module TestSuite.Queries.ArrayGetVal (tests)  where
  
  import Data.SBV.Control
  
  import Utils.SBVTestFramework
  
  -- Test suite
  tests :: TestTree
  tests =
    testGroup "Basics.ArrayGetVal"
      [ goldenCapturedIO "arrayGetValTest1" testQuery
      ]
  
  testQuery :: FilePath -> IO ()
  testQuery rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t1
                    appendFile rf ("\n FINAL:" ++ show r ++ "\nDONE!\n")
  
  t1 :: Symbolic Integer
  t1 = do a :: SArray Integer Integer <- sArray "a"
          query $ do ensureSat
                     getValue (readArray (writeArray a 1 2) 1)
  