diff --git a/tutorials/2_union.ipynb b/tutorials/2_union.ipynb
index 54ebac88..6ba2ad00 100644
--- a/tutorials/2_union.ipynb
+++ b/tutorials/2_union.ipynb
@@ -597,7 +597,7 @@
     "synthesisRewriteTarget expr sketch = do\n",
     "  let lhs = eval expr\n",
     "  let rhs = eval .# sketch\n",
-    "  r <- cegisForAll (precise z3) expr $ cegisPostCond $ lhs .== rhs\n",
+    "  r <- cegisForAll z3 expr $ cegisPostCond $ lhs .== rhs\n",
     "  case r of\n",
     "    (_, CEGISSuccess model) -> do\n",
     "      putStrLn \"Successfully synthesized RHS:\"\n",
@@ -917,7 +917,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 19,
    "id": "1b96410a-87c1-4437-8533-d191b8b3910b",
    "metadata": {},
    "outputs": [
@@ -959,6 +959,7 @@
        ".hoogle-class {\n",
        "font-weight: bold;\n",
        "}\n",
+       "\n",
        ".get-type {\n",
        "color: green;\n",
        "font-weight: bold;\n",
@@ -990,10 +991,12 @@
        ".err-msg.in.collapse {\n",
        "padding-top: 0.7em;\n",
        "}\n",
+       "\n",
        ".highlight-code {\n",
        "white-space: pre;\n",
        "font-family: monospace;\n",
        "}\n",
+       "\n",
        ".suggestion-warning { \n",
        "font-weight: bold;\n",
        "color: rgb(200, 130, 0);\n",
@@ -1005,6 +1008,7 @@
        ".suggestion-name {\n",
        "font-weight: bold;\n",
        "}\n",
+       "\n",
        "</style><span class='get-type'>return :: forall (m :: * -> *) a. Monad m => a -> m a</span>"
       ],
       "text/plain": [
@@ -1052,6 +1056,7 @@
        ".hoogle-class {\n",
        "font-weight: bold;\n",
        "}\n",
+       "\n",
        ".get-type {\n",
        "color: green;\n",
        "font-weight: bold;\n",
@@ -1083,10 +1088,12 @@
        ".err-msg.in.collapse {\n",
        "padding-top: 0.7em;\n",
        "}\n",
+       "\n",
        ".highlight-code {\n",
        "white-space: pre;\n",
        "font-family: monospace;\n",
        "}\n",
+       "\n",
        ".suggestion-warning { \n",
        "font-weight: bold;\n",
        "color: rgb(200, 130, 0);\n",
@@ -1098,6 +1105,7 @@
        ".suggestion-name {\n",
        "font-weight: bold;\n",
        "}\n",
+       "\n",
        "</style><span class='get-type'>mrgReturn :: forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a</span>"
       ],
       "text/plain": [
@@ -1196,7 +1204,7 @@
    "mimetype": "text/x-haskell",
    "name": "haskell",
    "pygments_lexer": "Haskell",
-   "version": "9.6.5"
+   "version": "9.8.2"
   }
  },
  "nbformat": 4,
diff --git a/tutorials/3_monad_transformer.ipynb b/tutorials/3_monad_transformer.ipynb
index d5b3542b..f5d2b867 100644
--- a/tutorials/3_monad_transformer.ipynb
+++ b/tutorials/3_monad_transformer.ipynb
@@ -904,7 +904,7 @@
     "  Assign \"res\" (mrgDiv (mrgI \"b\") (mrgVar \"a\"))\n",
     "  ]\n",
     "\n",
-    "solve (precise z3) $ simpleMerge $ do\n",
+    "solve z3 $ simpleMerge $ do\n",
     "  res <- runExceptT $ runProg [] prog\n",
     "  case res of\n",
     "    Left DivisionError -> mrgReturn $ con True\n",
@@ -948,7 +948,7 @@
     "  Assign \"res\" (mrgDiv (mrgI \"b\") (mrgVar \"a\"))\n",
     "  ]\n",
     "\n",
-    "solveExcept (precise z3) expectedPath $ runProg [] prog1"
+    "solveExcept z3 expectedPath $ runProg [] prog1"
    ]
   },
   {
@@ -985,7 +985,7 @@
    "mimetype": "text/x-haskell",
    "name": "haskell",
    "pygments_lexer": "Haskell",
-   "version": "9.6.5"
+   "version": "9.8.2"
   }
  },
  "nbformat": 4,