content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Grisette.Backend.LoweringTests (loweringTests) where
  
  import Control.Monad.Trans (MonadIO (liftIO), MonadTrans (lift))
  import Data.Bits
    ( Bits (complement, xor, (.&.), (.|.)),
    )
  import Data.Dynamic (Typeable, fromDynamic)
  import Data.Either (isRight)
  import qualified Data.HashMap.Strict as M
  import Data.Proxy (Proxy (Proxy))
  import qualified Data.SBV as SBV
  import qualified Data.SBV.Control as SBV
  import qualified Data.Text as T
  import GHC.Stack (HasCallStack)
  import Grisette
    ( AsKey (AsKey),
      EvalSym (evalSym),
      FP,
      FPRoundingMode,
      Function ((#)),
      IntN,
      LogicalOp ((.&&)),
      Solvable (con),
      SymEq ((.==)),
      SymInteger,
      SymRep (SymType),
      WordN,
      solve,
      type (-~>),
      type (=~>),
    )
  import Grisette.Internal.Backend.QuantifiedStack
    ( emptyQuantifiedStack,
    )
  import Grisette.Internal.Backend.Solving
    ( GrisetteSMTConfig (sbvConfig),
      lowerSinglePrim,
      lowerSinglePrimCached,
      z3,
    )
  import Grisette.Internal.Backend.SymBiMap
    ( SymBiMap (biMapToSBV),
    )
  import Grisette.Internal.Core.Data.Class.AsKey (KeyEq)
  import Grisette.Internal.SymPrim.AlgReal (AlgReal)
  import Grisette.Internal.SymPrim.FP (FP32)
  import Grisette.Internal.SymPrim.Prim.SomeTerm
    ( SomeTerm (SomeTerm),
    )
  import Grisette.Internal.SymPrim.Prim.Term
    ( FPTrait
        ( FPIsInfinite,
          FPIsNaN,
          FPIsNegative,
          FPIsNegativeInfinite,
          FPIsNegativeZero,
          FPIsNormal,
          FPIsPoint,
          FPIsPositive,
          FPIsPositiveInfinite,
          FPIsPositiveZero,
          FPIsSubnormal,
          FPIsZero
        ),
      FloatingUnaryOp
        ( FloatingAcos,
          FloatingAsin,
          FloatingAtan,
          FloatingCos,
          FloatingCosh,
          FloatingSin,
          FloatingSinh,
          FloatingTan,
          FloatingTanh
        ),
      SBVRep (SBVType),
      SupportedPrim,
      Term,
      TypedConstantSymbol,
      absNumTerm,
      addNumTerm,
      andBitsTerm,
      andTerm,
      bitCastOrTerm,
      bitCastTerm,
      bvConcatTerm,
      bvSelectTerm,
      bvsignExtendTerm,
      bvzeroExtendTerm,
      complementBitsTerm,
      conTerm,
      divIntegralTerm,
      eqTerm,
      existsTerm,
      fdivTerm,
      floatingUnaryTerm,
      forallTerm,
      fpTraitTerm,
      iteTerm,
      leOrdTerm,
      ltOrdTerm,
      modIntegralTerm,
      mulNumTerm,
      negNumTerm,
      notTerm,
      orBitsTerm,
      orTerm,
      pevalAndTerm,
      pevalFPTraitTerm,
      pevalNotTerm,
      quotIntegralTerm,
      recipTerm,
      remIntegralTerm,
      rotateLeftTerm,
      rotateRightTerm,
      shiftLeftTerm,
      shiftRightTerm,
      signumNumTerm,
      ssymTerm,
      xorBitsTerm,
    )
  import Test.Framework (Test, TestOptions' (topt_timeout), plusTestOptions, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit (Assertion, assertBool, assertFailure, (@?=))
  import Test.QuickCheck (Arbitrary, ioProperty)
  import Type.Reflection (typeRep)
  
  testUnaryOpLowering ::
    forall a b as.
    ( HasCallStack,
      SupportedPrim a,
      SBV.EqSymbolic (SBVType b),
      Typeable (SBVType a),
      SBV.SymVal as,
      SBVType a ~ SBV.SBV as,
      Show as
    ) =>
    GrisetteSMTConfig ->
    (Term a -> Term b) ->
    String ->
    (SBVType a -> SBVType b) ->
    Assertion
  testUnaryOpLowering = testUnaryOpLowering' Nothing
  
  testUnaryOpLowering' ::
    forall a b as.
    ( HasCallStack,
      SupportedPrim a,
      SBV.EqSymbolic (SBVType b),
      Typeable (SBVType a),
      SBV.SymVal as,
      SBVType a ~ SBV.SBV as,
      Show as
    ) =>
    (Maybe (SBVType a -> SBVType Bool)) ->
    GrisetteSMTConfig ->
    (Term a -> Term b) ->
    String ->
    (SBVType a -> SBVType b) ->
    Assertion
  testUnaryOpLowering' precond config f name sbvfun = do
    let a :: Term a = ssymTerm "a"
    let fa :: Term b = f a
    SBV.runSMTWith (sbvConfig config) $ do
      (m, lt, _) <- lowerSinglePrim fa
      let sbva :: Maybe (SBVType a) =
            M.lookup (SomeTerm a) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      case sbva of
        Nothing -> lift $ assertFailure "Failed to extract the term"
        Just sbvav -> SBV.query $ do
          SBV.constrain $ lt emptyQuantifiedStack SBV..== sbvfun sbvav
          satres <- SBV.checkSat
          case satres of
            SBV.Sat -> return ()
            _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unsolvable formula"
    SBV.runSMTWith (sbvConfig config) $ do
      (m, lt, _) <- lowerSinglePrim fa
      let sbvv :: Maybe (SBVType a) =
            M.lookup (SomeTerm a) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      case sbvv of
        Nothing -> lift $ assertFailure "Failed to extract the term"
        Just sbvvv -> SBV.query $ do
          case precond of
            Just p -> SBV.constrain $ p sbvvv
            Nothing -> return ()
          SBV.constrain $ lt emptyQuantifiedStack SBV../= sbvfun sbvvv
          r <- SBV.checkSat
          case r of
            SBV.Sat -> do
              counterExample <- SBV.getValue sbvvv
              lift $ assertFailure $ "Translation counter example found: " ++ show counterExample
            SBV.Unsat -> return ()
            _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"
  
  testBinaryOpLowering ::
    forall a b c as bs.
    ( HasCallStack,
      SupportedPrim a,
      SupportedPrim b,
      SBV.EqSymbolic (SBVType c),
      Typeable (SBVType a),
      Typeable (SBVType b),
      SBV.SymVal as,
      SBV.SymVal bs,
      Show as,
      Show bs,
      SBVType a ~ SBV.SBV as,
      SBVType b ~ SBV.SBV bs
    ) =>
    GrisetteSMTConfig ->
    (Term a -> Term b -> Term c) ->
    String ->
    (SBVType a -> SBVType b -> SBVType c) ->
    Assertion
  testBinaryOpLowering config f name sbvfun = do
    let a :: Term a = ssymTerm "a"
    let b :: Term b = ssymTerm "b"
    let fab :: Term c = f a b
    SBV.runSMTWith (sbvConfig config) $ do
      (m, lt, _) <- lowerSinglePrim fab
      let sbva :: Maybe (SBVType a) =
            M.lookup (SomeTerm a) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      let sbvb :: Maybe (SBVType b) =
            M.lookup (SomeTerm b) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      case (sbva, sbvb) of
        (Just sbvav, Just sbvbv) -> SBV.query $ do
          SBV.constrain $ lt emptyQuantifiedStack SBV..== sbvfun sbvav sbvbv
          satres <- SBV.checkSat
          case satres of
            SBV.Sat -> return ()
            _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unsolvable formula"
        _ -> lift $ assertFailure "Failed to extract the term"
    SBV.runSMTWith (sbvConfig config) $ do
      (m, lt, _) <- lowerSinglePrim fab
      let sbva :: Maybe (SBVType a) =
            M.lookup (SomeTerm a) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      let sbvb :: Maybe (SBVType b) =
            M.lookup (SomeTerm b) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      case (sbva, sbvb) of
        (Just sbvav, Just sbvbv) -> SBV.query $ do
          SBV.constrain $ lt emptyQuantifiedStack SBV../= sbvfun sbvav sbvbv
          r <- SBV.checkSat
          case r of
            SBV.Sat -> do
              counterExampleA <- SBV.getValue sbvav
              counterExampleB <- SBV.getValue sbvbv
              lift $ assertFailure $ "Translation counter example found: " ++ show (counterExampleA, counterExampleB)
            SBV.Unsat -> return ()
            _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"
        _ -> lift $ assertFailure "Failed to extract the term"
  
  testTernaryOpLowering ::
    forall a b c d as bs cs.
    ( HasCallStack,
      SupportedPrim a,
      SupportedPrim b,
      SupportedPrim c,
      SBV.EqSymbolic (SBVType d),
      Typeable (SBVType a),
      Typeable (SBVType b),
      Typeable (SBVType c),
      SBV.SymVal as,
      SBV.SymVal bs,
      SBV.SymVal cs,
      Show as,
      Show bs,
      Show cs,
      SBVType a ~ SBV.SBV as,
      SBVType b ~ SBV.SBV bs,
      SBVType c ~ SBV.SBV cs
    ) =>
    GrisetteSMTConfig ->
    (Term a -> Term b -> Term c -> Term Bool) ->
    (Term a -> Term b -> Term c -> Term d) ->
    T.Text ->
    (SBVType a -> SBVType b -> SBVType c -> SBVType d) ->
    Assertion
  testTernaryOpLowering config precond f name sbvfun = do
    let a :: Term a = ssymTerm "a"
    let b :: Term b = ssymTerm "b"
    let c :: Term c = ssymTerm "c"
    let fabc :: Term d = f a b c
    SBV.runSMTWith (sbvConfig config) $ do
      (m, lt, _) <- lowerSinglePrim fabc
      let sbva :: Maybe (SBVType a) =
            M.lookup (SomeTerm a) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      let sbvb :: Maybe (SBVType b) =
            M.lookup (SomeTerm b) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      let sbvc :: Maybe (SBVType c) =
            M.lookup (SomeTerm c) (biMapToSBV m)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      case (sbva, sbvb, sbvc) of
        (Just sbvav, Just sbvbv, Just sbvcv) -> SBV.query $ do
          SBV.constrain $ lt emptyQuantifiedStack SBV..== sbvfun sbvav sbvbv sbvcv
          satres <- SBV.checkSat
          case satres of
            SBV.Sat -> return ()
            _ -> lift $ assertFailure $ T.unpack $ "Lowering for " <> name <> " generated unsolvable formula"
        _ -> lift $ assertFailure "Failed to extract the term"
    SBV.runSMTWith (sbvConfig config) $ do
      (m, lt, _) <- lowerSinglePrim fabc
      (m2, p, _) <- lowerSinglePrimCached (precond a b c) m
      let sbva :: Maybe (SBVType a) =
            M.lookup (SomeTerm a) (biMapToSBV m2)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      let sbvb :: Maybe (SBVType b) =
            M.lookup (SomeTerm b) (biMapToSBV m2)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      let sbvc :: Maybe (SBVType c) =
            M.lookup (SomeTerm c) (biMapToSBV m2)
              >>= \f -> fromDynamic (f emptyQuantifiedStack)
      case (sbva, sbvb, sbvc) of
        (Just sbvav, Just sbvbv, Just sbvcv) -> SBV.query $ do
          SBV.constrain $
            (lt emptyQuantifiedStack SBV../= sbvfun sbvav sbvbv sbvcv)
              SBV..&& p emptyQuantifiedStack
          r <- SBV.checkSat
          case r of
            SBV.Sat -> do
              counterExampleA <- SBV.getValue sbvav
              counterExampleB <- SBV.getValue sbvbv
              counterExampleC <- SBV.getValue sbvcv
              lift $
                assertFailure $
                  "Translation counter example found: "
                    ++ show (counterExampleA, counterExampleB, counterExampleC)
            SBV.Unsat -> return ()
            _ -> lift $ assertFailure $ T.unpack $ "Lowering for " <> name <> " generated unknown formula"
        _ -> lift $ assertFailure "Failed to extract the term"
  
  modelParseTestBody ::
    forall t.
    ( Solvable t (SymType t),
      SymEq (SymType t),
      EvalSym (SymType t),
      KeyEq (SymType t),
      Show (SymType t)
    ) =>
    t ->
    Assertion
  modelParseTestBody v = do
    let a = "a" :: SymType t
    r <- solve z3 $ a .== con v
    case r of
      Left err -> assertFailure $ "Failed to solve: " ++ show err
      Right m -> AsKey (evalSym False m a) @?= AsKey (con v)
  
  testModelParse ::
    forall t.
    ( Show t,
      Arbitrary t,
      Solvable t (SymType t),
      SymEq (SymType t),
      EvalSym (SymType t),
      Show (SymType t),
      Typeable t,
      KeyEq (SymType t)
    ) =>
    Test
  testModelParse = testProperty ("Model parse(" ++ show (typeRep @t) ++ ")") $
    \(v :: t) -> ioProperty $ modelParseTestBody v
  
  loweringTests :: Test
  loweringTests =
    let unboundedConfig = z3 {sbvConfig = SBV.z3 {SBV.solverSetOptions = [SBV.SetLogic SBV.Logic_ALL]}}
     in testGroup
          "Lowering"
          [ plusTestOptions (mempty {topt_timeout = Just (Just 1000000)}) $
              testCase "proper memo" $ do
                let pair = ("a" :: SymInteger, "b" :: SymInteger)
                let iter (x, y) = (y, x + y)
                let r = iterate iter pair !! 100
                m <- solve z3 $ snd r .== 0
                assertBool "should success" $ isRight m,
            testGroup
              "Bool Lowering"
              [ testModelParse @Bool,
                testCase "Not" $ do
                  testUnaryOpLowering @Bool @Bool unboundedConfig notTerm "not" SBV.sNot,
                testCase "And" $ do
                  testBinaryOpLowering @Bool @Bool @Bool unboundedConfig andTerm "and" (SBV..&&)
                  testBinaryOpLowering @Bool @Bool @Bool
                    unboundedConfig
                    andTerm
                    "and"
                    (\x y -> SBV.sNot (x SBV..<+> y) SBV..&& (x SBV..|| y)),
                testCase "Or" $ do
                  testBinaryOpLowering @Bool @Bool @Bool unboundedConfig orTerm "or" (SBV..||)
                  testBinaryOpLowering @Bool @Bool @Bool
                    unboundedConfig
                    orTerm
                    "or"
                    (\x y -> (x SBV..<+> y) SBV..|| (x SBV..&& y)),
                testCase "Eqv" $ do
                  testBinaryOpLowering @Bool @Bool @Bool unboundedConfig eqTerm "eqv" (SBV..==)
                  testBinaryOpLowering @Bool @Bool @Bool
                    unboundedConfig
                    eqTerm
                    "eqv"
                    (\x y -> SBV.sNot (x SBV..<+> y)),
                testCase "ITE" $ do
                  let truePrecond _ _ _ = conTerm True
                  testTernaryOpLowering @Bool @Bool @Bool @Bool
                    unboundedConfig
                    truePrecond
                    iteTerm
                    "ite"
                    SBV.ite
                  testTernaryOpLowering @Bool @Bool @Bool @Bool
                    unboundedConfig
                    truePrecond
                    iteTerm
                    "ite"
                    (\c x y -> (c SBV..=> x) SBV..&& (SBV.sNot c SBV..=> y))
              ],
            testGroup
              "Integer Lowering"
              [ testModelParse @Integer,
                testCase "Add" $ do
                  testBinaryOpLowering @Integer @Integer @Integer unboundedConfig addNumTerm "(+)" (+)
                  testBinaryOpLowering @Integer @Integer @Integer
                    unboundedConfig
                    addNumTerm
                    "(+)"
                    (\x y -> (x + 1) * (y + 1) - x * y - 1),
                testCase "Uminus" $ do
                  testUnaryOpLowering @Integer @Integer unboundedConfig negNumTerm "negate" negate
                  testUnaryOpLowering @Integer @Integer
                    unboundedConfig
                    negNumTerm
                    "negate"
                    (\x -> (x + 1) * (x + 1) - 3 * x - x * x - 1),
                testCase "Abs" $ do
                  testUnaryOpLowering @Integer @Integer unboundedConfig absNumTerm "abs" abs,
                testCase "Signum" $ do
                  testUnaryOpLowering @Integer @Integer unboundedConfig signumNumTerm "signum" signum,
                testCase "Times" $ do
                  testBinaryOpLowering @Integer @Integer @Integer unboundedConfig mulNumTerm "(*)" (*)
                  testBinaryOpLowering @Integer @Integer @Integer
                    unboundedConfig
                    mulNumTerm
                    "(*)"
                    (\x y -> (x + 1) * (y + 1) - x - y - 1),
                testCase "Lt" $ do
                  testBinaryOpLowering @Integer @Integer @Bool unboundedConfig ltOrdTerm "(<)" (SBV..<)
                  testBinaryOpLowering @Integer @Integer @Bool
                    unboundedConfig
                    ltOrdTerm
                    "(<)"
                    (\x y -> x * 2 - x SBV..< y * 2 - y),
                testCase "Le" $ do
                  testBinaryOpLowering @Integer @Integer @Bool unboundedConfig leOrdTerm "(<=)" (SBV..<=)
                  testBinaryOpLowering @Integer @Integer @Bool
                    unboundedConfig
                    leOrdTerm
                    "(<=)"
                    (\x y -> x * 2 - x SBV..<= y * 2 - y),
                testCase "Div" $ do
                  testBinaryOpLowering @Integer @Integer @Integer unboundedConfig divIntegralTerm "div" SBV.sDiv,
                testCase "Mod" $ do
                  testBinaryOpLowering @Integer @Integer @Integer unboundedConfig modIntegralTerm "mod" SBV.sMod,
                testCase "Quot" $ do
                  testBinaryOpLowering @Integer @Integer @Integer unboundedConfig quotIntegralTerm "quot" SBV.sQuot,
                testCase "Rem" $ do
                  testBinaryOpLowering @Integer @Integer @Integer unboundedConfig remIntegralTerm "rem" SBV.sRem
              ],
            testGroup
              "IntN Lowering"
              [ testModelParse @(IntN 4),
                testCase "Add" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig addNumTerm "(+)" (+)
                  testBinaryOpLowering @(IntN 5) @(IntN 5)
                    unboundedConfig
                    addNumTerm
                    "(+)"
                    (\x y -> (x + 1) * (y + 1) - x * y - 1),
                testCase "Uminus" $ do
                  testUnaryOpLowering @(IntN 5) unboundedConfig negNumTerm "negate" negate
                  testUnaryOpLowering @(IntN 5)
                    unboundedConfig
                    negNumTerm
                    "negate"
                    (\x -> (x + 1) * (x + 1) - 3 * x - x * x - 1),
                testCase "Abs" $ do
                  testUnaryOpLowering @(IntN 5) unboundedConfig absNumTerm "abs" abs,
                testCase "Signum" $ do
                  testUnaryOpLowering @(IntN 5) unboundedConfig signumNumTerm "signum" signum,
                testCase "Times" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig mulNumTerm "(*)" (*)
                  testBinaryOpLowering @(IntN 5) @(IntN 5)
                    unboundedConfig
                    mulNumTerm
                    "(*)"
                    (\x y -> (x + 1) * (y + 1) - x - y - 1),
                testCase "Lt" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig ltOrdTerm "(<)" (SBV..<)
                  testBinaryOpLowering @(IntN 5) @(IntN 5)
                    unboundedConfig
                    ltOrdTerm
                    "(<)"
                    (\x y -> x * 2 - x SBV..< y * 2 - y),
                testCase "Le" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig leOrdTerm "(<=)" (SBV..<=)
                  testBinaryOpLowering @(IntN 5) @(IntN 5)
                    unboundedConfig
                    leOrdTerm
                    "(<=)"
                    (\x y -> x * 2 - x SBV..<= y * 2 - y),
                testCase "Extract" $ do
                  testUnaryOpLowering @(IntN 5) @(IntN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @1))
                    "select"
                    (SBV.bvExtract @0 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @1))
                    "select"
                    (SBV.bvExtract @1 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @2) (Proxy @1))
                    "select"
                    (SBV.bvExtract @2 @2 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @3) (Proxy @1))
                    "select"
                    (SBV.bvExtract @3 @3 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @4) (Proxy @1))
                    "select"
                    (SBV.bvExtract @4 @4 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @2))
                    "select"
                    (SBV.bvExtract @1 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @2))
                    "select"
                    (SBV.bvExtract @2 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @2) (Proxy @2))
                    "select"
                    (SBV.bvExtract @3 @2 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @3) (Proxy @2))
                    "select"
                    (SBV.bvExtract @4 @3 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 3)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @3))
                    "select"
                    (SBV.bvExtract @2 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 3)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @3))
                    "select"
                    (SBV.bvExtract @3 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 3)
                    unboundedConfig
                    (bvSelectTerm (Proxy @2) (Proxy @3))
                    "select"
                    (SBV.bvExtract @4 @2 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 4)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @4))
                    "select"
                    (SBV.bvExtract @3 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 4)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @4))
                    "select"
                    (SBV.bvExtract @4 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(IntN 5) @(IntN 5)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @5))
                    "select"
                    id,
                testCase "Extension" $ do
                  testUnaryOpLowering @(IntN 5) @(IntN 6)
                    unboundedConfig
                    (bvzeroExtendTerm (Proxy @6))
                    "bvzeroExtend"
                    SBV.zeroExtend
                  testUnaryOpLowering @(IntN 5) @(IntN 10)
                    unboundedConfig
                    (bvzeroExtendTerm (Proxy @10))
                    "bvzeroExtend"
                    SBV.zeroExtend
                  testUnaryOpLowering @(IntN 5) @(IntN 6)
                    unboundedConfig
                    (bvsignExtendTerm (Proxy @6))
                    "bvsignExtend"
                    SBV.signExtend
                  testUnaryOpLowering @(IntN 5) @(IntN 10)
                    unboundedConfig
                    (bvsignExtendTerm (Proxy @10))
                    "bvsignExtend"
                    SBV.signExtend,
                testCase "Concat" $ do
                  testBinaryOpLowering @(IntN 4) @(IntN 5) @(IntN 9)
                    unboundedConfig
                    bvConcatTerm
                    "bvconcat"
                    (SBV.#),
                testCase "AndBits" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig andBitsTerm "(.&.)" (.&.),
                testCase "OrBits" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig orBitsTerm "(.|.)" (.|.),
                testCase "XorBits" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) unboundedConfig xorBitsTerm "xor" xor,
                testCase "ComplementBits" $ do
                  testUnaryOpLowering @(IntN 5) unboundedConfig complementBitsTerm "complement" complement,
                testCase "ShiftLeft" $ do
                  testBinaryOpLowering @(IntN 5) unboundedConfig shiftLeftTerm "shiftLeft" SBV.sShiftLeft,
                testCase "ShiftRight" $ do
                  testBinaryOpLowering @(IntN 5) unboundedConfig shiftRightTerm "shiftRight" SBV.sShiftRight,
                testCase "RotateLeft" $ do
                  testBinaryOpLowering @(IntN 5)
                    unboundedConfig
                    rotateLeftTerm
                    "rotateLeft"
                    ( \a b ->
                        SBV.sFromIntegral $
                          SBV.sRotateLeft
                            (SBV.sFromIntegral a :: SBV.SWord 5)
                            (SBV.sFromIntegral b :: SBV.SWord 5)
                    ),
                testCase "RotateRight" $ do
                  testBinaryOpLowering @(IntN 5)
                    unboundedConfig
                    rotateRightTerm
                    "rotateRight"
                    ( \a b ->
                        SBV.sFromIntegral $
                          SBV.sRotateRight
                            (SBV.sFromIntegral a :: SBV.SWord 5)
                            (SBV.sFromIntegral b :: SBV.SWord 5)
                    ),
                testCase "Div - bounded" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) unboundedConfig divIntegralTerm "div" SBV.sDiv,
                testCase "Mod - bounded" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) unboundedConfig modIntegralTerm "mod" SBV.sMod,
                testCase "Quot - bounded" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) unboundedConfig quotIntegralTerm "quot" SBV.sQuot,
                testCase "Rem - bounded" $ do
                  testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) unboundedConfig remIntegralTerm "rem" SBV.sRem,
                testCase "BitCast" $ do
                  testUnaryOpLowering @(IntN 5) @(WordN 5) unboundedConfig bitCastTerm "bitCast" SBV.sFromIntegral
                  testUnaryOpLowering @(IntN 1) @Bool unboundedConfig bitCastTerm "bitCast" (`SBV.sTestBit` 0)
                  testUnaryOpLowering @Bool @(IntN 1) unboundedConfig bitCastTerm "bitCast" (\x -> SBV.ite x 1 0)
              ],
            testGroup
              "WordN"
              [ testModelParse @(WordN 4),
                testCase "Add" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig addNumTerm "(+)" (+)
                  testBinaryOpLowering @(WordN 5) @(WordN 5)
                    unboundedConfig
                    addNumTerm
                    "(+)"
                    (\x y -> (x + 1) * (y + 1) - x * y - 1),
                testCase "Uminus" $ do
                  testUnaryOpLowering @(WordN 5) unboundedConfig negNumTerm "negate" negate
                  testUnaryOpLowering @(WordN 5)
                    unboundedConfig
                    negNumTerm
                    "negate"
                    (\x -> (x + 1) * (x + 1) - 3 * x - x * x - 1),
                testCase "Abs" $ do
                  testUnaryOpLowering @(WordN 5) unboundedConfig absNumTerm "abs" abs,
                testCase "Signum" $ do
                  testUnaryOpLowering @(WordN 5) unboundedConfig signumNumTerm "signum" signum,
                testCase "Times" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig mulNumTerm "(*)" (*)
                  testBinaryOpLowering @(WordN 5) @(WordN 5)
                    unboundedConfig
                    mulNumTerm
                    "(*)"
                    (\x y -> (x + 1) * (y + 1) - x - y - 1),
                testCase "Lt" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig ltOrdTerm "(<)" (SBV..<)
                  testBinaryOpLowering @(WordN 5) @(WordN 5)
                    unboundedConfig
                    ltOrdTerm
                    "(<)"
                    (\x y -> x * 2 - x SBV..< y * 2 - y),
                testCase "Le" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig leOrdTerm "(<=)" (SBV..<=)
                  testBinaryOpLowering @(WordN 5) @(WordN 5)
                    unboundedConfig
                    leOrdTerm
                    "(<=)"
                    (\x y -> x * 2 - x SBV..<= y * 2 - y),
                testCase "Extract" $ do
                  testUnaryOpLowering @(WordN 5) @(WordN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @1))
                    "select"
                    (SBV.bvExtract @0 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @1))
                    "select"
                    (SBV.bvExtract @1 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @2) (Proxy @1))
                    "select"
                    (SBV.bvExtract @2 @2 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @3) (Proxy @1))
                    "select"
                    (SBV.bvExtract @3 @3 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 1)
                    unboundedConfig
                    (bvSelectTerm (Proxy @4) (Proxy @1))
                    "select"
                    (SBV.bvExtract @4 @4 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @2))
                    "select"
                    (SBV.bvExtract @1 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @2))
                    "select"
                    (SBV.bvExtract @2 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @2) (Proxy @2))
                    "select"
                    (SBV.bvExtract @3 @2 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 2)
                    unboundedConfig
                    (bvSelectTerm (Proxy @3) (Proxy @2))
                    "select"
                    (SBV.bvExtract @4 @3 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 3)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @3))
                    "select"
                    (SBV.bvExtract @2 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 3)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @3))
                    "select"
                    (SBV.bvExtract @3 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 3)
                    unboundedConfig
                    (bvSelectTerm (Proxy @2) (Proxy @3))
                    "select"
                    (SBV.bvExtract @4 @2 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 4)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @4))
                    "select"
                    (SBV.bvExtract @3 @0 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 4)
                    unboundedConfig
                    (bvSelectTerm (Proxy @1) (Proxy @4))
                    "select"
                    (SBV.bvExtract @4 @1 @5 Proxy Proxy)
                  testUnaryOpLowering @(WordN 5) @(WordN 5)
                    unboundedConfig
                    (bvSelectTerm (Proxy @0) (Proxy @5))
                    "select"
                    id,
                testCase "Extension" $ do
                  testUnaryOpLowering @(WordN 5) @(WordN 6)
                    unboundedConfig
                    (bvzeroExtendTerm (Proxy @6))
                    "bvzeroExtend"
                    SBV.zeroExtend
                  testUnaryOpLowering @(WordN 5) @(WordN 10)
                    unboundedConfig
                    (bvzeroExtendTerm (Proxy @10))
                    "bvzeroExtend"
                    SBV.zeroExtend
                  testUnaryOpLowering @(WordN 5) @(WordN 6)
                    unboundedConfig
                    (bvsignExtendTerm (Proxy @6))
                    "bvsignExtend"
                    SBV.signExtend
                  testUnaryOpLowering @(WordN 5) @(WordN 10)
                    unboundedConfig
                    (bvsignExtendTerm (Proxy @10))
                    "bvsignExtend"
                    SBV.signExtend,
                testCase "Concat" $ do
                  testBinaryOpLowering @(WordN 4) @(WordN 5) @(WordN 9)
                    unboundedConfig
                    bvConcatTerm
                    "bvconcat"
                    (SBV.#),
                testCase "AndBits" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig andBitsTerm "(.&.)" (.&.),
                testCase "OrBits" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig orBitsTerm "(.|.)" (.|.),
                testCase "XorBits" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) unboundedConfig xorBitsTerm "xor" xor,
                testCase "ComplementBits" $ do
                  testUnaryOpLowering @(WordN 5) unboundedConfig complementBitsTerm "complement" complement,
                testCase "ShiftLeft" $ do
                  testBinaryOpLowering @(WordN 5) unboundedConfig shiftLeftTerm "shiftLeft" SBV.sShiftLeft,
                testCase "ShiftRight" $ do
                  testBinaryOpLowering @(WordN 5) unboundedConfig shiftRightTerm "shiftRight" SBV.sShiftRight,
                testCase "RotateLeft" $ do
                  testBinaryOpLowering @(WordN 5) unboundedConfig rotateLeftTerm "rotateLeft" SBV.sRotateLeft,
                testCase "RotateRight" $ do
                  testBinaryOpLowering @(WordN 5) unboundedConfig rotateRightTerm "rotateRight" SBV.sRotateRight,
                testCase "Div" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) unboundedConfig divIntegralTerm "div" SBV.sDiv,
                testCase "Mod" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) unboundedConfig modIntegralTerm "mod" SBV.sMod,
                testCase "Quot" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) unboundedConfig quotIntegralTerm "quot" SBV.sQuot,
                testCase "Rem" $ do
                  testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) unboundedConfig remIntegralTerm "rem" SBV.sRem,
                testCase "BitCast" $ do
                  testUnaryOpLowering @(WordN 5) @(IntN 5) unboundedConfig bitCastTerm "bitCast" SBV.sFromIntegral
                  testUnaryOpLowering @(WordN 1) @Bool unboundedConfig bitCastTerm "bitCast" (`SBV.sTestBit` 0)
                  testUnaryOpLowering @Bool @(WordN 1) unboundedConfig bitCastTerm "bitCast" (\x -> SBV.ite x 1 0)
              ],
            testGroup
              "FP"
              [ testCase "Model parse (float)" $ modelParseTestBody (10.012 :: FP32),
                testModelParse @FPRoundingMode,
                testCase "Eqv" $
                  testBinaryOpLowering @FP32 @FP32 @Bool unboundedConfig eqTerm "eqv" (SBV..==),
                testCase "ITE" $ do
                  let precond _ l r =
                        pevalAndTerm
                          ( pevalNotTerm $
                              pevalFPTraitTerm FPIsNaN (l :: Term FP32)
                          )
                          ( pevalNotTerm $
                              pevalFPTraitTerm FPIsNaN (r :: Term FP32)
                          )
                  testTernaryOpLowering @Bool @FP32 @FP32 @FP32
                    unboundedConfig
                    precond
                    iteTerm
                    "ite"
                    SBV.ite,
                testGroup "FPTrait" $ do
                  (name, trait, op) <-
                    [ ("isNaN", FPIsNaN, SBV.fpIsNaN),
                      ("isPositive", FPIsPositive, SBV.fpIsPositive),
                      ("isNegative", FPIsNegative, SBV.fpIsNegative),
                      ( "isPositiveInfinite",
                        FPIsPositiveInfinite,
                        \x -> SBV.fpIsPositive x SBV..&& SBV.fpIsInfinite x
                      ),
                      ( "isNegativeInfinite",
                        FPIsNegativeInfinite,
                        \x -> SBV.fpIsNegative x SBV..&& SBV.fpIsInfinite x
                      ),
                      ("isInfinite", FPIsInfinite, SBV.fpIsInfinite),
                      ("isPositiveZero", FPIsPositiveZero, SBV.fpIsPositiveZero),
                      ("isNegativeZero", FPIsNegativeZero, SBV.fpIsNegativeZero),
                      ("isZero", FPIsZero, SBV.fpIsZero),
                      ("isNormal", FPIsNormal, SBV.fpIsNormal),
                      ("isSubnormal", FPIsSubnormal, SBV.fpIsSubnormal),
                      ("isPoint", FPIsPoint, SBV.fpIsPoint)
                    ]
                  return $ testCase name $ do
                    testUnaryOpLowering @FP32 @Bool
                      unboundedConfig
                      (fpTraitTerm trait)
                      "isNaN"
                      op,
                testCase "BitCastOr" $ do
                  testBinaryOpLowering @(WordN 8) @(FP 3 5)
                    unboundedConfig
                    bitCastOrTerm
                    "bitCastOr"
                    ( \d v ->
                        SBV.ite
                          (SBV.fpIsNaN v)
                          d
                          (SBV.sFloatingPointAsSWord v)
                    )
                  testBinaryOpLowering @(IntN 8) @(FP 3 5)
                    unboundedConfig
                    bitCastOrTerm
                    "bitCastOr"
                    ( \d v ->
                        SBV.ite
                          (SBV.fpIsNaN v)
                          d
                          (SBV.sFromIntegral $ SBV.sFloatingPointAsSWord v)
                    ),
                testCase "BitCast" $ do
                  testUnaryOpLowering' @(WordN 8) @(FP 3 5)
                    ( Just $ \x ->
                        SBV.sNot $
                          SBV.fpIsNaN
                            ( SBV.sWordAsSFloatingPoint x ::
                                SBV.SFloatingPoint 3 5
                            )
                    )
                    unboundedConfig
                    bitCastTerm
                    "bitCast"
                    SBV.sWordAsSFloatingPoint
                  testUnaryOpLowering' @(IntN 8) @(FP 3 5)
                    ( Just $ \x ->
                        SBV.sNot $
                          SBV.fpIsNaN
                            ( SBV.sWordAsSFloatingPoint . SBV.sFromIntegral $ x ::
                                SBV.SFloatingPoint 3 5
                            )
                    )
                    unboundedConfig
                    bitCastTerm
                    "bitCast"
                    (SBV.sWordAsSFloatingPoint . SBV.sFromIntegral)
              ],
            testGroup
              "AlgReal"
              [ testModelParse @AlgReal,
                testCase "Eqv" $
                  testBinaryOpLowering @AlgReal @AlgReal @Bool
                    unboundedConfig
                    eqTerm
                    "eqv"
                    (SBV..==),
                testCase "ITE" $ do
                  let truePrecond _ _ _ = conTerm True
                  testTernaryOpLowering @Bool @AlgReal @AlgReal @AlgReal
                    unboundedConfig
                    truePrecond
                    iteTerm
                    "ite"
                    SBV.ite,
                testCase "Add" $ do
                  testBinaryOpLowering @AlgReal @AlgReal @AlgReal unboundedConfig addNumTerm "(+)" (+)
                  testBinaryOpLowering @AlgReal @AlgReal @AlgReal
                    unboundedConfig
                    addNumTerm
                    "(+)"
                    (\x y -> (x + 1) * (y + 1) - x * y - 1),
                testCase "Uminus" $ do
                  testUnaryOpLowering @AlgReal @AlgReal unboundedConfig negNumTerm "negate" negate
                  testUnaryOpLowering @AlgReal @AlgReal
                    unboundedConfig
                    negNumTerm
                    "negate"
                    (\x -> (x + 1) * (x + 1) - 3 * x - x * x - 1),
                testCase "Abs" $
                  testUnaryOpLowering @AlgReal @AlgReal unboundedConfig absNumTerm "abs" abs,
                testCase "Signum" $
                  testUnaryOpLowering @AlgReal @AlgReal unboundedConfig signumNumTerm "signum" signum,
                testCase "Times" $ do
                  testBinaryOpLowering @AlgReal @AlgReal @AlgReal unboundedConfig mulNumTerm "(*)" (*)
                  testBinaryOpLowering @AlgReal @AlgReal @AlgReal
                    unboundedConfig
                    mulNumTerm
                    "(*)"
                    (\x y -> (x + 1) * (y + 1) - x - y - 1),
                testCase "Lt" $ do
                  testBinaryOpLowering @Integer @Integer @Bool unboundedConfig ltOrdTerm "(<)" (SBV..<)
                  testBinaryOpLowering @Integer @Integer @Bool
                    unboundedConfig
                    ltOrdTerm
                    "(<)"
                    (\x y -> x * 2 - x SBV..< y * 2 - y),
                testCase "Le" $ do
                  testBinaryOpLowering @Integer @Integer @Bool unboundedConfig leOrdTerm "(<=)" (SBV..<=)
                  testBinaryOpLowering @Integer @Integer @Bool
                    unboundedConfig
                    leOrdTerm
                    "(<=)"
                    (\x y -> x * 2 - x SBV..<= y * 2 - y),
                testCase "fdiv" $ do
                  testBinaryOpLowering @AlgReal @AlgReal @AlgReal
                    unboundedConfig
                    fdivTerm
                    "fdiv"
                    (/),
                testCase "recip" $ do
                  testUnaryOpLowering @AlgReal @AlgReal
                    unboundedConfig
                    recipTerm
                    "recip"
                    recip,
                testGroup "Floating unary" $ do
                  (name, f, op) <-
                    -- Those unsupported by z3 are commented out
                    [ -- ("exp", exp, FloatingExp),
                      -- ("log", log, FloatingLog),
                      -- ("sqrt", sqrt, FloatingSqrt),
                      ("sin", sin, FloatingSin),
                      ("cos", cos, FloatingCos),
                      ("tan", tan, FloatingTan),
                      ("asin", asin, FloatingAsin),
                      ("acos", acos, FloatingAcos),
                      ("atan", atan, FloatingAtan),
                      ("sinh", sinh, FloatingSinh),
                      ("cosh", cosh, FloatingCosh),
                      ("tanh", tanh, FloatingTanh)
                    ]
                  return $
                    testCase name $
                      testUnaryOpLowering @AlgReal @AlgReal
                        unboundedConfig
                        (floatingUnaryTerm op)
                        name
                        f {-,
                          testCase "**" $ do
                            testBinaryOpLowering @AlgReal @AlgReal @AlgReal
                              unboundedConfig
                              powerTerm
                              "(**)"
                              (**)-}
              ],
            testCase "TabularFun" $ do
              let f = "f" :: SymInteger =~> SymInteger =~> SymInteger
              let a = "a" :: SymInteger
              let b = "b" :: SymInteger
              let c = "c" :: SymInteger
              let d = "d" :: SymInteger
              Right m <-
                solve unboundedConfig $
                  (f # a # b .== a + b)
                    .&& (f # a # c .== a + c)
                    .&& (f # a # d .== a + d)
                    .&& (f # b # d .== b + d)
                    .&& (a .== 10 .&& b .== 20 .&& c .== 30 .&& d .== 40)
              AsKey (evalSym False m (f # a # b .== a + b)) @?= con True
              AsKey (evalSym False m (f # a # c .== a + c)) @?= con True
              AsKey (evalSym False m (f # a # d .== a + d)) @?= con True
              AsKey (evalSym False m (f # b # d .== b + d)) @?= con True,
            testCase "GeneralFun" $ do
              let f = "f" :: SymInteger -~> SymInteger -~> SymInteger
              let a = "a" :: SymInteger
              let b = "b" :: SymInteger
              let c = "c" :: SymInteger
              let d = "d" :: SymInteger
              r <-
                solve unboundedConfig $
                  (f # a # b .== a + b)
                    .&& (f # a # c .== a + c)
                    .&& (f # a # d .== a + d)
                    .&& (f # b # d .== b + d)
                    .&& (a .== 10 .&& b .== 20 .&& c .== 30 .&& d .== 40)
              case r of
                Left err -> fail $ show err
                Right m -> do
                  AsKey (evalSym False m (f # a # b .== a + b)) @?= con True
                  AsKey (evalSym False m (f # a # c .== a + c)) @?= con True
                  AsKey (evalSym False m (f # a # d .== a + d)) @?= con True
                  AsKey (evalSym False m (f # b # d .== b + d)) @?= con True,
            sbvVersionCheck $
              testGroup
                "Quantifiers"
                [ testCase "Forall" $ do
                    let asym :: TypedConstantSymbol Integer = "a"
                    let a :: Term Integer = ssymTerm "a"
                    let xsym :: TypedConstantSymbol Integer = "x"
                    let x :: Term Integer = ssymTerm "x"
                    let xterm =
                          forallTerm
                            xsym
                            (eqTerm (addNumTerm a x) (addNumTerm x $ conTerm 10))
                    let yterm =
                          forallTerm
                            asym
                            (eqTerm (addNumTerm a x) (addNumTerm a $ conTerm 20))
                    SBV.runSMTWith SBV.z3 $ do
                      (m, v, _) <- lowerSinglePrim (andTerm xterm yterm)
                      let sbva =
                            M.lookup (SomeTerm a) (biMapToSBV m)
                              >>= \f -> fromDynamic (f emptyQuantifiedStack)
                      let sbvx =
                            M.lookup (SomeTerm x) (biMapToSBV m)
                              >>= \f -> fromDynamic (f emptyQuantifiedStack)
                      case (sbva, sbvx) of
                        (Just (sbvav :: SBV.SInteger), Just (sbvxv :: SBV.SInteger)) ->
                          SBV.query $ do
                            SBV.constrain $ v emptyQuantifiedStack
                            satres <- SBV.checkSat
                            case satres of
                              SBV.Sat -> do
                                av <- SBV.getValue sbvav
                                liftIO $ av @?= 10
                                xv <- SBV.getValue sbvxv
                                liftIO $ xv @?= 20
                              _ -> liftIO $ assertFailure "Unsat"
                        _ -> liftIO $ assertFailure "Failed to find a",
                  testCase "Forall failed" $ do
                    let xsym :: TypedConstantSymbol Integer = "x"
                    let x :: Term Integer = ssymTerm "x"
                    let xterm = forallTerm xsym (eqTerm x (conTerm 10))
                    SBV.runSMTWith SBV.z3 $ do
                      (_, v, _) <- lowerSinglePrim xterm
                      SBV.query $ do
                        SBV.constrain $ v emptyQuantifiedStack
                        satres <- SBV.checkSat
                        case satres of
                          SBV.Unsat -> return ()
                          _ -> liftIO $ assertFailure "Should be unsat",
                  testCase "Forall-Exists" $ do
                    let asym :: TypedConstantSymbol Integer = "a"
                    let a :: Term Integer = ssymTerm "a"
                    let xsym :: TypedConstantSymbol Integer = "x"
                    let x :: Term Integer = ssymTerm "x"
                    let xterm =
                          forallTerm xsym $ existsTerm asym (ltOrdTerm x a)
                    SBV.runSMTWith SBV.z3 $ do
                      (_, v, _) <- lowerSinglePrim xterm
                      SBV.query $ do
                        SBV.constrain $ v emptyQuantifiedStack
                        satres <- SBV.checkSat
                        case satres of
                          SBV.Sat -> return ()
                          _ -> liftIO $ assertFailure "Unsat",
                  testCase "Exists-Forall" $ do
                    let asym :: TypedConstantSymbol Integer = "a"
                    let a :: Term Integer = ssymTerm "a"
                    let xsym :: TypedConstantSymbol Integer = "x"
                    let x :: Term Integer = ssymTerm "x"
                    let xterm =
                          existsTerm asym $ forallTerm xsym (ltOrdTerm x a)
                    SBV.runSMTWith SBV.z3 $ do
                      (_, v, _) <- lowerSinglePrim xterm
                      SBV.query $ do
                        SBV.constrain $ v emptyQuantifiedStack
                        satres <- SBV.checkSat
                        case satres of
                          SBV.Unsat -> return ()
                          _ -> liftIO $ assertFailure "should be unsat"
                ]
          ]
  
  #if MIN_VERSION_sbv(10,1,0)
  sbvVersionCheck :: Test -> Test
  sbvVersionCheck = id
  #else
  sbvVersionCheck :: Test -> Test
  sbvVersionCheck _ = testGroup "Quantifiers" []
  #endif
  