module Main where
import Data.SBV
import Data.SBV.Control
import Control.Monad

t :: Symbolic (Int -> SReal)
t = do
    x <- sReal "prob"
    return $ \y -> if y == 2 then x else 1.0


q :: Symbolic ()
q = do
    f <- t
    query $ do
        cs <- checkSat
        case cs of
          Sat -> do
            v <- getValue (f 1)
            return ()



main :: IO ()
main = do
  runSMTWith z3{verbose=True} q