diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,10 @@
 * Hackage: <http://hackage.haskell.org/package/sbvPlugin>
 * GitHub:  <http://github.com/LeventErkok/sbvPlugin>
 
+### Version 9.14.1, 2026-01-12
+  * Changes required to compile with GHC 9.14.1
+  * Bump up sbv dependence to >= 13.4
+  
 ### Version 9.12.1, 2025-03-12
   * Changes required to compile with GHC 9.12.1
   * Add support for CVC5, DReal, OpenSMT, and Bitwuzla as backend solvers
diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs
--- a/Data/SBV/Plugin/Analyze.hs
+++ b/Data/SBV/Plugin/Analyze.hs
@@ -599,7 +599,7 @@
                     resK  <- getComposite res
                     return $ wrap tvs $ foldr KFun resK argKs
  where wrap ts f         = foldr (KFun . mkUninterpreted) f ts
-       mkUninterpreted v = KBase $ S.KUserSort (show (occNameFS (occName (varName v)))) Nothing
+       mkUninterpreted v = KBase $ S.KADT (show (occNameFS (occName (varName v)))) [] []
 
        -- | Extract tuples, lists, or base kinds
        getComposite :: Type -> Eval SKind
@@ -630,7 +630,7 @@
                             case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of
                               k:_ -> return k
                               []  -> do nm <- mkValidName $ showSDoc flags (ppr bt)
-                                        let k = S.KUserSort nm Nothing
+                                        let k = S.KADT nm [] []
                                         liftIO $ modifyIORef rUITypes ((bt, k) :)
                                         return k
 
diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal
--- a/sbvPlugin.cabal
+++ b/sbvPlugin.cabal
@@ -1,6 +1,6 @@
 Cabal-Version     : 2.2
 Name              : sbvPlugin
-Version           : 9.12.1
+Version           : 9.14.1
 Category          : Formal methods, Theorem provers, Math, SMT, Symbolic Computation
 Synopsis          : Formally prove properties of Haskell programs using SBV/SMT
 Description       : GHC plugin for proving properties over Haskell functions using SMT solvers, based
@@ -18,11 +18,11 @@
 Build-Type        : Simple
 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md
 
-Tested-With       : GHC==9.12.1
+Tested-With       : GHC==9.14.1
 
 source-repository head
     type:       git
-    location:   git://github.com/LeventErkok/sbvPlugin.git
+    location:   https://github.com/LeventErkok/sbvPlugin.git
 
 Library
   default-language: Haskell2010
@@ -34,13 +34,13 @@
                   , Data.SBV.Plugin.Examples.MergeSort
                   , Data.SBV.Plugin.Examples.MicroController
   build-depends   : base >= 4.19 && < 5
-                  , sbv      >= 11.4
-                  , ghc      >= 9.12.1
+                  , sbv      >= 13.4
+                  , ghc      >= 9.14.1
                   , ghc-prim
                   , containers
                   , mtl
                   , template-haskell
-  Other-modules   : Data.SBV.Plugin.Analyze
+  other-modules   : Data.SBV.Plugin.Analyze
                   , Data.SBV.Plugin.Common
                   , Data.SBV.Plugin.Env
                   , Data.SBV.Plugin.Plugin