content: {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
  
  {-# HLINT ignore "Use elemIndex" #-}
  {-# HLINT ignore "Use elemIndices" #-}
  {-# HLINT ignore "Use nub" #-}
  {-# HLINT ignore "Use union" #-}
  {-# HLINT ignore "Use intersect" #-}
  {-# HLINT ignore "Use insert" #-}
  {-# HLINT ignore "Use group" #-}
  
  module Grisette.Lib.Data.ListTests (listTests) where
  
  import Data.List
    ( delete,
      deleteBy,
      deleteFirstsBy,
      dropWhileEnd,
      elemIndex,
      elemIndices,
      findIndex,
      findIndices,
      group,
      groupBy,
      insert,
      insertBy,
      intersect,
      intersectBy,
      isInfixOf,
      isPrefixOf,
      isSubsequenceOf,
      isSuffixOf,
      nub,
      nubBy,
      partition,
      stripPrefix,
      union,
      unionBy,
      (\\),
    )
  import Grisette
    ( ITEOp (symIte),
      LogicalOp (symNot, (.&&), (.||)),
      Solvable (con),
      SymBool,
      SymEq ((./=), (.==)),
      SymOrd (symCompare, (.<=), (.>=)),
      Union,
      mrgGroupBy,
      mrgIf,
    )
  import Grisette.Lib.Control.Applicative (mrgPure)
  import Grisette.Lib.Data.List
    ( mrgBreak,
      mrgDelete,
      mrgDeleteBy,
      mrgDeleteFirstsBy,
      mrgDrop,
      mrgDropWhile,
      mrgDropWhileEnd,
      mrgElemIndex,
      mrgElemIndices,
      mrgFilter,
      mrgFindIndex,
      mrgFindIndices,
      mrgGroup,
      mrgInsert,
      mrgInsertBy,
      mrgIntersect,
      mrgIntersectBy,
      mrgLookup,
      mrgNub,
      mrgNubBy,
      mrgPartition,
      mrgSpan,
      mrgSplitAt,
      mrgStripPrefix,
      mrgTake,
      mrgTakeWhile,
      mrgUnion,
      mrgUnionBy,
      symIsInfixOf,
      symIsPrefixOf,
      symIsSubsequenceOf,
      symIsSuffixOf,
      (.!?),
      (.\\),
    )
  import Grisette.SymPrim (SymInteger)
  import Grisette.TestUtil.SymbolicAssertion ((.@?=))
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.QuickCheck (Gen, forAll, ioProperty, listOf, oneof)
  
  aint, bint, cint, dint, eint, fint :: SymInteger
  aint = "a"
  bint = "b"
  cint = "c"
  dint = "d"
  eint = "e"
  fint = "f"
  
  ranint :: Gen SymInteger
  ranint = oneof $ return <$> [aint, bint, cint, dint, eint, fint, -1, 0, 1]
  
  ranilist :: Gen [SymInteger]
  ranilist = listOf ranint
  
  listTests :: Test
  listTests =
    testGroup
      "List"
      [ testGroup
          "mrgTake"
          [ testProperty "concrete int" $
              \(n :: Integer) -> forAll ranilist $ \ranilist -> ioProperty $ do
                let actual = mrgTake n ranilist :: Union [SymInteger]
                let expected = mrgPure $ take (fromInteger n) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = mrgTake aint [bint, cint, dint] :: Union [SymInteger]
              let expected =
                    mrgIf (aint .<= 0) (return []) $
                      mrgIf (aint .== 1) (return [bint]) $
                        mrgIf (aint .== 2) (return [bint, cint]) $
                          return [bint, cint, dint]
              actual .@?= expected
          ],
        testGroup
          "mrgDrop"
          [ testProperty "concrete int" $
              \(n :: Integer) -> forAll ranilist $ \ranilist -> ioProperty $ do
                let actual = mrgDrop n ranilist :: Union [SymInteger]
                let expected = mrgPure $ drop (fromInteger n) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = mrgDrop aint [bint, cint, dint] :: Union [SymInteger]
              let expected =
                    mrgIf (aint .>= 3) (return []) $
                      mrgIf (aint .== 2) (return [dint]) $
                        mrgIf (aint .== 1) (return [cint, dint]) $
                          return [bint, cint, dint]
              actual .@?= expected
          ],
        testGroup
          "mrgSplitAt"
          [ testProperty "concrete int" $
              \(n :: Integer) -> forAll ranilist $ \ranilist -> ioProperty $ do
                let actual =
                      mrgSplitAt n ranilist ::
                        Union ([SymInteger], [SymInteger])
                let expected = mrgPure $ splitAt (fromInteger n) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgSplitAt aint [bint, cint, dint] ::
                      Union ([SymInteger], [SymInteger])
              let expected =
                    mrgIf (aint .<= 0) (return ([], [bint, cint, dint])) $
                      mrgIf (aint .== 1) (return ([bint], [cint, dint])) $
                        mrgIf (aint .== 2) (return ([bint, cint], [dint])) $
                          return ([bint, cint, dint], [])
              actual .@?= expected
          ],
        testGroup
          "mrgTakeWhile"
          [ testProperty "concrete int" $
              \ranilist -> ioProperty $ do
                let actual = mrgTakeWhile (.== 0) ranilist :: Union [Integer]
                let expected = mrgPure $ takeWhile (== 0) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgTakeWhile (.== 0) [aint, bint, cint] :: Union [SymInteger]
              let expected =
                    mrgIf (aint ./= 0) (return []) $
                      mrgIf (bint ./= 0) (return [aint]) $
                        mrgIf (cint ./= 0) (return ([aint, bint])) $
                          return [aint, bint, cint]
              actual .@?= expected
          ],
        testGroup
          "mrgDropWhile"
          [ testProperty "concrete int" $
              \ranilist -> ioProperty $ do
                let actual = mrgDropWhile (.== 0) ranilist :: Union [Integer]
                let expected = mrgPure $ dropWhile (== 0) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgDropWhile (.== 0) [aint, bint, cint] :: Union [SymInteger]
              let expected =
                    mrgIf
                      ((aint .== 0 .&& bint .== 0) .&& cint .== 0)
                      (return [])
                      $ mrgIf (aint .== 0 .&& bint .== 0) (return [cint])
                      $ mrgIf (aint .== 0) (return ([bint, cint]))
                      $ return [aint, bint, cint]
              actual .@?= expected
          ],
        testGroup
          "mrgDropWhileEnd"
          [ testProperty "concrete int" $
              \ranilist -> ioProperty $ do
                let actual = mrgDropWhileEnd (.== 0) ranilist :: Union [Integer]
                let expected = mrgPure $ dropWhileEnd (== 0) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgDropWhileEnd (.== 0) [aint, bint, cint] ::
                      Union [SymInteger]
              let expected =
                    mrgIf
                      ((cint .== 0 .&& bint .== 0) .&& aint .== 0)
                      (return [])
                      $ mrgIf (cint .== 0 .&& bint .== 0) (return [aint])
                      $ mrgIf (cint .== 0) (return ([aint, bint]))
                      $ return [aint, bint, cint]
              actual .@?= expected
          ],
        testGroup
          "mrgSpan"
          [ testProperty "concrete int" $
              \ranilist -> ioProperty $ do
                let actual =
                      mrgSpan (.== 0) ranilist :: Union ([Integer], [Integer])
                let expected = mrgPure $ span (== 0) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgSpan (.== 0) [aint, bint, cint] ::
                      Union ([SymInteger], [SymInteger])
              let expected =
                    mrgIf (aint ./= 0) (return ([], [aint, bint, cint])) $
                      mrgIf (bint ./= 0) (return ([aint], [bint, cint])) $
                        mrgIf (cint ./= 0) (return ([aint, bint], [cint])) $
                          return ([aint, bint, cint], [])
              actual .@?= expected
          ],
        testGroup
          "mrgBreak"
          [ testProperty "concrete int" $
              \ranilist -> ioProperty $ do
                let actual =
                      mrgBreak (.== 0) ranilist :: Union ([Integer], [Integer])
                let expected = mrgPure $ break (== 0) ranilist
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgBreak (.== 0) [aint, bint, cint] ::
                      Union ([SymInteger], [SymInteger])
              let expected =
                    mrgIf (aint .== 0) (return ([], [aint, bint, cint])) $
                      mrgIf (bint .== 0) (return ([aint], [bint, cint])) $
                        mrgIf (cint .== 0) (return ([aint, bint], [cint])) $
                          return ([aint, bint, cint], [])
              actual .@?= expected
          ],
        testGroup
          "mrgStripPrefix"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = mrgStripPrefix l1 l2 :: Union (Maybe [Integer])
                let expected = mrgPure $ stripPrefix l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgStripPrefix [aint, bint] [cint, dint, eint] ::
                      Union (Maybe [SymInteger])
              let expected =
                    mrgIf
                      ((aint ./= cint) .|| (bint ./= dint))
                      (return Nothing)
                      (return $ Just [eint])
              actual .@?= expected
          ],
        testGroup
          "mrgGroup"
          [ testProperty "concrete int" $
              \l -> ioProperty $ do
                let actual = mrgGroup l :: Union [[Integer]]
                let expected = mrgPure $ group l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = mrgGroup [aint, bint, cint] :: Union [[SymInteger]]
              let expected =
                    mrgIf
                      (aint .== bint .&& aint .== cint)
                      (return [[aint, bint, cint]])
                      $ mrgIf
                        (aint .== bint .|| bint .== cint)
                        ( mrgIf (aint .== bint) (return [[aint, bint], [cint]]) $
                            return [[aint], [bint, cint]]
                        )
                      $ return [[aint], [bint], [cint]]
  
              actual .@?= expected
          ],
        testGroup
          "symIsPrefixOf"
          [ testProperty "concrete int" $
              \(l1 :: [Int]) l2 -> ioProperty $ do
                let actual = symIsPrefixOf l1 l2 :: SymBool
                let expected = con $ isPrefixOf l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = symIsPrefixOf [aint, bint] [cint, dint, eint]
              actual .@?= (aint .== cint .&& bint .== dint),
            testCase "symbolic int, not long enough" $ do
              let actual = symIsPrefixOf [cint, dint, eint] [aint, bint]
              actual .@?= con False
          ],
        testGroup
          "symIsSuffixOf"
          [ testProperty "concrete int" $
              \(l1 :: [Int]) l2 -> ioProperty $ do
                let actual = symIsSuffixOf l1 l2 :: SymBool
                let expected = con $ isSuffixOf l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = symIsSuffixOf [aint, bint] [cint, dint, eint]
              actual .@?= (bint .== eint .&& aint .== dint),
            testCase "symbolic int, not long enough" $ do
              let actual = symIsSuffixOf [cint, dint, eint] [aint, bint]
              actual .@?= con False
          ],
        testGroup
          "symIsInfixOf"
          [ testProperty "concrete int" $
              \(l1 :: [Int]) l2 -> ioProperty $ do
                let actual = symIsInfixOf l1 l2 :: SymBool
                let expected = con $ isInfixOf l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = symIsInfixOf [aint, bint] [cint, dint, eint, fint]
              actual
                .@?= ( (aint .== cint .&& bint .== dint)
                         .|| (aint .== dint .&& bint .== eint)
                     )
                .|| (aint .== eint .&& bint .== fint),
            testCase "symbolic int, not long enough" $ do
              let actual = symIsInfixOf [cint, dint, eint] [aint, bint]
              actual .@?= con False
          ],
        testGroup
          "symIsSubsequenceOf"
          [ testProperty "concrete int" $
              \(l1 :: [Int]) l2 -> ioProperty $ do
                let actual = symIsSubsequenceOf l1 l2 :: SymBool
                let expected = con $ isSubsequenceOf l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    symIsSubsequenceOf [aint, bint] [cint, dint, eint, fint]
              actual
                .@?= symIte
                  (aint .== cint)
                  (bint .== dint .|| (bint .== eint .|| bint .== fint))
                  ( symIte
                      (aint .== dint)
                      (bint .== eint .|| bint .== fint)
                      (aint .== eint .&& bint .== fint)
                  ),
            testCase "symbolic int, not long enough" $ do
              let actual = symIsSubsequenceOf [cint, dint, eint] [aint, bint]
              actual .@?= con False
          ],
        testGroup
          "mrgLookup"
          [ testProperty "concrete int" $
              \v l -> ioProperty $ do
                let actual = mrgLookup (v :: Integer) l :: Union (Maybe Integer)
                let expected = mrgPure $ lookup v l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgLookup
                      aint
                      [ (bint, Just cint),
                        (dint, Nothing),
                        (fint, Just eint)
                      ] ::
                      Union (Maybe (Maybe SymInteger))
              let expected =
                    mrgIf
                      ((aint ./= bint .&& aint ./= dint) .&& aint ./= fint)
                      (return Nothing)
                      $ mrgIf (aint .== bint) (return $ Just $ Just cint)
                      $ mrgIf
                        (aint .== dint)
                        (return $ Just Nothing)
                        (return $ Just $ Just eint)
              actual .@?= expected
          ],
        testGroup
          "mrgFilter"
          [ testProperty "concrete int" $
              \l -> ioProperty $ do
                let actual = mrgFilter (.== 0) l :: Union [Integer]
                let expected = mrgPure $ filter (== 0) l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgFilter (.== 0) [aint, bint] :: Union [SymInteger]
              let expected =
                    mrgIf (aint ./= 0 .&& bint ./= 0) (return []) $
                      mrgIf
                        (aint ./= 0 .|| bint ./= 0)
                        (return [symIte (aint .== 0) aint bint])
                        (return [aint, bint])
              actual .@?= expected
          ],
        testGroup
          "mrgPartition"
          [ testProperty "concrete int" $
              \l -> ioProperty $ do
                let actual =
                      mrgPartition (.== 0) l ::
                        Union ([Integer], [Integer])
                let expected = mrgPure $ partition (== 0) l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgPartition (.== 0) [aint, bint] ::
                      Union ([SymInteger], [SymInteger])
              let expected =
                    mrgIf
                      (aint ./= 0 .&& bint ./= 0)
                      (return ([], [aint, bint]))
                      $ mrgIf
                        (aint ./= 0 .|| bint ./= 0)
                        ( return
                            ( [symIte (aint .== 0) aint bint],
                              [symIte (aint .== 0) bint aint]
                            )
                        )
                        (return ([aint, bint], []))
              actual .@?= expected
          ],
        testGroup
          ".!?"
          [ testProperty "concrete int" $
              \l (i :: Int) -> ioProperty $ do
                let actual = l .!? i :: Union (Maybe Integer)
                let expected =
                      mrgPure $
                        if i < 0 || i >= length l then Nothing else Just $ l !! i
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    [aint, bint, cint] .!? dint :: Union (Maybe SymInteger)
              let expected =
                    mrgIf
                      (dint ./= 0 .&& dint ./= 1 .&& dint ./= 2)
                      (return Nothing)
                      ( return $
                          Just $
                            symIte (dint .== 0) aint $
                              symIte (dint .== 1) bint cint
                      )
              actual .@?= expected
          ],
        testGroup
          "mrgElemIndex"
          [ testProperty "concrete int" $
              \(v :: Integer) l -> ioProperty $ do
                let actual = mrgElemIndex v l :: Union (Maybe Int)
                let expected = mrgPure $ elemIndex v l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgElemIndex aint [bint, cint, dint] ::
                      Union (Maybe SymInteger)
              let expected =
                    mrgIf
                      (aint ./= bint .&& aint ./= cint .&& aint ./= dint)
                      (mrgPure Nothing)
                      ( mrgPure $
                          Just $
                            symIte (aint .== bint) 0 (symIte (aint .== cint) 1 2)
                      )
              actual .@?= expected
          ],
        testGroup
          "mrgElemIndices"
          [ testProperty "concrete int" $
              \(v :: Integer) l -> ioProperty $ do
                let actual = mrgElemIndices v l :: Union [Int]
                let expected = mrgPure $ elemIndices v l
                actual .@?= expected
          ],
        testGroup
          "mrgFindIndex"
          [ testProperty "concrete int" $
              \(l :: [Integer]) -> ioProperty $ do
                let actual = mrgFindIndex (.== 0) l :: Union (Maybe Int)
                let expected = mrgPure $ findIndex (== 0) l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgFindIndex (.== 0) [aint, bint, cint] ::
                      Union (Maybe SymInteger)
              let expected =
                    mrgIf
                      (aint ./= 0 .&& bint ./= 0 .&& cint ./= 0)
                      (mrgPure Nothing)
                      ( mrgPure $
                          Just $
                            symIte (aint .== 0) 0 (symIte (bint .== 0) 1 2)
                      )
              actual .@?= expected
          ],
        testGroup
          "mrgFindIndices"
          [ testProperty "concrete int" $
              \(l :: [Integer]) -> ioProperty $ do
                let actual = mrgFindIndices (.== 0) l :: Union [Int]
                let expected = mrgPure $ findIndices (== 0) l
                actual .@?= expected
          ],
        testGroup
          "mrgNub"
          [ testProperty "concrete int" $
              \l -> ioProperty $ do
                let actual = mrgNub l :: Union [Integer]
                let expected = mrgPure $ nub l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual = mrgNub [aint, bint, cint] :: Union [SymInteger]
              let expected =
                    mrgIf
                      (bint .== aint .&& cint .== aint)
                      (return [aint])
                      $ mrgIf
                        (bint .== aint .|| cint .== bint .|| cint .== aint)
                        (return [aint, symIte (bint .== aint) cint bint])
                        (return [aint, bint, cint])
              actual .@?= expected
          ],
        testGroup
          "mrgDelete"
          [ testProperty "concrete int" $
              \i l -> ioProperty $ do
                let actual = mrgDelete i l :: Union [Integer]
                let expected = mrgPure $ delete i l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgDelete aint [bint, cint, dint] :: Union [SymInteger]
              let expected =
                    mrgIf
                      (aint .== bint .|| aint .== cint .|| aint .== dint)
                      ( return
                          [ symIte (aint .== bint) cint bint,
                            symIte (aint .== bint .|| aint .== cint) dint cint
                          ]
                      )
                      (return [bint, cint, dint])
              actual .@?= expected
          ],
        testGroup
          ".\\\\"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = l1 .\\ l2 :: Union [Integer]
                let expected = mrgPure $ l1 \\ l2
                actual .@?= expected
          ],
        testGroup
          "mrgUnion"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = mrgUnion l1 l2 :: Union [Integer]
                let expected = mrgPure $ union l1 l2
                actual .@?= expected
          ],
        testGroup
          "mrgIntersect"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = mrgIntersect l1 l2 :: Union [Integer]
                let expected = mrgPure $ intersect l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgIntersect [aint, bint] [cint, dint] :: Union [SymInteger]
              let expected =
                    mrgIf
                      ( symNot $
                          (bint .== cint .|| bint .== dint)
                            .|| (aint .== cint .|| aint .== dint)
                      )
                      (return [])
                      ( mrgIf
                          ( symNot $
                              (bint .== cint .|| bint .== dint)
                                .&& (aint .== cint .|| aint .== dint)
                          )
                          ( return
                              [symIte (bint .== cint .|| bint .== dint) bint aint]
                          )
                          (return [aint, bint])
                      )
              actual .@?= expected
          ],
        testGroup
          "mrgNubBy"
          [ testProperty "concrete int" $
              \l -> ioProperty $ do
                let actual = mrgNubBy (.==) l :: Union [Integer]
                let expected = mrgPure $ nubBy (==) l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgNubBy (.==) [aint, bint, cint] :: Union [SymInteger]
              let expected =
                    mrgIf
                      (bint .== aint .&& cint .== aint)
                      (return [aint])
                      $ mrgIf
                        (bint .== aint .|| cint .== bint .|| cint .== aint)
                        (return [aint, symIte (bint .== aint) cint bint])
                        (return [aint, bint, cint])
              actual .@?= expected
          ],
        testGroup
          "mrgDeleteBy"
          [ testProperty "concrete int" $
              \i l -> ioProperty $ do
                let actual = mrgDeleteBy (./=) i l :: Union [Integer]
                let expected = mrgPure $ deleteBy (/=) i l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgDeleteBy (./=) aint [bint, cint, dint] ::
                      Union [SymInteger]
              let expected =
                    mrgIf
                      (aint ./= bint .|| aint ./= cint .|| aint ./= dint)
                      ( return
                          [ symIte (aint ./= bint) cint bint,
                            symIte (aint ./= bint .|| aint ./= cint) dint cint
                          ]
                      )
                      (return [bint, cint, dint])
              actual .@?= expected
          ],
        testGroup
          "mrgDeleteFirstsBy"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = mrgDeleteFirstsBy (./=) l1 l2 :: Union [Integer]
                let expected = mrgPure $ deleteFirstsBy (/=) l1 l2
                actual .@?= expected
          ],
        testGroup
          "mrgUnionBy"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = mrgUnionBy (.==) l1 l2 :: Union [Integer]
                let expected = mrgPure $ unionBy (==) l1 l2
                actual .@?= expected
          ],
        testGroup
          "mrgIntersectBy"
          [ testProperty "concrete int" $
              \l1 l2 -> ioProperty $ do
                let actual = mrgIntersectBy (.==) l1 l2 :: Union [Integer]
                let expected = mrgPure $ intersectBy (==) l1 l2
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgIntersectBy (.==) [aint, bint] [cint, dint] ::
                      Union [SymInteger]
              let expected =
                    mrgIf
                      ( symNot $
                          (bint .== cint .|| bint .== dint)
                            .|| (aint .== cint .|| aint .== dint)
                      )
                      (return [])
                      ( mrgIf
                          ( symNot $
                              (bint .== cint .|| bint .== dint)
                                .&& (aint .== cint .|| aint .== dint)
                          )
                          ( return
                              [symIte (bint .== cint .|| bint .== dint) bint aint]
                          )
                          (return [aint, bint])
                      )
              actual .@?= expected
          ],
        testGroup
          "mrgGroupBy"
          [ testProperty "concrete int" $
              \l -> ioProperty $ do
                let actual = mrgGroupBy (.==) l :: Union [[Integer]]
                let expected = mrgPure $ groupBy (==) l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgGroupBy (.==) [aint, bint, cint] :: Union [[SymInteger]]
              let expected =
                    mrgIf
                      (aint .== bint .&& aint .== cint)
                      (return [[aint, bint, cint]])
                      $ mrgIf
                        (aint .== bint .|| bint .== cint)
                        ( mrgIf (aint .== bint) (return [[aint, bint], [cint]]) $
                            return [[aint], [bint, cint]]
                        )
                      $ return [[aint], [bint], [cint]]
  
              actual .@?= expected
          ],
        testGroup
          "mrgInsert"
          [ testProperty "concrete int" $
              \i l -> ioProperty $ do
                let actual = mrgInsert i l :: Union [Integer]
                let expected = mrgPure $ insert i l
                actual .@?= expected,
            testCase "symbolic int" $ do
              let actual =
                    mrgInsert aint [bint, cint, dint] :: Union [SymInteger]
              let expected =
                    mrgPure
                      [ symIte (aint .<= bint) aint bint,
                        symIte (aint .<= bint) bint $
                          symIte (aint .<= cint) aint cint,
                        symIte (aint .<= bint .|| aint .<= cint) cint $
                          symIte (aint .<= dint) aint dint,
                        symIte
                          (aint .<= bint .|| aint .<= cint .|| aint .<= dint)
                          dint
                          aint
                      ]
              actual .@?= expected
          ],
        testGroup
          "mrgInsertBy"
          [ testProperty "concrete int" $
              \i l -> ioProperty $ do
                let actual = mrgInsertBy symCompare i l :: Union [Integer]
                let expected = mrgPure $ insertBy compare i l
                actual .@?= expected
          ]
      ]
  