diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,9 @@
 # Changes
 
+## Version 0.2.0.0
+
+Update to grisette-0.4.0.0.
+
 ## Version 0.1.0.0
+
 Initial release.
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2021-2022, Sirui Lu (siruilu@cs.washington.edu)
+Copyright (c) 2021-2024, Sirui Lu (siruilu@cs.washington.edu)
 
 All rights reserved.
 
diff --git a/grisette-monad-coroutine.cabal b/grisette-monad-coroutine.cabal
--- a/grisette-monad-coroutine.cabal
+++ b/grisette-monad-coroutine.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.1.
+-- This file has been generated from package.yaml by hpack version 0.36.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:           grisette-monad-coroutine
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Support for monad-coroutine package with Grisette
 description:    Orphan instances and wrappers for monad-coroutine package with Grisette.
 category:       Formal Methods, Theorem Provers, Symbolic Computation, SMT
@@ -13,7 +13,7 @@
 bug-reports:    https://github.com/lsrcz/grisette-monad-coroutine/issues
 author:         Sirui Lu
 maintainer:     Sirui Lu (siruilu@cs.washington.edu)
-copyright:      2021-2023 Sirui Lu
+copyright:      2021-2024 Sirui Lu
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
@@ -25,7 +25,7 @@
   type: git
   location: https://github.com/lsrcz/grisette-monad-coroutine
 
-flag fast
+flag optimize
   description: Compile with O2 optimization
   manual: False
   default: True
@@ -42,12 +42,12 @@
   ghc-options: -Wall -ferror-spans
   build-depends:
       base >4.14 && <5
-    , grisette >=0.1.0 && <0.2
+    , grisette >=0.4.0 && <0.5
     , monad-coroutine >=0.9.0.4 && <9.3
-    , mtl >=2.2.2 && <2.3
-    , transformers >=0.5.6.2 && <0.6
+    , mtl >=2.2.2 && <2.4
+    , transformers >=0.5.6.2 && <0.7
   default-language: Haskell2010
-  if flag(fast)
+  if flag(optimize)
     ghc-options: -O2
   else
     ghc-options: -O0
@@ -63,18 +63,19 @@
       test
   ghc-options: -Wall -ferror-spans
   build-depends:
-      base >4.14 && <5
-    , grisette >=0.1.0 && <0.2
+      HUnit ==1.6.*
+    , QuickCheck >=2.13.2 && <2.15
+    , base >4.14 && <5
+    , grisette >=0.4.0 && <0.5
     , grisette-monad-coroutine
     , monad-coroutine >=0.9.0.4 && <9.3
-    , mtl >=2.2.2 && <2.3
-    , tasty >=1.1.0.3 && <1.5
-    , tasty-hunit ==0.10.*
-    , tasty-quickcheck >=0.10.1 && <0.11
-    , tasty-test-reporter >=0.1.1.2 && <0.2
-    , transformers >=0.5.6.2 && <0.6
+    , mtl >=2.2.2 && <2.4
+    , test-framework >=0.8.2 && <0.9
+    , test-framework-hunit >=0.3.0.2 && <0.4
+    , test-framework-quickcheck2 >=0.3.0.5 && <0.4
+    , transformers >=0.5.6.2 && <0.7
   default-language: Haskell2010
-  if flag(fast)
+  if flag(optimize)
     ghc-options: -O2
   else
     ghc-options: -O0
diff --git a/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs b/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs
--- a/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs
+++ b/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs
@@ -5,11 +5,14 @@
 module Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctorsTests where
 
 import Control.Monad.Coroutine.SuspensionFunctors
+import GHC.Stack (HasCallStack)
 import Grisette
 import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors ()
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.Framework.Providers.QuickCheck2
+import Test.HUnit (Assertion, assertFailure, (@?=))
+import Test.QuickCheck
 
 testMergeableSimpleEquivClass ::
   (HasCallStack, Mergeable x, Show x, Eq x) => x -> [DynamicSortedIdx] -> [(SymBool, x, x, x)] -> Assertion
@@ -17,15 +20,15 @@
   let (idxsT, s) = resolveStrategy rootStrategy x
   case s of
     SimpleStrategy m -> do
-      idxsT @=? idxs
+      idxsT @?= idxs
       go cases
       where
         go [] = return ()
         go ((c, t, f, r) : xs) = do
-          fst (resolveStrategy rootStrategy t) @=? idxs
-          fst (resolveStrategy rootStrategy f) @=? idxs
-          fst (resolveStrategy rootStrategy r) @=? idxs
-          m c t f @=? r
+          fst (resolveStrategy rootStrategy t) @?= idxs
+          fst (resolveStrategy rootStrategy f) @?= idxs
+          fst (resolveStrategy rootStrategy r) @?= idxs
+          m c t f @?= r
           go xs
     _ -> assertFailure $ "Bad strategy type for " ++ show x
 
@@ -35,19 +38,19 @@
   let (idxsT, s) = resolveStrategy rootStrategy x
   case s of
     SimpleStrategy m -> do
-      idxsT @=? idxs
+      idxsT @?= idxs
       go cases
       where
         go [] = return ()
         go ((c, t, f, r) : xs) = do
-          fst (resolveStrategy rootStrategy t) @=? idxs
-          fst (resolveStrategy rootStrategy f) @=? idxs
-          fst (resolveStrategy rootStrategy r) @=? idxs
-          vis (m c t f) @=? vis r
+          fst (resolveStrategy rootStrategy t) @?= idxs
+          fst (resolveStrategy rootStrategy f) @?= idxs
+          fst (resolveStrategy rootStrategy r) @?= idxs
+          vis (m c t f) @?= vis r
           go xs
     _ -> assertFailure $ "Bad strategy type for " ++ show (vis x)
 
-suspensionFunctorsTests :: TestTree
+suspensionFunctorsTests :: Test
 suspensionFunctorsTests =
   testGroup
     "SuspensionFunctorsSpec"
@@ -57,8 +60,8 @@
            in [ testProperty "Yield Integer Integer" $
                   ioProperty . \(x :: Integer, y :: Integer) -> do
                     let (idxs, SimpleStrategy s) = resolveStrategy rootStrategy (Yield x y)
-                    idxs @=? [DynamicSortedIdx x, DynamicSortedIdx y]
-                    visYield (s "a" (Yield x y) (Yield x y)) @=? visYield (Yield x y),
+                    idxs @?= [DynamicSortedIdx x, DynamicSortedIdx y]
+                    visYield (s "a" (Yield x y) (Yield x y)) @?= visYield (Yield x y),
                 testCase "Yield SymBool SymBool" $ do
                   testMergeableSimpleEquivClass'
                     (\(Yield a b) -> (a, b))
@@ -67,21 +70,21 @@
                     [ ( "a",
                         Yield "b" "c",
                         Yield "d" "e",
-                        Yield (ites "a" "b" "d") (ites "a" "c" "e")
+                        Yield (symIte "a" "b" "d") (symIte "a" "c" "e")
                       )
                     ],
                 testCase "Await SymBool SymBool" $ do
                   let SimpleStrategy s = rootStrategy :: MergingStrategy (Await SymBool SymBool)
-                  let a1 = Await nots
-                  let a2 = Await ("a" &&~)
+                  let a1 = Await symNot
+                  let a2 = Await ("a" .&&)
                   let Await a3 = s "b" a1 a2
-                  a3 "c" @=? ites "b" (nots "c") ("a" &&~ "c"),
+                  a3 "c" @?= symIte "b" (symNot "c") ("a" .&& "c"),
                 testCase "Request SymBool SymBool SymBool" $ do
                   let SimpleStrategy s = rootStrategy :: MergingStrategy (Request SymBool SymBool SymBool)
-                  let a1 = Request "a" nots
-                  let a2 = Request "b" ("c" &&~)
+                  let a1 = Request "a" symNot
+                  let a2 = Request "b" ("c" .&&)
                   let Request v3 a3 = s "d" a1 a2
-                  v3 @=? ites "d" "a" "b"
-                  a3 "e" @=? ites "d" (nots "e") ("c" &&~ "e")
+                  v3 @?= symIte "d" "a" "b"
+                  a3 "e" @?= symIte "d" (symNot "e") ("c" .&& "e")
               ]
     ]
diff --git a/test/Grisette/Lib/Control/Monad/CoroutineTests.hs b/test/Grisette/Lib/Control/Monad/CoroutineTests.hs
--- a/test/Grisette/Lib/Control/Monad/CoroutineTests.hs
+++ b/test/Grisette/Lib/Control/Monad/CoroutineTests.hs
@@ -8,10 +8,11 @@
 import Control.Monad.Coroutine.SuspensionFunctors
 import Grisette
 import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors ()
-import Test.Tasty
-import Test.Tasty.HUnit
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.HUnit (assertFailure, (@?=))
 
-coroutineTests :: TestTree
+coroutineTests :: Test
 coroutineTests =
   testGroup
     "CoroutineTests"
@@ -28,13 +29,13 @@
                         Coroutine (Yield SymBool) UnionM SymBool
                     )
             case v of
-              SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
-                x @=? ites "a" "b" "d"
-                y @=? ites "a" "c" "e"
+              Single (Left (Yield x (Coroutine (Single (Right y))))) -> do
+                x @?= symIte "a" "b" "d"
+                y @?= symIte "a" "c" "e"
               _ -> assertFailure "Failed to merge Coroutine",
           testCase "mrgReturn" $ do
             case (mrgReturn 1 :: Coroutine (Yield SymBool) UnionM Integer) of
-              Coroutine (SingleU (Right 1)) -> return ()
+              Coroutine (Single (Right 1)) -> return ()
               _ -> assertFailure "mrgReturn for Coroutine is not working",
           testCase "mrgIf" $ do
             let Coroutine v =
@@ -44,9 +45,9 @@
                     (Coroutine $ single $ Left $ Yield "d" $ Coroutine $ single $ Right "e") ::
                     Coroutine (Yield SymBool) UnionM SymBool
             case v of
-              SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
-                x @=? ites "a" "b" "d"
-                y @=? ites "a" "c" "e"
+              Single (Left (Yield x (Coroutine (Single (Right y))))) -> do
+                x @?= symIte "a" "b" "d"
+                y @?= symIte "a" "c" "e"
               _ -> assertFailure "Failed to merge Coroutine"
         ],
       testCase "Mergeable for Coroutine" $ do
@@ -57,9 +58,9 @@
               Coroutine (mrgReturn (Left (Yield "c" (Coroutine (mrgReturn (Right "d"))))))
         let Coroutine r = s "e" a1 a2
         case r of
-          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
-            x @=? ites "e" "a" "c"
-            y @=? ites "e" "b" "d"
+          Single (Left (Yield x (Coroutine (Single (Right y))))) -> do
+            x @?= symIte "e" "a" "c"
+            y @?= symIte "e" "b" "d"
           _ -> assertFailure "Bad shape",
       testCase "SimpleMergeable for Coroutine" $ do
         let a1 :: Coroutine (Yield SymBool) UnionM SymBool =
@@ -70,18 +71,18 @@
         let Coroutine r1 = mrgIte1 "e" a1 a2
         let Coroutine ru1 = mrgIf "e" a1 a2
         case r of
-          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
-            x @=? ites "e" "a" "c"
-            y @=? ites "e" "b" "d"
+          Single (Left (Yield x (Coroutine (Single (Right y))))) -> do
+            x @?= symIte "e" "a" "c"
+            y @?= symIte "e" "b" "d"
           _ -> assertFailure "Bad shape"
         case r1 of
-          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
-            x @=? ites "e" "a" "c"
-            y @=? ites "e" "b" "d"
+          Single (Left (Yield x (Coroutine (Single (Right y))))) -> do
+            x @?= symIte "e" "a" "c"
+            y @?= symIte "e" "b" "d"
           _ -> assertFailure "Bad shape"
         case ru1 of
-          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
-            x @=? ites "e" "a" "c"
-            y @=? ites "e" "b" "d"
+          Single (Left (Yield x (Coroutine (Single (Right y))))) -> do
+            x @?= symIte "e" "a" "c"
+            y @?= symIte "e" "b" "d"
           _ -> assertFailure "Bad shape"
     ]
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,18 +2,11 @@
 
 import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctorsTests
 import Grisette.Lib.Control.Monad.CoroutineTests
-import Test.Tasty
-import Test.Tasty.Ingredients
-import qualified Test.Tasty.Ingredients.ConsoleReporter as ConsoleReporter
-import qualified Test.Tasty.Runners.Reporter as Reporter
+import Test.Framework (defaultMain, testGroup)
 
 main :: IO ()
-main = defaultMainWithIngredients [composeReporters Reporter.ingredient ConsoleReporter.consoleTestReporter] tests
-
-tests :: TestTree
-tests =
-  testGroup
-    "grisette-monad-coroutine"
+main =
+  defaultMain
     [ testGroup
         "Grisette.Lib.Control.Monad"
         [ testGroup