sbv-7.5: SBVTestSuite/TestSuite/Queries/BadOption.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  TestSuite.Queries.BadOption
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Testing that a bad option setting is caught properly.
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}

module TestSuite.Queries.BadOption (tests)  where

import Data.SBV.Control
import qualified Control.Exception as C

import Utils.SBVTestFramework

-- Test suite
tests :: TestTree
tests =
  testGroup "Basics.QueryIndividual"
    [ goldenCapturedIO "query_badOption" $ \rf -> runSMTWith z3{verbose=True, redirectVerbose=Just rf} q
                                                  `C.catch`
                                                  (\(e::C.SomeException) -> appendFile rf ("\n" ++ show e))
    ]

q :: Symbolic ()
q = do _ <- sInteger "x"
       setOption $ OptionKeyword ":there-is-no-such-option" ["bad", "argument"]
       query $ return ()